Lecturas compartidas el 17 de marzo de 2024

#ATP #CurryHoward #FunctionalProgramming #Haskell #ILP #ITP #LambdaCalculus #Lean4 #Logic #LogicProgramming #Math #Programming #Python

Buenos días

Las lecturas compartidas en Mastodon el 17 de marzo de 2024 son

• Lecturas compartidas el 16 de marzo de 2024. #Coq #FormalVerification #ILP #ITP #IsabelleHOL #Lean4 #LogicProgramming #SMT #cvc5

• Libro "Calculemus (Demostraciones con Lean4)" (versión 16-mar-24). #ITP #LeanProver #Lean4 #Matemáticas

• #Exercitium: Reconocimiento de potencias de 4. #Haskell #Python #Matemáticas

• A study on actions for atomic logics. ~ Raül Espejo-Boix. #ITP #Coq #Logic

• A bargain for mergesorts (functional pearl) – How to prove your mergesort correct and stable, almost for free. ~ Cyril Cohen, Kazuhiko Sakaguchi. #ITP #Coq

• Binomial tabulation: A short story. ~ Hsiang-Shang Ko, Shin-Cheng Mu, Jeremy Gibbons. #Haskell #FunctionalProgramming

• Building my own HTTP server in Haskell. #Haskell #FunctionalProgramming

• Reification, Curry-Howard correspondence, and didactical consequences. ~ Reinhard Oldenburg. #CurryHoward #FunctionalProgramming #LambdaCalculus

• Logic and logic programming. ~ J. A. Robinson (1992). #Logic #LogicProgramming #ATP

• Computer programming as an art. ~ Donald E. Knuth (1974). #Programming

• Scientific knowledge discovery using inductive logic programming. ~ Stephen Muggleton (1999). #ILP

• "The rest of the world disappears": Claire Voisin on mathematical creativity (The recipient of the 2024 Crafoord Prize in Mathematics discusses math as art, math as language, and math as abstract thought). ~ Jordana Cepelewicz (@jordanacep). #Math

También están en GitHub.

Saludos, José A.

---

"La mejor cura para el cuerpo es una mente tranquila." ~ Napoleón Bonaparte (1769-1821).