Resumen de lecturas compartidas del 19 al 24 de enero de 2020
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