Resumen de lecturas compartidas del 1 al 11 de enero de 2020
Esta entrada es una recopilación de lecturas compartidas, del 1 al 11 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 (#FunctionalProgramming #Haskell)
- Defunctionalization: Everybody does it, nobody talks about it. ~ James Koppel. #FunctionalProgramming #Haskell
- Gain confidence with Haskell! ~ Brandon Chinn. #Haskell #FunctionalProgramming
- Generating small binaries in Haskell. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming
- Kind inference for datatypes. ~ N. Xie, R.A. Eisenberg, B.C.d.S. Oliveira. #Haskell #FunctionalProgramming
- Haskell language extension taxonomy. ~ Doug Beardsley. #Haskell #FunctionalProgramming
- Linear algebra of programming – Algebraic matrices in Haskell. ~ Armando Santos (@_bolt12). #Haskell #FunctionalProgramming #Math
- Selective applicative functors & probabilities. ~ Armando Santos (@_bolt12). #MSc_Thesis #Haskell #FunctionalProgramming #Math
- Collections of papers and books about Haskell, type theory and category theory. ~ Saurabh Kukade. #Haskell #TypeTheory #CategoryTheory
- Learn Haskell now! ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming
- Mandelbrot & Lovejoy’s rain fractals. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming
- Organizing our package! ~ James Bowen (@james_OWA). #Haskell #Cabal #FunctionalProgramming
- Programming with categories. ~ Peter Smith. #Programming #CategoryTheory
- The simple Haskell initiative. #Haskell #FunctionalProgramming
1.2 Programación lógica con Prolog (#LogicProgramming #Prolog)
- On correctness of an n queens program. ~ Włodzimierz Drabent. #LogicProgramming #Prolog #Verification
2 DAO: Demostración asistida por ordenador (#ITP)
2.1 DAO con Isabelle/HOL
- Proof pearl: Braun trees. ~ T. Nipkow, T. Sewell. #ITP #IsabelleHOL
- Bicategories in Isabelle/HOL ~ Eugene W. Stark. #ITP #IsabelleHOL
- Gauss sums and the Pólya–Vinogradov inequality. ~ R. Raya, M. Eberl. #ITP #IsabelleHOL #Math
- Formalizing a Seligman-style tableau system for hybrid logic in Isabelle/HOL. ~ Asta Halkjær. #ITP #IsabelleHOL #Logic
- Skip lists in Isabelle/HOL. ~ M.W. Haslbeck, M. Eberl. #ITP #IsabelleHOL
- The irrationality of ζ(3) in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
2.2 DAO con Coq
- A formal proof of the irrationality of ζ(3). ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math
- Lean versus Coq: The cultural chasm. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq
- LF+ in Coq for “fast and loose” reasoning. ~ F. Alessi. #ITP #Coq
2.3 DAO con Lean
- Lean versus Coq: The cultural chasm. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq
- Lean 3 for hackers. ~ J Kenneth King. #LeanProver #FunctionalProgramming
2.4 DAO con HOL
- Design and verification of parity checking circuit using HOL4 theorem proving. ~ E. Deni̇z, K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4
- Introduction to HOL4 theorem prover. ~ K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4
- Formalizing modal logic in HOL. ~ Yiming Xu. #PhD_Thesis #ITP #HOL #Logic
- Proof searching in HOL4 with genetic algorithm. ~ M.Z. Nawaz et als #ITP #HOL4
3 Lógica (#Logic)
- Constructive reverse mathematics. ~ Hannes Diener. #Logic #Math
- Different problems, common threads: Computing the difficulty of mathematical problems. ~ Karen Lange. #Logic #Math #CompSci
- Motivated proofs: what they are, why they matter and how to write them. ~ Rebecca Lea Morris. #Logic #Math