Resumen de lecturas compartidas durante febrero de 2021

Esta entrada es una recopilación de lecturas compartidas, durante febrero 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.

• Proof verification technology and elementary physics. ~ Ernest Davis. #FormalVerification #Physics
• How I use Dante. #Haskell #FunctionalProgramming #Emacs
• Computational logic in the first semester of computer science: An experience report. ~ David M. Cerna et als. #Logic #CompSci
• Certifying choreography compilation. ~ Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti. #ITP #Coq
• Formalising mathematics: workshop 6 (limits). ~ Kevin Buzzard. #ITP #LeanProver #Math
• A verified imperative implementation of B-trees (in Isabelle/HOL). ~ Niels Mündle. #ITP #IsabelleHOL
• Totality. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
• Evaluación perezosa en Python. Parte 4: Evaluación perezosa avanzada. ~ Chema Cortés. #Python #Programación
• Formal Puiseux series (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• PureScript and Haskell. ~ Drew Olson. #Haskell #PureScript #FunctionalProgramming
• The Burali-Forti argument in HoTT/UF. ~ Martin Escardo. #Logic #Math #HoTT
• Rerecorded introduction to the Algebra of Programming research group. ~ Jeremy Gibbons. #CompSci #Haskell #FunctionalProgramming
• Course: Principles of Programming Languages. ~ Gregor Richards. #Programming #Haskell #Prolog #Pascal #Smalltalk #Erlang #C
• Knowledge graphs. ~ Claudio Gutierrez, Juan F. Sequeda. #AI #Logic #CompSci
• The decline of computers as a general purpose technology. ~ Neil C. Thompson, Svenja Spanuth. #CompSci
• 50 years of Pascal. ~ Niklaus Wirth. #Pascal #Programming #CompSci
• Inductive logic programming at 30. ~ Andrew Cropper, Sebastijan Dumančić, Richard Evans, Stephen H. Muggleton. #ILP #LogicProgramming #MachineLearning
• A formal proof of safegcd bounds. ~ Russell O’Connor, Andrew Poelstra. #ITP #Coq
• Formalized Haar measure. ~ Floris van Doorn. #ITP #LeanProver #Math
• A variant of Wagner’s theorem based on combinatorial hypermaps. ~ Christian Doczkal. #ITP #Coq #Math
• IPDL: A simple framework for formally verifying distributed cryptographic protocols. ~ Greg Morrisett, Elaine Shi, Kristina Sojakova, Xiong Fan, Joshua Gancher. #ITP #Coq
• Category theory as an excuse to learn type theory. ~ Eduardo Ochs, Selana Ochs. #CategoryTheory #TypeTheory
• Introducción al sistema de tipos en Haskell. ~ Manuel Soto. #Haskell #FunctionalProgramming
• Type classes: de aprendiz a maestro. ~ Alejandro Serrano. #Haskell #FunctionalProgramming
• Formalizing groups in type theory. ~ Farida Kachapova. #Logic #Math #ITP
• Formalising mathematics: workshop 5 (filters). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Filter (mathematics). ~ Wikipedia. #Math
• Filters in topology. ~ Wikipedia. #Math
• Set theory (in “The Stanford Encyclopedia of Philosophy”). ~ Joan Bagaria. #Logic #Math
• Set theory. ~ Joan Bagaria. #Logic #Math
• Models of set theory. ~ Joan Bagaria. #Logic #Math #Set_theory
• The mathematics of boolean algebra (in “The Stanford Encyclopedia of Philosophy”). ~ J. Donald Monk. #Logic #Math
• Reflections on using Haskell for my startup. ~ Alistair Burrowes. #Haskell #FunctionalProgramming
• Formalizing relations in type theory. ~ Farida Kachapova. #Logic #Math
• Course: Interactive theorem proving and applications. ~ Burkhart Wolff. #ITP #IsabelleHOL
• #SEP: Algebra (in “The Stanford Encyclopedia of Philosophy”). ~ Vaughan Pratt. #Math
• Evaluación perezosa en Python. Parte 3: Cachés y memoización. ~ Chema Cortés. #Python #Programación
• Patterns, predictions, and actions: A story about machine learning. ~ Moritz Hardt, Benjamin Recht. #eBook #MachineLearning
• A geometric view of the square root algorithm. ~ A. Grzesina. #Math #Algorithms
• Study of Isabelle/HOL on formal algorithm analysis and code generation. ~ Haitao Wang, Lihua Song. #ITP #IsabelleHOL
• Cantor’s theorem without reductio ad absurdum. ~ Christoph Benzmüller, David Fuenmayor. #ITP #IsabelleHOL #Logic #Math
• #SEP: Fallacies. ~ Hans Hansen. #Logic
• #SEP: The algebra of logic tradition. ~ Stanley Burris, Javier Legris. #Logic
• Kruskal’s algorithm implemented in Clojure. ~ Atabey Kaygun. #Clojure #Algorithms
• Kruskal’s algorithm in Common Lisp. ~ Atabey Kaygun. #CommonLisp #Algorithms
• Value-oriented legal argumentation in Isabelle/HOL. ~ Christoph Benzmüller, David Fuenmayor. #ITP #IsabelleHOL
• Unsolvability of the quintic formalized in dependent type theory. ~ Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. #ITP #Coq #Math
• Machine-checked computer-aided mathematics. ~ Assia Mahboubi. #ITP #Coq #Math
• A study of continuous vector representations for theorem proving. ~ StanisŁaw PurgaŁ, Julian Parsert, Cezary Kaliszyk. #ATP #MachineLearning
• Decades-old computer science conjecture solved in two pages. ~ Erica Klarreich. #Math #CompSci
• Hall’s Marriage Theorem in Lean. ~ Alena Gusakov, Bhavik Mehta, Kyle Miller. #ITP #LeanProver #Math
• Liouville’s theorem in Lean. ~ Jujian Zhang. #ITP #LeanProver #Math
• Formalization in Lean of IMO (International Mathematical Olympiads) 1987, Q1. ~ Yury Kudryashov. #ITP #LeanProver #Math
• A formal proof of modal completeness for provability logic. ~ Marco Maggesi, Cosimo Perini Brogi. #ITP #HOL_Light #Logic
• HaskellRank: HackerRank in Haskell. ~ @tsoding. #Haskell #FunctionalProgramming
• Evaluación perezosa en Python – Parte 2: Secuencias infinitas. ~ Chema Cortés. #Python #Programming
• The laws of large numbers (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Formalising mathematics: workshop 4 (topology). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Learning equational theorem proving. ~ Jelle Piepenbrock, Tom Heskes, Mikoláš Janota, Josef Urban. #ATP #MachineLearning
• An algebra of properties of binary relations. ~ Jochen Burghardt. #Logic #Math #ATP #Eprover
• IMO 2013 Q1 in Lean. ~ David Renshaw. #ITP #LeanProver #Math
• Certifying differential equation solutions from computer algebra systems in Isabelle/HOL. ~ Thomas Hickman, Christian Pardillo Laursen, Simon Foster. #ITP #IsabelleHOL #Math
• Vampire with a brain is a good ITP hammer. ~ Martin Suda. #Vampire #ATP #ITP #MachineLearning
• Modelling puzzles in First Order Logic. ~ Adrian Groza. #Logic #ATP #Prover9
• Evaluación perezosa en Python. Parte 1: Introducción a la evaluación perezosa. ~ Chema Cortés. #Python #Programming
• The Ramanujan Machine is an intellectual fraud. #AI #Math
• A verified decision procedure for univariate real arithmetic with the BKR algorithm. ~ Katherine Cordwell, Yong Kiam Tan, André Platzer. #ITP #IsabelleHOL #Math
• A formal proof of the independence of the continuum hypothesis. ~ Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Logic #Math
• Automated propositional sequent proofs in your browser with Tau Prolog. Philip Zucker. #ATP #Logic #Prolog #LogicProgramming
• Emacs and org-mode for reproducible research. (Organize your research in plain text!). ~ Thibault Lestang. #Emacs #OrgMode
• Writing the Emacs configuration script in org-mode: a simple example of literate programming. ~ Hsin-Hao Yu. #Emacs
• Folds are constructor substitution. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming
• Model-based testing of networked applications. ~ Yishuai Li, Benjamin C. Pierce, Steve Zdancewic. #ITP #Coq
• Verifying the Hashgraph consensus algorithm. ~ Karl Crary. #ITP #Coq
• AI maths whiz creates tough new problems for humans to solve. ~ Davide Castelvecchi. #AI #Math #ITP
• The Ramanujan Machine (an algorithmic approach to discover new mathematical conjectures). #AI #Math
• The Ramanujan Machine: automatically generated conjectures on fundamental constants. ~ Gal Raayoni, Shahar Gottlieb, George Pisha, Yoav Harris, Yahel Manor, Uri Mendlovic, Doron Haviv, Yaron Hadad, Ido Kaminer. #AI #Math
• GHC reading guide (Exploring entrances and mental models to the source code). ~ Takenobu Tani. #Haskell #FunctionalProgramming
• Computer Science by Example. #CompSci #Programming
• Formalising a Turing-complete choreographic language in Coq. ~ Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti. #ITP #Coq
• A formalization of Dedekind domains and class groups of global fields. ~ Anne Baanen, Sander R. Dahmen, Ashvni Narayanan, Filippo A. E. Nuccio Mortarino Majno di Capriglio. #ITP #LeanProver #Math
• New random interface. ~ Alexey Kuleshevich. #Haskell #FunctionalProgramming
• Formalising mathematics: Workshop 3 (Limits of sequences). ~ Kevin Buzzard. #ITP #LeanProver #Math
• What is a filter? How some computer scientists think about limits. ~ Kevin Buzzard. #ITP #LeanProver #Math
• What is a uniform space? How some computer scientists think about completions. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Superconnected left quasigroups and involutory quandles. ~ Marco Bonatto. #ATP #Prover9 #Math
• Haskell’s @ symbol – Type application. ~ Zac Wood. #Haskell #FunctionalProgramming
• The working programmer’s guide to setting up Haskell projects. ~ Jonas Carpay. #Haskell #FunctionalProgramming
• El cifrado de los monjes cistercienses: de 0000 a 9999 con «símbolos raros». ~ @Alvy. #Matemáticas
• Tarski’s parallel postulate implies the 5th postulate of Euclid, the postulate of Playfair and the original parallel postulate of Euclid. ~ Roland Coghetto. #ITP #IsabelleHOL #Math
• Solution to the xkcd Blue Eyes puzzle (in Isabelle/HOL). ~ Jakub Kądziołka. #ITP #IsabelleHOL
• Proving me wrong (How QuickCheck destroyed my favourite theory). ~ Thomas Mahler. #Haskell #FunctionalProgramming #QuickCheck
• Verification of dynamic bisimulation theorems in Coq. ~ R Fervari, F Trucco, B Ziliani. #ITP #Coq
• Tutorial on implementing Hoare logic for imperative programs in Haskell. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
• Deriving monadic quicksort (Declarative Pearl). ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming