Resumen de lecturas compartidas durante abril de 2021
Esta entrada es una recopilación de lecturas compartidas, durante abril de 2021, 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.
- Trakhtenbrot’s theorem in Coq: Finite model theory through the constructive lens. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic #Math
- Topos: Programming language which can treat set and topology. #Haskell #FunctionalProgramming #Math
- Announcing Ema – Static sites in Haskell. ~ Sridhar Ratnakumar. #Haskell #FunctionalProgramming
- Introduce BIO: A simple streaming abstraction. ~ Dong Han. #Haskell #FunctionalProgramming
- We are happy being poor: El problema de Erdös-Faber-Lovász. ~ Juan Arias de Reyna. #Matemáticas
- A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
- Verified approximation algorithms. ~ Robin Eßmann, Tobias Nipkow, Simon Robillard. #ITP #IsabelleHOL #Algorithms
- Formalizations of the Church-Rosser theorem in Agda. ~ Andrea Laretto. #ITP #Agda
- Learning from Łukasiewicz and Meredith: Investigations into proof structures (Extended version). ~ Christoph Wernhard, Wolfgang Bibel. #ATP #Prover9 #Logic
- Haskell tutorial: Get started with functional programming. ~ Ryan Thelin. #Haskell #FunctionalProgramming
- Mathematics in the computer. ~ Mario Carneiro. #Math #ITP #LeanProver #Metamath #Metamath_Zero
- A verified decision procedure for orders in Isabelle/HOL. ~ Lukas Stevens, Tobias Nipkow. #ITP #IsabelleHOL #Logic #Math
- Gale-Stewart games (in Isabelle/HOL). ~ Sebastiaan Joosten. #ITP #IsabelleHOL
- Induction and collection up to definable elements: calibrating the strength of parameter-free Δn-minimization. ~ Andrés Cordón. #Logic #Math
- Lógica de programação funcional: Programe em Hope. ~ José Augusto N. G. Manzano, José A. Alonso. #Hope #FunctionalProgramming
- Código fonte do livro “Lógica de programação funcional: Programe em Hope”. ~ José Augusto N. G. Manzano. #Hope #FunctionalProgramming
- Isabelle’s metalogic: Formalization and proof checker. ~ Tobias Nipkow, Simon Roßkopf. #ITP #IsabelleHOL #Logic
- Mathematical structures in dependent type theory. ~ Assia Mahboubi. #ITP #Coq #Math
- Balancing the formal and the informal in user-centred design. ~ M.D. Harrison, P. Masci, J.C. Campos. #ITP #PVS
- A satisfying result. ~ Don Monroe.t#.YIeLaVxXfk0.twitter #Math #CompSci #SATSolvers
- El producto de matrices, en pos de una meta mítica. ~ Kevin Hartnett. #Matemáticas #Computación
- A formalised theorem in the partition calculus. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
- The BKR decision procedure for univariate real arithmetic (in Isabelle/HOL). ~ Katherine Cordwell, Yong Kiam Tan, André Platzer. #ITP #IsabelleHOL #Math
- Grandes ideas de la Filosofía: Lógica. #Lógica
- Formalization in Lean of IMO 2001 Q2. ~ Tian Chen. #ITP #LeanProver #Math #IMO
- Homotopy Type Theory in Isabelle. ~ Joshua Chen. #ITP #IsabelleHOL #HoTT
- Formal verification of pattern matching analyses. ~ Henning Dieterichs. #ITP #LeanProver
- Modeling and proving in computational type theory using the Coq proof assistant. ~ Gert Smolka. #eBook #ITP #Coq
- Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie. ~ Diane Gallois-Wong. #ITP #Coq #Math
- Logic for exact real arithmetic. ~ Helmut Schwichtenberg, Franziskus Wiesnet. #ITP #MinLog #Haskell
- Induction on equality. #Logic #Math #CompSci
- Ackermann’s function in iterative form: A proof assistant experiment. ~ Lawrence C Paulson. #ITP #IsabelleHOL
- Of function instances and abstract syntax. ~ Daniel Brice. #Haskell #FunctionalProgramming
- Type families in Haskell: The definitive guide. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
- What I wish somebody told me when I was learning Haskell. ~ Evgeny Poberezkin. #Haskell #FunctionalProgramming
- 15 graphs you need to see to understand AI in 2021. ~ Eliza Strickland. #AI
- A practical difference between Props and Types in Lean. ~ Mathieu Guay-Paquet. #ITP #LeanProver
- Product of segments of chords in Lean. ~ Manuel Candales. #ITP #LeanProver #Math
- The end of history for programming. ~ Gabriel Gonzalez. #Programming
- Simple type theory is not too simple: Grothendieck’s schemes without dependent types. ~ Anthony Bordg, Lawrence Paulson, Wenda Li. #ITP #IsabelleHOL #Math
- Sokoban implementation in Lean for proving solvability / unsolvability. ~ Miroslav Olšák. #ITP #LeanProver
- Continued fractions: Haskell, equational reasoning, property testing, and rewrite rules in action. ~ Chris Smith. #Haskell #FunctionalProgramming
- A random tour of typeclass in Haskell. ~ Ong Yi Ren. #Haskell #FunctionalProgramming
- Writing technical documentation with Emacs. #Emacs #OrgMode
- Induction on equality. ~ Kevin Buzzard. #ITP #LeanProver #Math
- A Coq formalization of Lebesgue integration of nonnegative functions. ~ Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero. #ITP #Coq #Math
- A secure and formally verified Linux KVM hypervisor. ~ Shih-Wei Li, Xupeng Li, Ronghui Gu, Jason Nieh, John Zhuang Hui. #ITP #Coq
- Machine-checked ZKP for NP-relations: Formally verified security proofs and implementations of MPC-in-the-head. ~ José Carlos Bacelar Almeida et als. #EasyCrypt
- EasyCrypt: Computer-aided cryptographic proofs. #EasyCrypt
- EasyCrypt: A tutorial. ~ Gilles Barthe et als. #EasyCrypt
- Online machine learning techniques for Coq: A comparison. ~ Liao Zhang, Lasse Blaauwbroek, Bartosz Piotrowski, Prokop Černý, Cezary Kaliszyk, Josef Urban. #ITP #Coq #MachineLearning
- Balanced Academic Curriculum: Looking for an optimal solution with metaheuristics and functional programming. ~ José Miguel Rubio, Cristian Vidal-Silva, Luis Carter, Miguel Tupac-Yupanqui. #Haskell #FunctionalProgramming
- Poltergeist types. ~ G. Allais. #Haskell #FunctionalProgramming
- Functional flocks. ~ Eddie Jones. #Haskell #FunctionalProgramming
- Checking for uncheckable: optional constraints. #Haskell #FunctionalProgramming
- Type theory. ~ Thierry Coquand. #TypeTheory
- More on types, typeclasses and the foldable typeclass. ~ Marty Stumpf. #Haskell #FunctionalProgramming
- The movement principle. ~ Chris Done. #Haskell #FunctionalProgramming
- Arrows, through a different lens. ~ Juan Raphael Diaz Simões. #Haskell #FunctionalProgramming
- Ad-hoc interpreters with capability. ~ Gaël Deest, Andreas Herrmann. #Haskell #FunctionalProgramming
- Lisp & the Web (Introductory reference guide to creating Web applications with Common Lisp & Google Compute Engine). ~ Ashok Khanna. #CommonLisp #Programming
- Mathematician disproves 80-year-old algebra conjecture. ~ Erica Klarreich. #Math
- Formalization in Lean of IMO 1977 Q6. ~ Tian Chen. #ITP #LeanProver #Math
- Heron’s Formula (in Lean). ~ Matt Kempster. #ITP #LeanProver #Math
- ¿Para qué sirven las matemáticas? ~ Marta Macho Stadler. #Matemáticas
- Topological semantics for paraconsistent and paracomplete logics in Isabelle/HOL. ~ David Fuenmayor. #ITP #IsabelleHOL #Logic
- The working programmer’s guide to setting up Haskell projects. ~ Jonas Carpay. #Haskell #FunctionalProgramming
- Things I wish someone had explained about functional programming (Part 1: Faulty assumptions). ~ James Sinclair. #FunctionalProgramming
- Things I wish someone had explained about functional programming (Part 2: Algebraic structures). ~ James Sinclair. #FunctionalProgramming
- Things I wish someone had explained about functional programming (Part 3: Type classes). ~ James Sinclair. #FunctionalProgramming
- Things I wish someone had explained about functional programming (Part 4: Algebraic data types). ~ James Sinclair. #FunctionalProgramming
- Generative art using Haskell. ~ David Luposchainsky. #Haskell #FunctionalProgramming
- Programar es de pobres: por qué el mundo del ‘software’ está roto en España. ~ Eduardo Manchón. #Programación #Informática
- Intuitionistic tautology (
itauto
) decision procedure in Lean. ~ Mario Carneiro. #ITP #LeanProver #Logic - First-order natural deduction in Agda. ~ Louis Warren. #ITP #Agda #Logic
- The Dao of functional programming. ~ Bartosz Milewski. #Haskell #FunctionalProgramming #CategoryTheory
- The beauty of programming. ~ Linus Torvalds. #Programming
- Gnus Emacs as email client in IMAP with ProtonMail. ~ Joseph Vidal-Rosset. #Emacs #ProtonMail
- Products and sums, named and anonymous. ~ Ömer Sinan Ağacan. #Haskell #FunctionalProgramming
- Connecting constructive notions of ordinals in Homotopy Type Theory. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #Logic #Math #HoTT
- Propuesta de enseñanza de la formalización de la Matemática utilizando un asistente de pruebas en estudiantes de la Licenciatura en Ciencias de la Computación. ~ Daniel Severın, Alejandro Hernández. #ITP #Coq
- Formalization in Lean of IMO 2008 Q3. ~ Manuel Candales. #ITP #LeanProver #Math
- NaturalProofs: Mathematical theorem proving in natural language. ~ Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, Kyunghyun Cho. #ATP #MachineLearning
- Type theory from the perspective of Artificial Intelligence. ~ David McAllester. #TypeTheory #AI
- A review of formal methods applied to machine learning. ~ Caterina Urban, Antoine Miné. #MachineLearning #FormalMethods
- Prolog meta-interpreters. ~ Markus Triska. #Prolog #LogicProgramming
- Grothendieck’s Schemes in Algebraic Geometry. ~ Anthony Bordg, Lawrence Paulson, Wenda Li. #ITP #IsabelleHOL #Math
- Continued fractions in Haskell. ~ Chris Smith.l#P7oZc6pbWBK6wRaBBMm0goA #Haskell #FunctionalProgramming #Math
- Algorithmic puzzle: Continuous increasing subsequences. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
- How to replace Proxy with AllowAmbiguousTypes. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming
- Formalization in Lean of IMO 2008 Q4. ~ Manuel Candales. #ITP #LeanProver #Math
- Giml’s type inference engine. ~ Gil Mizrahi. #Haskell #FunctionalProgramming
- Scrabbλe: A one- or two-player implementation of Scrabble for teaching functional programming. ~ Jim Burton. #eBook #Haskell #FunctionalProgramming
- Intuitionistic NF Set Theory. ~ Michael Beeson. #Logic #Math #ITP #LeanProver
- Girard’s paradox. ~ Mario Carneiro. #ITP #LeanProver #Logic #Math
- Formalization in Lean of IMO 2005 Q3. ~ Manuel Candales. #ITP #LeanProver #Math
- Formalization in Lean of IMO 2008 Q2. ~ Manuel Candales. #ITP #LeanProver #Math
- Formalization in Lean of IMO 2011 Q5. ~ Alain Verberkmoes. #ITP #LeanProver #Math
- Capturing number theory in Haskell. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming #Math
- Auto build and publish emacs org configuration as a website. ~ Erick Navarro. #Emacs
- Division by zero in Logic and Computing. ~ Jan Bergstra. #Logic #Math #CompSci
- Induction, and inductive types. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Doing mathematics with simple types: Infinitary combinatorics in Isabelle/HOL. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
- An evaluation of the Archive of Formal Proofs. ~ Carlin MacKenzie, Jacques Fleuriot, James Vaughan. #ITP #IsabelleHOL
- Default exception handler in Haskell. ~ Taylor Fausak. #Haskell #FunctionalProgramming
- Emacs org-mode examples and cookbook. ~ Eric H. Neilsen, Jr. #Emacs
- ProverX: Rewriting and extending Prover9. ~ Ivo Robert. #PhDThesis #ATP #Prover9
- SSProve: A foundational framework for modular cryptographic proofs in Coq. ~ Carmine Abate et als. #ITP #Coq
- Código fonte do livro “Lógica de programação funcional: Pense em Hope”. ~ José Augusto N. G. Manzano. #Hope #FunctionalProgramming
- Dependent stringly-typed programming. ~ @anormalform. #Agda #FunctionalProgramming #ITP
- Designing command line interfaces in Haskell. ~ Stephan Schiffels. #Haskell #FunctionalProgramming
- Category theory illustrated. ~ Boris Marinov. #CategoryTheory
- #SEP: Category theory. ~ Jean-Pierre Marquis. #CategoryTheory #Logic #Math