Esta entrada es una recopilación de lecturas compartidas, del 19 al 24 de enero, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
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.
1 Programación declarativa
1.1 Programación funcional con Haskell
- Haskell problems for a new decade. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
- For beginners. ~ Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
- Algebraic data types aren’t numbers on steroids. Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
- The Functor family: Profunctor. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming
- Nicer package organization with Stack! ~ James Bowen (@james_OWA). #Haskell #Stack
- Beautiful mutable values. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
- Folding lists. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
1.2 Programación funcional con Lisp
- Lisping at JPL. ~ Ron Garret. #Programming #CommonLisp
1.3 Programación lógica con Prolog
- Drawing Prolog search trees: A manual for teachers and students of logic programming. ~ Johan Bos. #Prolog #LogicProgramming
2 DAO: Demostración asistida por ordenador
2.1 DAO con Isabelle/HOL
- Towards an Isabelle Theory for distributed, interactive systems-the untimed case. ~ Jens Christoph Bürger et als. #ITP #IsabelleHOL
- Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. ~ Simon Foster, Jonathan Julián Huerta y Munive, and Georg Struth. #ITP #IsabelleHOL
- Formal specification of a security framework for smart contracts. ~ M. Mandrykin et als. #ITP #IsabelleHOL
- Mersenne primes and the Lucas–Lehmer test in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Proof pearl: Braun trees. ~ Tobias Nipkow. #ITP #IsabelleHOL
2.2 DAO con Coq
- A Coq formalization of Lebesgue integration of nonnegative functions. ~ Sylvie Boldo et als. #ITP #Coq #Math
- SMTCoq: Coq automation and its application to formal mathematics. ~ Chantal Keller. #ITP #Coq #SMT #Math
- Undecidability of higher-order unification formalised in Coq. ~ Simon Spies. #ITP #Coq
- A functional proof pearl: Inverting the Ackermann heirarchy. ~ Linh Tran. #ITP #Coq
- Verified programming of Turing machines in Coq. ~ Fabian Kunze. #ITP #Coq
2.3 DAO con Lean
- Tabled typeclass resolution. ~ D. Selsam, S. Ullrich, L. de Moura. #ITP #LeanProver
2.4 DAO con Agda
- Coinductive formalization of SECD machine in Agda. ~ Adam Krupička. #MsC_Thesis #ITP #Agda
- Formalizing π-calculus in Guarded Cubical Agda. ~ Niccolò Veltri, Andrea Vezzosi. #ITP #Agda
- Three equivalent ordinal notation systems in cubical Agda. ~ Fredrick Nordvall Forsberg. #ITP #Agda #Math
2.5 DAO en general
- The future of Mathematics? ~ Kevin Buzzard. #Math #ITP
- Metamath Zero (or: how to verify a verifier). ~ Mario Carneiro. #ITP #MetamathZero
- First-order theorem (dis)proving for reachability problems in verification and experimental mathematics. ~ Alexei Lisitsa. #ATP #Prover9 #Mace4 #Math
3 Lógica
- Crash course on higher-order logic, type theory, etc. ~ Theodore Sider. #Logic via @RrrichardZach
- A modern perspective on type theory: From its origins until today. ~ Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. #eBook #TypeTheory