Resumen de lecturas compartidas durante junio de 2020
Esta entrada es una recopilación de lecturas compartidas, durante junio de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
- Breve historia de Haskell. ~ Emanuel Goette (@emanuelpeg). #Haskell #ProgramaciónFuncional
- The Nash-Williams partition theorem in Isabelle/HOL. ~ Lawrence C. Paulson. #ITP #IsabelleHOL
- Setting up a Haskell development environment with Nix. ~ Romain Viallard. #Haskell #Nix
- Big step normalisation for type theory. ~ Thorsten Altenkirch, Colin Geniet. #ITP #Agda
- Carnegie Mellon tool automatically turns math into pictures. #Math
- Penrose: from mathematical notation to beautiful diagrams. ~ Katherine Ye el als. #Math
- Welcome to The Proof Theory Blog! ~ Anupam Das. #Logic #Math
- Penrose: Create beautiful diagrams just by typing mathematical notation in plain text. #Haskell #DSL #Math #Visualization
- Lean tutorial for mere mortals. ~ Alcides Fonseca. #ITP #LeanProver
- A formally verified checker of the safe distance traffic rules for autonomous vehicles. ~ Albert Rizaldi, Fabian Immler. #ITP #IsabelleHOL
- Isomorphic data type transformations. ~ Alessandro Coglio, Stephen Westfold. #ITP #ACL2
- Cellular cohomology in homotopy type theory. ~ Ulrik Buchholtz, Kuen-Bang Hou. #ITP #Agda #Math
- A history of Clojure. ~ Rich Hickey. #Clojure #FunctionalProgramming
- Adventures in refactoring. ~ Sam Tay. #Haskell #FunctionalProgramming
- Reanimate: a tutorial on making programmatic animations. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
- Using Template Haskell to generate boilerplate. ~ Jonathan Dowland. #Haskell #FunctionalProgramming
- Simulated annealing. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming
- Trusting toList. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
- Formal verification: History and methods. ~ Danya Rogozin. #FormalVerification
- Red Blob Games: interactive visual explanations of math and algorithms, using motivating examples from computer games. ~ Amit Patel. #Algorithms
- Toy machine learning with Haskell. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming #MachineLearning
- The sphere eversion project. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Algorithm design with Haskell. ~ Richard Bird, Jeremy Gibbons.1#v=onepage&q&f=false #eBook #Haskell #FunctionalProgramming #Algorithms
- Formalization of the computational theory of a Turing complete functional language model. ~ TMF Ramos, AA Almeida, M Ayala-Rincón. #ITP #PVS
- The proof-theoretic foundations of logic programming. ~ Dale Miller. #LogicProgramming
- What is Mathematics? ~ Get Smarter. #Math
- Formalizing text editors in Coq. ~ Boro Sitnikovski. #ITP #Coq
- Making the most of Cabal. ~ Luke Lau. #Haskell #FunctionalProgramming
- The pain points of Haskell: A practical summary. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming
- Functional programming in data science projects. ~ Nathanael Weill. #FuncionalProgramming #DataScience
- Using client-side Haskell web frameworks in CodeWorld. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld
- 4 excellent free books to learn Agda and type theory. ~ Erik Karlsson. #ITP #Agda #FunctionalProgramming #TypeTheory
- Disco: Functional teaching language for use in a discrete mathematics course. ~ Brent Yorgey. #Haskell #FunctionalProgramming #DSL #Math
- Hoogle searching overview. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
- The ‘useless’ perspective that transformed mathematics. ~ Kevin Hartnett (@KSHartnett). #Math
- “The truth: What is the truth?”, at Gödel’s Lost Letter and P=NP. ~ R.J. Lipton. #Logic #Math
- Scripting in Haskell: Parsing command line arguments. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
- Template Haskell and stream-processing programs. ~ Jonathan Dowland (@jmtd). #Haskell #FunctionalProgramming
- How to design co-programs. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
- Conway’s circle theorem: a proof, this time with words. ~ Colin Beveridge, Elizabeth A. Williams. #Math
- Monadic equational reasoning in Coq. ~ Reynald Affeldt. #ITP #Coq
- Category theory for computing science. ~ Michael Barr, Charles Wells (1998). #eBook #CategoryTheory #Math #CompSci
- Seven sketches in compositionality: An invitation to applied category theory. ~ Brendan Fong, David I. Spivak (2018). #eBook #CategoryTheory #Math #CompSci
- What functional programming is, what it isn’t, and why it matters. ~ Noel Welsh. #FunctionalProgramming
- Simple Haskell install instructions – ZuriHac 2020. #Haskell #FunctionalProgramming
- La logique: un instrument théorique pour des problèmes pratiques. ~ Franco Raimondi. #Logic #Math #CompSci
- Deploying your application with NixOS. ~ Romain Viallard. #Nix #Haskell
- An extended comparative study of language support for generic programming. ~ Ronald Garcia, Jaakko J Ärvi, Andrew Lumsdaine, Jeremy Siek, Jeremiah Willcock. #Cpp #SML #OCaml #Haskell #Eiffel #Java #Csharp #Cecil.
- Towards a verified first-stage bootloader in Coq. ~ Zygimantas Straznickas. #MsC_Thesis #ITP #Coq
- Completeness theorems for first-order logic analysed in constructive type theory. ~ Yannick Forster, Dominik Kirst, Dominik Weh. #ITP #Coq #Logic
- Efficient verified implementation of introsort and pdqsort. ~ Peter Lammich. #ITP #IsabelleHOL
- (Programming Languages) in Agda = Programming (Languages in Agda). ~ Philip Wadler. #ITP #Agda
- Verifying strong eventual consistency in δ-CRDTs. Taylor Blau. #ITP #IsabelleHOL
- The history of Standard ML. ~ David MacQueen, Robert Harper, John Reppy. #SML #FunctionalProgramming
- Programación funcional: Próximamente en un lenguaje de programación cerca de usted. ~ Andrés Marzal. #ProgramaciónFuncional
- Awesome Haskell videos (A collection of awesome Haskell videos). ~ @_andys8 #Haskell #FunctionalProgramming
- Type inference. ~ Splinter Suidman. #Haskell #FunctionalProgramming
- Practical proof search for Coq by type inhabitation. ~ Lukasz Czajka. #ITP #Coq
- Validating mathematical structures. ~ Kazuhiko Sakaguchi. #ITP #Coq #math
- Competing inheritance paths in dependent type theory: a case study in functional analysis. ~ Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling and Kazuhiko Sakaguchi. #ITP #Coq #Math
- Quotients of bounded natural functors. ~ Basil Fürer, Andreas Lochbihler, Joshua Schneider and Dmitriy Traytel. #ITP #IsabelleHOL
- Application of formal systems to model biological systems. ~ @prathyvsh #Math #Biology
- Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. ~ Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross and Adam Chlipala. #ITP #Coq
- Adventures in verifying arithmetic. ~ John Harrison. #ITP #HOL_Light #Math
- A formally verified, optimized monitor for metric first-order dynamic logic. ~ David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, Dmitriy Traytel. #ITP #IsabelleHOL
- The resolution of Keller’s conjecture. ~ Joshua Brakensiek, Marijn Heule, John Mackey, David Narvaez. ~ #ATP #SAT_Solver #Math
- Monoidal catamorphisms. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #CategoryTheory
- Free Math Textbooks. #Math
- The power of IO in Haskell. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
- Training our agent with Haskell! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
- A Lean tactic for normalising ring expressions with exponents. ~ Anne Baanen. #ITP #LeanProver #Math
- Verified approximation algorithms. ~ Robin Eßmann, Tobias Nipkow, Simon Robillard. #ITP #IsabelleHOL
- Análisis de texto usando funciones de orden superior. ~ Emanuel Goette (@emanuelpeg). #Haskell #ProgramaciónFuncional
- Using Template Haskell to generate static data. ~ Andreas Klebinger. #Haskell #FunctionalProgramming
- Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis. ~ Grigory Devadze, Victor Magron, Stefan Streif. #ITP #MinLog #Math
- Basic optics: lenses, prisms, and traversals in Haskell. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
- Simple linear regression in one pass. ~ Daniel Brice (@fried_brice). #Haskell #FuncionalProgramming
- Solving algorithm challenges in Haskell: Anagrams. ~ Theofanis Despoudis (@nerdokto). #Haskell #FunctionalProgramming
- Lean 4. ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver
- Connected Papers: A visual tool to help researchers and practitioners find and explore academic papers. ~ @ConnectedPapers
- Linear types are merged in GHC. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- Proofs and computation with trees. ~ Boro Sitnikovski (@BSitnikovski). #Math #CompSci
- Mathematics in type theory. ~ Kevin Buzzard (@XenaProject). #Logic #Math #ITP #LeanProver
- Verified Isabelle/HOL tactic for the theory of bounded linear integer arithmeticl based on quantifier instantiation and SMT. ~ Rafael Sadykov , Mikhail Mandrykin. #ITP #IsabelleHOL #SMT
- An efficient normalisation procedure for linear temporal logic: Isabelle/HOL formalisation. ~ Salomon Sickert. #ITP #IsabelleHOL #Logic
- Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2. ~ David M. Russinoff. #ITP #ACL2
- Cauchy-Schwarz in ACL2(r) abstract vector spaces. ~ Carl Kwan, Yan Peng, Mark R. Greenstreet. #ITP #ACL2 #Math
- Quadratic extensions in ACL2. ~ Ruben Gamboa, John Cowles, Woodrow Gamboa. #ITP #ACL2 #Math
- Techniques for implementation of symbolically interpretable Haskell EDSLs. ~ Grigoriy Volkov. #Haskell #FunctionalProgramming
- Leibniz equality is isomorphic to Martin-Löf identity, parametrically. ~ Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany. #ITP #Agda #FunctionalProgramming
- Strongly typed system F in GHC. ~ Stephanie Weirich. #Haskell #FunctionalProgramming #Logic
- An introduction to parsing text in Haskell with Parsec. ~ Nick Chung. #Haskell #FunctionalProgramming
- The HLint match engine. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
- Rendering frozen lake with Gloss! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
- Haskell for a new decade. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
- Calculating correct compilers II (Return of the register machines). ~ Patrick Bahr, Graham Hutton. #Haskell #FuncionalProgramming
- Lucas’s theorem: Formalising generating function proofs. ~ Chelsea Edmonds. #ITP #IsabelleHOL #Math
- Ackermann’s function in iterative form: A subtle termination proof with Isabelle/HOL. ~ Lawrence Paulson. #ITP #IsabelleHOL
- Axiomatic architecture of scientific theories. ~ Andrei V. Rodin. #PhD_Thesis #Logic #Math
- A concise sequent calculus for teaching first-order logic. ~ Asta Halkjær From, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
- SErAPIS : A concept-oriented search engine for the Isabelle libraries based on natural language. ~ Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL
- Authenticated data structures as functors in Isabelle/HOL. ~ Andreas Lochbihler, Ognjen Marić. #ITP #IsabelleHOL
- A generic framework for verified compilers using Isabelle/HOL’s locales. ~ Martin Desharnais, Stefan Brunthaler. #ITP #IsabelleHOL
- Competitive programming in Haskell: vectors and 2D geometry. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- A mechanized proof of a textbook type unification algorithm. ~ Maycon Amaro, Rodrigo Ribeiro, André Rauber Du Bois. #ITP #Coq
- Reasoning about partial correctness assertions in Isabelle/HOL. ~ A.R. Martini. #ITP #IsabelleHOL
- Extensive infinite games and escalation, an exercice in Agda. ~ Pierre Lescanne. #ITP #Agda
- Animated logic: Correct functional conversion to conjunctive normal form. ~ Pedro Barroso, Mário Pereira, António Ravara. #Why3 #Logic
- Teaching interactive proofs to mathematicians. ~ M. Ayala-Rincón, T.A. de Lima. #ITP #PVS #Math
- Interactively proving mathematical theorems. ~ M. Ayala-Rincón et als. #Logic #Math #ITP #PVS
- Undergraduate mathematics in mathlib. #ITP #LeanProver #Math
- Formalization of ring theory in PVS (Isomorphism theorems, principal, prime and maximal ideals ,chinese remainder theorem). ~ T.A. de Lima, A L. Galdino, A. Borges Avelar, M. Ayala-Rincón. #ITP #PVS #Math
- Why we need structured proofs in mathematics. ~ M. Ayala-Rincón, G.F. Silva. #Logic #Math #ITP #PVS
- Lambda Calculus – step by step. ~ Helmut Brandl. #Logic #Math #CompSci #LambdaCalculus
- Programming with Lambda Calculus. ~ Helmut Brandl. #Logic #Math #CompSci #LambdaCalculus
- The quest for Artificial Intelligence (A history of ideas and achievements). ~ Nils J. Nilsson. #eBook #AI
- Teaching dependent type theory to 4 year olds via mathematics. ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver
- Deep generation of Coq lemma names using elaborated terms. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq
- El traje nuevo de la inteligencia artificial. ~ Ramon López de Mántaras. #IA
- Try these 4 languages from 4 corners of programming. ~ Saurabh Sharma (@itsjzt). #C #Smalltak #Clojure #Haskell
- Using Haskell in the Mission Control Domain. ~ Michael Oswald (@OswaldChocolate). #Haskell #FunctionalProgramming
- Splittable pseudo-random number generators in Haskell: random v1.1 and v1.2. ~ Leonhard Markert. #Haskell #FunctionalProgramming #Math
- Formalizing the soundness of the encoding methods of SAT-based model checking. ~ Daisuke Ishii, Saito Fujii. #ITP #Coq
- Teaching Lean what a group is (ignoring the fact that it actually already knows). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Competitive programming in Haskell: data representation and optimization, with cake. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Algorithm design with Haskell. ~ Jeremy Gibbons (@jer_gib). #Haskell #FunctionalProgramming