Readings on computational logic, interactive theorem proving and functional programming

This repository is a collection of readings shared on Twitter about computational logic, interactive theorem proving and functional programming.

The collection is sorted by the date of its publication on Twitter.

At the end of each article you will find tags related to the systems it uses or its content.

Content

Readings of the year 2022

January 2022

19-Jan-22

Mathematical problems. ~ David Hilbert (1900). #Math #CompSci
Mechanizing matching logic in Coq. ~ Péter Bereczky, Xiaohong Chen, Dániel Horpácsi, Tamás Bálint Mizsei, Lucas Peña. #ITP #Coq #Logic
Interactive teaching of programming language theory with a proof assistant. ~ Péter Bereczky, István Donkó, Dániel Horpácsi, Ambrus Kaposi, Dávid János Németh. #ITP #Coq

18-Jan-22

The complexity of theorem-proving procedures. ~ Stephen A. Cook (1971). #CompSci #Logic #Math
[[https://youtu.be/mbjeniWFqcM ][[Formalising math 2022] Section 02: the reals, solutions to sheet 1 (“norm_num”)]]. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic #Math
[[https://youtu.be/fuNF7lVouWs][[Formalising math 2022] Section 02: the reals, solutions to sheet 2 (“ring”)]]. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic #Math
[[https://youtu.be/jCQ1_zXo5GI][[Formalising math 2022] Section 02: the reals, solutions to sheet 3 (limits of sequences)]]. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic #Math
[[https://youtu.be/rf-lie7U04Q][[Haskell beginners 2022]: Lecture 2 about pattern matching, algebraic data types, parametric polymorphism and function composition]]. ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
A history of Artificial Intelligence. ~ S. Hussain Ather (@SHussainAther). #AI #History
Automated Theorem Proving. ~ Arnon Avron, Mooly Sagiv. #ATP #Logic #CompSci
Certifying derivation of state machines from coroutines. ~ Mirai Ikebuchi, Andres Erbsen, Adam Chlipala. #ITP #Coq
DSLsofMath Week 1: Extra lecture on Haskell, part 1/3. ~ Patrik Jansson (@patrikja). #Haskell #FunctionalProgramming
DSLsofMath Week 1: Extra lecture on Haskell, part 2/3. ~ Patrik Jansson (@patrikja). #Haskell #FunctionalProgramming
DSLsofMath Week 1: Extra lecture on Haskell, part 3/3. ~ Patrik Jansson (@patrikja). #Haskell #FunctionalProgramming
DSLsofMath Week 1, Lecture 1, Part 1. ~ Patrik Jansson (@patrikja). #Haskell #FunctionalProgramming #Math
DSLsofMath Week 1, Lecture 1, Part 2. ~ Patrik Jansson (@patrikja). #Haskell #FunctionalProgramming #Math
Effective metatheory for type theory. ~ Philipp Georg Haselwarter. #PhD_Thesis #TypeTheory
Verified first-order monitoring with recursive rules. ~ Sheila Zingg, Sr̄dan Krstíc, Martin Raszyk, Joshua Schneider, Dmitriy Traytel. #ITP #IsabelleHOL
Computability and l²-Betti numbers. ~ Matthias Uschold. #MSc_Thesis #ITP #LeanProver

17-Jan-22

An axiomatic basis for computer programming. ~ C. A. R. Hoare (1969). #CompSci
A practical guide to writing tactics in Lean. ~ Daniel J. Velleman. #ITP #LeanProver
Lambda calculus: an Elm CLI. ~ James Carlson. #Elm #FunctionalProgramming #LambdaCalculus
From greek paradoxes to political paradoxes. ~ Moshe Y. Vardi (@vardi). #Logic
The design and use of QuickCheck. ~ Joe “begriffs” Nelson (2017). #Haskell #FunctionalProgramming
Formalising extremal graph theory, I. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
Transposing rows. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming

16-Jan-22

Recursive functions of symbolic expressions and their computation by machine. ~ John McCarthy (1960). #CompSci #Lisp
The foundations of arithmetic: a logico-mathematical enquiry into the concept of number. ~ Gottlob Frege (1884). #Logic #Math via @internetarchive
Die Grundlagen der Arithmetik: eine logisch mathematische Untersuchung über den Begriff der Zahl. ~ Gottlob Frege (1884). #Logic #Math via @internetarchive
SciLean: Framework for scientific computing written in Lean. ~ Tomas Skrivnan. #ITP #LeanProver #FunctionalProgramming #Math

15-Jan-22

Computing machinery and intelligence. ~ Alan Mathison Turing (1950). #CompSci #AI via @internetarchive
A treatise on algebra. ~ George Peacock (1830).
Logic and artificial intelligence. ~ Richmond Thomason (2018). #Logic #AI
Automated reasoning. ~ Frederic Portoraro (2019) #ATP #Logic #Math #CompSci
The emergence of first-order logic. ~ William Ewald (2018). #Logic #Math #History
The early development of set theory. ~ José Ferreirós (2020). #Logic #Math #SetTheory #History
The development of proof theory. ~ Jan von Plato (2014). #Logic #Math #History
“History of logic” (Encyclopedia Britannica). ~ Jaakko J. Hintikka, Paul Vincent Spade. #Logic #Math #CompSci #History
Proof assistants: History, ideas and future. ~ H. Geuvers (2009). #ITP #Logic #Math #CompSci #History
Twenty years of theorem proving for HOLs (Past, present and future). ~ Mike Gordon (2008). #Logic #CompSci #ITP
Delta dictionaries (Total and extensional finite maps in proof assistants). ~ Nick Collins. #ITP #Agda
Introduction to computation: Haskell, logic and automata. ~ Don Sannella, Michael Paul Fourman, Haoran Peng, Philip Wadler. #Haskell #FunctionalProgramming #Logic #CompSci
About that Reader trick. ~ Micah Cantor (@micah_cantor). #Haskell #FunctionalProgramming
Undefined values, or what do we get when we divide by zero? ~ Lawrence C. Paulson. #Logic #Math #ITPa
Explaining list folds (An easy explanation of the fold-left and fold-right functions). ~ Tony Morris (2013). #Haskell #FunctionalProgramming
Parse, don’t validate. ~ Alexis King (@lexi_lambda). #Haskell #FunctionalProgramming
Servant’s type-level domain specific language. ~ Brad Parker (@parkerbrads). #Haskell #FunctionalProgramming
Functor functors. ~ Benjamin Hodgson (2017). #Haskell #FunctionalProgramming
Providing an API for extensible-effects and monad transformers. ~ Ollie Charles (@acid2). #Haskell #FunctionalProgramming
Continuations all the way down. ~ T. Humphries./#/posts/2017/05/10/lambdajam-slides/index.html #Haskell #FunctionalProgramming
Applicative regular expressions using the free Alternative. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
Profunctors, arrows, & static analysis. Will Fancher (@ElvishJerricco). #Haskell #FunctionalProgramming
Haskell learning resource collection. ~ Jack Kelly. #Haskell #FunctionalProgramming

14-Jan-22

A symbolic analysis of relay and switching circuits. Claude Shannon (1938). #CompSci
Clojure & Datalog is Lisp & Prolog. ~ Kari Marttila. #Clojure #Datalog #Lisp #Prolog #FunctionalProgramming #LogicProgramming
[[https://youtu.be/UykGFDVfQNA][[London Learning Lean] Formalizing adèles and idèles]]. ~ María Inés de Frutos-Fernández. #ITP #LeanProver #Math
Formalising Lie algebras. ~ Oliver Nash. #ITP #LeanProver #Math
A practical guide to writing tactics in Lean. ~ Daniel J. Velleman. #ITP #LeanProver

13-Jan-22

On computable numbers, with an application to the Entscheidungsproblem. ~ Alan Mathison Turing (1936). #CompSci #Logic #Math
Building a consensus: A rectangle covering problem. ~ Richard S. Bird (2011). #Haskell #FunctionalProgramming
Can you solve it? Gödel’s incompleteness theorem (The proof that rocked maths). ~ Alex Bellos (@alexbellos). #Logic #Math).
10+ beautiful mathematical documentaries to make students love Math. ~ @abakcus #Math
Constructive theory of ordinals. ~ Thierry Coquand, Henri Lombardi, Stefan Neuwirth. #Logic #Math #SetTheory
A Lisp interpreter implemented in Conway’s Game of Life. ~ Hikaru Ikuta (@woodrush924). #Lisp #Programming
The role of functional programming in the organization of parallel computing. ~ Lidia V. Gorodnyaya. #FunctionalProgramming
Domain-Specific Languages of Mathematics: Presenting mathematical analysis using functional programming. ~ Cezar Ionescu, Patrik Jansson (2016). #Haskell #FunctionalProgramming #Math
Canonicity and normalization for type theory. ~ Thierry Coquand. #TypeTheory
Le point de vue constructif en mathématiques. ~ Henri Lombardi. #Logic #Math
Algèbre constructive. ~ Henri Lombardi. #Math
[[https://youtu.be/lubSFfj4B08][[Formalising math 2022] Section 01 Logic, solutions to sheet 4 (“and”)]]. ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Logic #Math
[[https://youtu.be/tQSA7x4AWD4][[Formalising math 2022] Section 01 Logic, solutions to sheet 5 (“iff”)]]. ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Logic #Math
[[https://youtu.be/Mwx9zkQM-Kk][[Formalising math 2022] Section 01 Logic, solutions to sheet 6 (“or”)]]. ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Logic #Math
“Group” theory. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming

12-Jan-22

An investigation of the laws of thought on which are founded the mathematical theories of logic and probabilities. ~ George Boole (1854). #Logic #Math
La machine de Turing (1/2). ~ Patrice Debrabant. #CompSci #Scratch
La préhistoire de l’informatique. ~ Bernard Ycart. #CompSci #History
Learning logic programs from noisy failures. ~ John Wahlig. #MSc_Thesis #ILP #MachineLearning #LogicProgramming
A simple formalization and proof for the mutilated chess board. ~ Lawrence C. Paulson (2001). #ITP #IsabelleHOL
Without loss of generality. ~ John Harrison (2013). #ITP #HOL_Light
Proving the obvious. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
Building partially static libraries with Cabal. ~ James Hobson. #Haskell #FunctionalProgramming
Learning programs by learning from failures. ~ Andrew Cropper, Rolf Morel (2020). #ILP #MachineLearning #LogicProgramming
Popper: an inductive logic programming (ILP) system. ~ Andrew Cropper et als. #ILP #MachineLearning #LogicProgramming #Prolog
Inductive logic programming at 30. ~ Andrew Cropper, Sebastijan Dumančić, Richard Evans, Stephen H. Muggleton. #ITP #MachineLearning #LogicProgramming
Learning logic programs through divide, constrain, and conquer. ~ Andrew Cropper. #ILP #MachineLearning #LogicProgramming
Inductive logic programming (Slides). ~ Andrew Cropper. #ILP #Logic #MachineLearning #LogicProgramming
ProbLog: A probabilistic Prolog and its application in link discovery. ~ Luc De Raedt, Angelika Kimmig, Hannu Toivonen (2007). #LogicProgramming #LogicProgramming
DeepProbLog: an extension of ProbLog that integrates probabilistic logic programming with deep learning by introducing the neural predicate. ~ Robin Manhaeve. #LogicProgramming #DeepLearning
Neural probabilistic logic. ~ Robin Manhaeve (Supervisor: Luc De Raedt). #PhD_Thesis #AI #DeepLearning #LogicProgramming #MachineLearning
Beneficial and harmful explanatory machine learning. ~ Lun Ai1, Stephen H. Muggleton, Céline Hocquette, Mark Gromowski, Ute Schmid. #ILP #MachineLearning #AI #XAI
Complete bottom-up predicate invention in meta-interpretive learning. ~ Céline Hocquette, Stephen H Muggleton. #ILP #MachineLearning #LogicProgramming
[[https://youtu.be/OZLfDQKbdFk][[Formalising math 2022] Section 01 Logic, solutions to sheet 1]]. ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Logic #Math
[[https://youtu.be/JTl6NHNxyDk][[Formalising math 2022] Section 01 Logic, solutions to sheet 2]]. ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Logic #Math
[[https://youtu.be/qDKtXrOy6CM][[Formalising math 2022] Section 01 Logic, solutions to sheet 3]]. ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Logic #Math

11-Jan-22

The true method. ~ Gottfried Wilhelm Leibniz (1677). #Logic #CompSci #AI #Knowledge_representation #Automated_reasoning
A Coq formalization of the Bochner integral. ~ Sylvie Boldo, François Clément, Louise Leclerc. #ITP #Coq #Math
The art of Lisp & writing. ~ Richard Gabriel (2003). #Lisp #Programming
Coq’s vibrant ecosystem for verification engineering. ~ Andrew W. Appel. #ITP #Coq
A formal foundation for symbolic evaluation with merging. ~ Sorawee Porncharoenwase, Luke Nelson, Xi Wang, Emina Torlak. #ITP #LeanProver
Verified online monitoring for metric temporal logic with lattice-based quantitative semantics. ~ Agnishom Chattopadhyay, Konstantinos Mamouras. #ITP #Coq #OCaml #FunctionalProgramming
WebSpec: Towards machine-checked analysis of browser security mechanisms. ~ Lorenzo Veronese, Benjamin Farinier, Mauro Tempesta, Marco Squarcina, Matteo Maffei. #ITP #Coq
Formalising mathematics: getting started (Video). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Formalising Mathematics (A course for mathematicians). ~ Kevin Buzzard (@XenaProject) #ITP #LeanProver #Math
Deriving efficient program transformations from rewrite rules. ~ John M. Li, Andrew W. Appel. #ITP #Coq
Functional correctness of C implementations of Dijkstra’s, Kruskal’s, and Prim’s algorithms. ~ Aquinas Hobor, Anshuman Mohan, Wei Xiang. #ITP #Coq
Demostración en una línea del teorema de Varignon. ~ Miguel Ángel Morales (@gaussianos). #Matemáticas

10-Jan-22

“Program development by stepwise refinement”. ~ Niklaus Wirth (1971). #CompSci
Dynamic programming in Haskell. ~ Amogh Rathore (@RathoreAmogh). #Haskell #FunctionalProgramming
Beatty’s theorem. ~ John D. Cook (@JohnDCook). #Math #Python
Pasado, presente y futuro de los lenguajes de programación. ~ Ricardo Peña Marí (2017). #Programación
Program / Proof. ~ Samuel Mimram. #Agda #FunctionalProgramming #ITP #Logic
Haskell Beginners 2022: Lecture 1 about Haskell and FP fundamentals. ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming

09-Jan-22

History of Lisp. ~ John McCarthy (1979). #Lisp #FunctionalProgramming
Three paradigms of Computer Science. ~ Amnon H. Eden (2007). #CompSci
The philosophy of computer languages. ~ Graham White (2004). #CompSci
Tutorial on good Lisp programming style. ~ Peter Norvig and Kent Pitman (1993). #Lisp #Programming
2021 - The Bottom Line. ~ Mathlib community. #ITP #LeanProver #Mathlib
Lenses to the left of me, Prisms to the right. ~ Bruno Gavranović (@bgavran3). #CategoryTheory #FunctionalProgramming #Haskell
Towards categorical foundations of learning. ~ Bruno Gavranović (@bgavran3). #CategoryTheory #DeepLearning
A neural network solves and generates mathematics problems by program synthesis: Calculus, differential equations, linear algebra, and more. ~ Iddo Drori et als. #MachineLearning #Math

08-Jan-22

A survey of symbolic logic. ~ Clarence Irving Lewis (1918). #Logic #Math
Preparando Emacs para trabajar con Clojure. ~ Notxor. #Emacs #Clojure #FunctionalProgramming
The paradox at the heart of mathematics: Gödel’s Incompleteness Theorem. ~ Marcus du Sautoy. #Logic #Math
Types in logic programming (An overview of type systems proposed for logic programming languages). ~ Wolfgang Witt. #LogicProgramming #TypeTheory #Mercury
Extracting certified Futhark code from Coq. ~ Kristian Knudsen Olesen. #BSc_Thesis #ITP #Coq
Practical heterogeneous unification for dependent type checking. ~ Víctor López Juan. #PhD_Thesis #ITP #Agda #FunctionalProgramming
The solutions to single-variable polynomials, implemented and verified in Lean. ~ Nicholas Dyson, Benedikt Ahrens, Jacopo Emmenegger. #ITP #LeanProver #Math
Explanation by automated reasoning using the Isabelle infrastructure framework. ~ Florian Kammüller. #ITP #IsabelleHOL #XAI #AI #MachineLearning
Pappus’s hexagon theorem in real projective plane. ~ Roland Coghetto. #ITP #Mizar #Math
Ascoli-Arzel`a theorem (in Mizar). ~ Hiroshi Yamazaki. #ITP #Mizar #Math
A comprehensive formalization of AADL with behavior annex. ~ Yu Tan, Yongwang Zhao, Dianfu Ma, and Xuejun Zhang. #ITP #IsabelleHOL
Machine checked properties of the Schulze method. ~ Mukesh Tiwari, Dirk Pattinson. #ITP #Coq
On weakly associative lattices and near lattices (in Mizar). ~ Damian Sawicki, Adam Grabowski. #ITP #Mizar #Math

07-Jan-22

On a property of the class of all real algebraic numbers. ~ Georg Cantor (1874). #Logic #Math #SetTheory
Sobre una propiedad del conjunto de los números algebraicos reales. ~ Georg Cantor (1874). #Lógica #Matemática #Teoría_de_conjuntos vía @kroftopkin
Ueber eine Eigenschaft des Inbegriffes aller reellen algebraischen Zahlen. ~ Georg Cantor (1874). #Logic #Math #SetTheory
Functional pearl: How to find a fake coin. ~ Richard S. Bird (2019). #Haskell #FunctionalProgramming
Machine learning: Algorithms, models, and applications. ~ Jaydip Sen et als. #eBook #MachineLearning
Databass, Part 1: Queries. ~ Joseph Morag. #Haskell #FunctionalProgramming
Databass, Part 2: Inserting into the database. ~ Joseph Morag. #Haskell #FunctionalProgramming
Buen código, teoría y la programación funcional por Felipe Santa-Cruz (@Felipe_StaCruz) y Camilo Chacón Sartori (@camilo_chacon_s) en “Había una vez un algoritmo…” #Podcast #Programación #ProgramaciónFuncional
Knowledge representation for explainable artificial intelligence: Modeling foundations from complex systems. ~ Joaquín Borrego Díaz, Juan Galán Páez. #AI #KR #XAI
Continuation-passing style, defunctionalization, accumulations, and associativity. ~ Jeremy Gibbons (@jer_gib). #FunctionalProgramming #Haskell
Algorithmics. ~ Richard Bird‚ Jeremy Gibbons‚ Ralf Hinze‚ Peter Hoefner‚ Johan Jeuring‚ Lambert Meertens‚ Bernhard Moeller‚ Carroll Morgan‚ Tom Schrijvers‚ Wouter Swierstra and Nicolas Wu (2020). #Algorithmic_programming
Functional programming. ~ Ralf Hinze (2019). #Haskell #FunctionalProgramming
Introduction to classical and quantum computing. ~ Thomas G. Wong (@thomasgwong). #eBook #Quantum_computing #CompSci
Effect algebras, Girard quantales and complementation in separation logic. ~ Callum Bannister, Peter Höfner, Georg Struth. #ITP #IsabelleHOL
Reasoning about effect interaction by fusion. ~ Zhixuan Yang, Nicolas Wu (2021). #Haskell #FunctionalProgramming
Structured handling of scoped effects. ~ Zhixuan Yang, Marco Paviotti, Nicolas Wu, Birthe van den Berg, and Tom Schrijvers. #Haskell #FunctionalProgramming
Fantastic morphisms and where to find them (A guide to recursion schemes). ~ Zhixuan Yang and Nicolas Wu (2019). #Haskell #FunctionalProgramming

06-Jan-22

An investigation of the laws of thought: On which are founded the mathematical theories of logic. ~ George Boole (1854). #Logic #Matha via @internetarchive
“Recursividad, investigación y el valor de los fundamentos” por Manuel Rubio-Sánchez (@MRubSan) y Camilo Chacón Sartori (@camilo_chacon) en “Había una vez un algoritmo…”. #Podcast #Programación #Computación #Matemáticas
“Programación funcional, Clojure y el amor a la informática” por Andros Fenollosa (@androsfenollosa) y Camilo Chacón Sartori (@camilo_chacon) en “Había una vez un algoritmo…”. #ProgramaciónFuncional #Clojure
The humble programmer. ~ Edsger W. Dijkstra (1972). #CompSci
El programador humilde. ~ Edsger W. Dijkstra (1972). #Programación
Thinking above the code (Video). ~ Leslie Lamport (2014). #CompSci
Thinking above the code (Slides). ~ Leslie Lamport (2014). #CompSci
Polynomial functors: A general theory of interaction. ~ David I. Spivak, Nelson Niu. #CategoryTheory via @Iceland_jack
A list of projects providing tactics for Agda. ~ Wen Kokke (@wenkokke). #ITP #Agda
Linearity and uniqueness: An entente cordiale. ~ Daniel Marshall, Michael Vollmer, and Dominic Orchard. #Granule #FunctionalProgramming via @brendanzab
Exercises for the Haskell Beginners 2022 course. ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
Bottom-up synthesis of recursive functional programs using angelic execution. ~ Anders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri, Isil Dillig. #OCaml #FunctionalProgramming

05-Jan-22

Los principios de la aritmética presentados por un nuevo método. ~ Giuseppe Peano (1889). #Lógica #Matemática via @kroftopkin
“Arithmetices principia, nova methodo exposita” or “The principles of arithmetic, presented by a new method” (both in the original latin and in parallel english translation with modern mathematical notation). ~ Giuseppe Peano (1889). #Logic #Math
Arithmetices principia: nova methodo. ~ Giuseppe Peano (1889). #Logic #Math via @internetarchive
From LCF to HOL: a short history. ~ Michael J. C. Gordon (2000). #ITP #LCF #HOL
Propositions as types. ~ Philip Wadler (2014). #Logic #CompSci
The de Bruijn criterion vs the LCF architecture. ~ Lawrence Paulson. #ITP
Formal verification of a cognitive agent using theorem proving. ~ Alexander Birch Jensen. #ITP #IsabelleHOL
A constructive and synthetic theory of reducibility (Myhill’s isomorphism theorem and Post’s problem for many-one and truth-table reducibility in Coq). ~ Yannick Forster, Felix Jahn, Gert Smolka. #ITP #Coq
Computability in constructive type theory. ~ Yannick Forster. #PhD_Thesis #ITP #Coq
Implementation of Bellard’s algorithm for calculating pi to ‘n’ digits in Haskell. ~ Calvin Beck. #Haskell #FunctionalProgramming #Math
Tealeaves: a Coq framework for proving theorems about syntax abstractly. ~ Lawrence Dunn. #ITP #Coq
Knight’s tour revisited revisited (in Isabelle/HOL). ~ Lukas Koller. #ITP #IsabelleHOL
A dependent dependency calculus. ~ Pritam Choudhury, Harley Eades III, Stephanie Weirich. #Dependent_types #Coq
This month in mathlib (Dec 2021). #ITP #LeanProver #Math
How to implement the lambda calculus, quickly. ~ Stephanie Weirich. #Haskell #FunctionalProgramming #LambdaCalculus
Modular, compositional, and executable formal semantics for LLVM IR. ~ Yannick Zakowski, Calvin Beck, Irene Yoon, Ilya Zaichuk, Vadim Zaliva, and Steve Zdancewic. #ITP #Coq
A type system for extracting functional specifications from memory-safe imperative programs. ~ Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic. #ITP #Coq
Formally verified quantum programming. ~ Robert Rand (2018). #PhD_Thesis #ITP #Coq #QuantumProgramming
Hyperdual numbers and forward differentiation (in Isabelle/HOL). ~ Filip Smola and Jacques Fleuriot. #ITP #IsabelleHOL #Math

04-Jan-22

The foundations of arithmetic: a logico-mathematical enquiry into the concept of number. ~ Gottlob Frege (1884). #Logic #Math
Los fundamentos de la aritmética. ~ Gottlob Frege (1884). #Lógica #Matemática
Die Grundlagen der Arithmetik : eine logisch mathematische Untersuchung über den Begriff der Zahl. ~ Gottlob Frege (1884). #Logic #Math
Cryptography with Prolog. ~ Markus Triska (@MarkusTriska). #Prolog #LogicProgramming
Cryptography with Prolog (Video). ~ Markus Triska (@MarkusTriska). #Prolog #LogicProgramming
Pirouette: Higher-Order typed functional choreographies. ~ Andrew K. Hirsch (@andrewkhirsch), Deepak Garg. #ITP #Coq
RefinedC: Automating the foundational verification of C code with refined ownership types. ~ Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg. #ITP #Coq
VIP: Verifying real-world C idioms with integer-pointer casts. ~ Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell. #ITP #Coq
Consejos y reglas de un simple programador. ~ Camilo Chacón Sartori (@camilo_chacon_s). #Computación #Aprendizaje #Filosofía
Connectivity graphs: A method for proving deadlock freedom based on separation logic. ~ Jules Jacobs, Stephanie Balzer and Robbert Krebbers. #ITP #Coq
Tutorial implementation of Hoare logic in Haskell. ~ Boro Sitnikovski (@BSitnikovski). #Haskell #FunctionalProgramming
Simuliris: A separation logic framework for verifying concurrent program optimizations. ~ Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hai Dang, Robbert Krebbers, Jeehong Kang and Derek Dreyer. #ITP #Coq
Intrinsically typed compilation with nameless labels. ~ Arjen Rouvoet, Robbert Krebbers and Eelco Visser. #ITP #Agda #FunctionalProgramming
Machine-checked semantic session typing. ~ Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers and Jesper Bengtson. #ITP #Coq
Compositional non-interference for fine-grained concurrent programs. ~ Dan Frumin, Robbert Krebbers and Lars Birkedal. #ITP #Coq
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. ~ Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer and Lars Birkedal. #ITP #Coq
ReLoC reloaded: A mechanized relational logic for fine-grained concurrency and logical atomicity. ~ Dan Frumin, Robbert Krebbers and Lars Birkedal. #ITP #Coq
Actris 2.0: Asynchronous session-type based reasoning in separation logic. ~ Jonas Kastberg Hinrichsen, Jesper Bengtson and Robbert Krebbers. #ITP #Coq
The challenge of computer mathematics. ~ Henk Barendregt and Freek Wiedijk (2005). #ITP #Math

03-Jan-22

El análisis matemático de la lógica. ~ George Boole (1847). #Lógica #Matemática
The mathematical analysis of logic. ~ George Boole (1847). #Math via @internetarchive
Gale-Shapley algorithm (in Isabelle/HOL). ~ Tobias Nipkow. #ITP #IsabelleHOL
Roth’s theorem on arithmetic progressions (in Isabelle/HOL). ~ Chelsea Edmonds, Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson. #ITP #IsabelleHOL #Math
Automated theorem proving in the classroom. ~ Wolfgang Windsteiger. #ITP #ATP #Logic #Math
Automated theorem proving in the classroom. ~ Wolfgang Windsteiger. #ITP #ATP #Logic #Math
Lucas’s theorem: formalising generating function proofs. ~ Chelsea Edmonds (2020). #ITP #IsabelleHOL #Math
Sharing geometry proofs across logics and systems. ~ Gilles Dowek. #ITP #Dedukti #Logic #Math
Foundations of formal proof systems. ~ Benjamin Werner. #Logic #Math
FindFacts: A scalable theorem search. ~ Fabian Huch and Alexander Krauss (2020). #ITP #IsabelleHOL
Simple type theory is not too simple: Grothendieck’s schemes without dependent types. ~ Anthony Bordg, Lawrence Paulson, Wenda Li. #TypeTheory #ITP #IsabelleHOL
LIME: Learning inductive bias for primitives of mathematical reasoning. ~ Yuhuai Wu, Markus Rabe, Wenda Li, Jimmy Ba, Roger Grosse, Christian Szegedy. #ITP #MachineLearning #Math
Towards justifying computer algebra algorithms in Isabelle/HOL. ~ Wenda Li (2019). #PhD_Thesis #ITP #IsabelleHOL #Math
INT: An inequality benchmark for evaluating generalization in theorem proving. ~ Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, Roger Grosse. #ITP #MachineLearning
Approche combinatoire pour l’automatisation en Coq des preuves formelles en géométrie d’incidence projective. ~ David Braun (2019). #PhD_Thesis #ITP #Coq #Math
Mechanization of incidence projective geometry in higher dimensions, a combinatorial approach. ~ Pascal Schreck, Nicolas Magaud and David Braun. #ITP #Coq #Math
Automated generation of illustrations for synthetic geometry proofs. ~ Predrag Janičić and Julien Narboux. #ATP #Math
Proofs in theories. ~ Gilles Dowek (2018). #eBook #Logic #Math
Computational logic in the first semester of computer science: An experience report. ~ David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere (2020). #Logic #ITP #ATP
Three different ways to prove Dandelin-Gallucci theorem. ~ David Braun, Nicolas Magaud, Pascal Schreck. #ITP #Coq #Math
Formalising geometric axioms for Minkowski spacetime and without-loss-of-generality theorems. ~ Richard Schmoetten, Jake Palmer, Jacques Fleuriot. #ITP #IsabelleHOL #Math

02-Jan-22

Improving automated strategies for univariate quantifier elimination. ~ Katherine Cordwell, Cesar A. Muñoz, and Aaron M. Dutle. #ITP #PVS #Math
Formal verification of MILS partition scheduling module using layered methods. ~ Yang Gao, Xia Yang, Wensheng Guo, and Xiutai Lu. #ITP #Coq
Haskell beginners 2022: Lecture 1 (Fundamentals). ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
Haskell beginners 2022: Lecture 2 (Data). ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
Haskell beginners 2022: Lecture 3 (Typeclasses). ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
¿Pueden pensar las computadoras digitales? ~ Alan Turing (1951). #Computación #IA
Getting bap in the browser 1. ~ Philip Zucker (@SandMouth). #Ocaml #FunctionalProgramming
Tractatus Logico-Philosophicus. ~ Ludwig Wittgenstein (1922). #Logic
Advent of Haskell: Denotational design. ~ Armando Santos (@_bolt12). #Haskell #FunctionalProgramming
Selective functors & probabilistic programming. ~ Armando Santos (@_bolt12). #MSc_Thesis #Haskell #FunctionalProgramming
Jupyter adaptation of “Learn You a Haskell for Great Good!” ~ James Brock (@jamesdbrock) #Haskell #FunctionalProgramming #Jupyter
Temas interactivos de programación funcional con Haskell. ~ J.A. Alonso. #Haskell #FunctionalProgramming #Jupyter
Compiling quantamorphisms for the IBM Q experience. ~ Ana Neri, Rui Soares Barbosa, José N. Oliveira. #Haskell #FunctionalProgramming #Quantum_computing
Towards quantum program calculation. ~ Ana Neri (2018). #MSc_Thesis #Haskell #FunctionalProgramming #Quantum_computing
Propiedades del número 2022. ~ Antonio Roldán (@Connumeros). #Matemáticas
The source code of Defect Process. ~ Jonathan Thaler (@JonathanThaler). #Haskell #FunctionalProgramming
Extending merge resolution to a family of proof systems. ~ Sravanthi Chede, Anil Shukla. #Logic #CompSci
Extending Prolog for quantified boolean Horn formulas. ~ Anish Mallick, Anil Shukla. #Prolog #LogicProgramming

01-Jan-22

Readings on computational logic, interactive theorem proving, and functional programming. #ITP #FunctionalProgramming
Machine checked properties of the Schulze method. ~ Mukesh Tiwari and Dirk Pattinson. #ITP #Coq
Comprehensive Python cheatsheet. ~ Jure Šorn. #Python
Engineering elegant systems: Systems as mathematical categories. ~ Michael D. Watson (2019). #CategoryTheory
Category theory for Engineers. ~ Larry A. Lambe (2018). #CategoryTheory
Categories, mathematics, and systems. ~ Larry A. Lambe (2018). #CategoryTheory
Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOL. ~ Jørgen Villadsen. #ITP #Agda #IsabelleHOL
Formally verified verifiable electronic voting scheme. ~ Mukesh Tiwari. #PhD_Thesis #ITP #Coq
Principia Mathematica (Vol. 1). ~ Alfred North Whitehead and Bertrand Russell (1910). #Logic #Math
Principia Mathematica (Vol. 2). ~ Alfred North Whitehead and Bertrand Russell (1912). #Logic #Math
Principia Mathematica (Vol. 3). ~ Alfred North Whitehead and Bertrand Russell (1927). #Logic #Math
Computational logic: its origins and applications. ~ Lawrence C. Paulson (2018). #Logic #CompSci #ITP
The Principia Rewrite project (rewriting ‘Principia Mathematica’ in Coq). ~ Landon D. C. Elkind (@LogicalAtomist) et als. #ITP #Coq #Logic #Math
Performing security proofs of stateful protocols. ~ Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker and Anders Schlichtkrull. #ITP #IsabelleHOL
Formalization of logic in the Isabelle proof assistant. ~ Anders Schlichtkrull (2018). #PhD_Thesis #ITP #IsabelleHOL #Logic
Hybrid logic. ~ Asta Halkjær From (2020). #MSc_Thesis #ITP #IsabelleHOL #Logic
History of Logic. ~ Prathyush (@prathyvsh). #Logic
Liquid Tensor Experiment: an update. ~ Johan Commelin. #ITP #LeanProver #Math
Resources for learning Category Theory for an enthusiast. ~ Prathyush (@prathyvsh). #CategoryTheory
La reina de las ciencias (algunos contenidos esenciales de la ciencia matemática). ~ Emilio Méndez Pinto (@kroftopkin). #Lógica #Matemática #Historia
Introduction to the seL4 proofs. ~ Matthew Brecknell (@mbrcknl). #ITP #IsabelleHOL
A compositional proof framework for FRETish requirements. ~ Esther Conrad, Laura Titolo, Dimitra Giannakopoulou, Thomas Pressburger, Aaron Dutle. #ITP #PVS
Formal analysis of the compact position reporting algorithm. ~ Aaron Dutle, Mariano M. Moscato, Laura Titolo, César A. Muñoz, Gregory Anderson, and François Bobot. #ITP #PVS
Formal verification of semi-algebraic sets and real analytic functions. ~ J. Tanner Slagel, Lauren White, and Aaron Dutle. #ITP #PVS #Mat

Readings of the year 2021

December 2021

31-Dic-21

Classification of finite fields with applications. ~ Hing-Lun Chan and Michael Norrish (2019). #ITP #HOL4 #Math
Proof pearl: Bounding least common multiples with triangles. ~ Hing-Lun Chan and Michael Norrish (2019). #ITP #HOL4 #Math
A string of pearls: Proofs of Fermat’s little theorem. ~ Hing-Lun Chan and Michael Norrish (2013). #ITP #HOL4 #Math
Mechanised modal model theory. ~ Yiming Xu and Michael Norrish (2020). #ITP #HOL4 #Logic
Formalizing modal logic in HOL. ~ Yiming Xu. #BSc_Thesis #ITP #HOL4 #Logic
Category theory: Lecture notes and online books. ~ Peter Smith (@PeterSmith). #CategoryTheory
People, ideas, milestones: a scientometric study of computational thinking. ~ M. Saqr, K. Ng, S. Oyelere, M. Tedre. #Computational_thinking
Names and numbers for modal logic axioms. ~ John D. Cook (@JohnDCook). #Logic

30-Dic-21

On the relational translation method for propositional modal logics. ~ Jian Zhang. #ATP #OTTER
Learning higher-order programs without meta-interpretive learning. ~ Stanisław J. Purgał, David M. Cerna, Cezary Kaliszyk. #ITP #MachineLearning #LogicProgramming #Prolog #ASP
Inductive and coinductive predicate liftings for effectful programs. ~ Niccolò Veltri, and Niels F.W. Voorneveld. #ITP #Agda
A cartesian bicategory of polynomial functors in Homotopy Type Theory. ~ Eric Finster, Samuel Mimram, Maxime Lucas, Thomas Seiller. #ITP #Agda #HoTT
Theorem Proving Haiku. #ITP
Importing CSV data with Haskell and the World’s dependency on fossil fuels. ~ Fábio Molinar. #Haskell #FunctionalProgramming
To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. (Edited by J.P. Seldin and J.R. Hindley, 1980). #Logic #Math #LambdaCalculus via @breandan
Évolution des mathématiques au XXe siècle et après. ~ Hourya Benis and Mirna Džamonja #Math
Théorie de la démonstration. ~ Pierre-Louis Curien (2009). #Logic #Math
Cours: Preuves assistées par ordinateur (hiver 2021). ~ Hugo Herbelin, and Théo Zimmermann. #ITP #Coq
Logic and mechanized reasoning. ~ Jeremy Avigad, Marijn J. H. Heule, and Wojciech Nawrocki. #eBook #Logic #Math #LeanProver #FunctionalProgramming #SAT #SMT
Logic and mechanized reasoning (Repository). ~ Jeremy Avigad, Marijn J. H. Heule, and Wojciech Nawrocki. #Logic #Math #LeanProver #FunctionalProgramming #SAT #SMT
Logic and mechanized reasoning (Course). ~ Jeremy Avigad, Marijn J. H. Heule, and Wojciech Nawrocki. #Logic #Math #LeanProver #FunctionalProgramming #SAT #SMT
Teaching logic and mechanized reasoning with Lean 4 (Slides). ~ Jeremy Avigad (Marijn Heule and Wojciech Nawrocki). #ITP #LeanProver #Logic
Formal verification of transcendental fixed and floating point algorithms using an automatic theorem prover. ~ Samuel Coward, L. C. Paulson, Theo Drane and Emiliano Morini. #ATP #MetiTarski #Math
A modular first formalisation of combinatorial design theory. ~ Chelsea Edmonds and L. C. Paulson. #ITP #IsabelleHOL
Formal mathematics, dependent type theory, and the Topos Institute (Slides). ~ Jeremy Avigad. #ITP #LeanProver #Math
Formal mathematics, dependent type theory, and the Topos Institute (Video). ~ Jeremy Avigad. #ITP #LeanProver #Math
Implementing a functional language with graph reduction. ~ Thomas Mahler. #Haskell #FunctionalProgramming
EditorConfig y Emacs. ~ Notxor. #Emacs
Theorem proving in Lean 4. ~ Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich. #Lean4 #ITP #FunctionalProgramming

29-Dic-21

Proof automation (Class 1: Impacts). ~ Talia Ringer (@TaliaRinger). #Proof_engineering #ITP #Coq
Proof automation (Spring 2022). ~ Talia Ringer (@TaliaRinger). #Proof_engineering #ITP
QED at large: A survey of engineering of formally verified software. ~ Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. #Proof_engineering #ITP
Implementing Euclid’s straightedge and compass constructions in type theory. ~ Ariel Kellison, Mark Bickford, and Robert Constable (2019). #ITP #Nuprl #Math
Formalizing ordinal partition relations using Isabelle/HOL. ~ Mirna Džamonja, Angeliki Koutsoukou-Argyraki, and Lawrence C. Paulson. #ITP #IsabelleHOL #Math
Formalising Ramsey theory, I. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
Regular tree relations (in Isabelle/HOL). ~ Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann, and Thomas Sternagel. #ITP #IsabelleHOL
Verified algorithms for solving Markov decision processes (in Isabelle/HOL). ~ Maximilian Schäffeler, Mohammad Abdulaziz. #ITP #IsabelleHOL #Math
Markov decision processes with rewards (in Isabelle/HOL). ~ Maximilian Schäffeler and Mohammad Abdulaziz. #ITP #IsabelleHOL #Math
Hoogle+ is a type-driven synthesis engine for Haskell - like Hoogle but able to find compositions of functions. Given a Haskell type, Hoogle+ generates terms that inhabit this type by composing library components. #Haskell #FunctionalProgramming
Hoogle+: Type-driven, component based synthesis, showcasing TYpe Guided Abstract Refinement (TYGAR). ~ Zheng Guo (@AaronGuo069). #Haskell #FunctionalProgramming
Program synthesis by type-guided abstraction refinement. ~ Zheng Guo et als. #Haskell #FunctionalProgramming
Digging for fold: Synthesis-aided API discovery for Haskell. ~ Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, and Nadia Polikarpova. #Haskell #FunctionalProgramming
[[https://aaronguo1996.github.io/talk/tygar/tygar_v4.pdf][Hoogle+: Program synthesis by type-guided abstraction refinement [Slides]]]. ~ Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. #Haskell #FunctionalProgramming
Co-presheaf optics. ~ Bartosz Milewski (@BartoszMilewski). #CategoryTheory

28-Dic-21

MetaCoq: a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq. #ITP #Coq
The MetaCoq project. ~ Matthieu Sozeau et als. #ITP #Coq
[[https://dannenkov.me/papers/COBRA2021-slides.pdf][Smart contracts in a proof assistant [Slides]]]. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters #ITP #Coq
Mathématiques assistées par ordinateur. ~ Assia Mahboubi. #ITP #Coq #Math
Machine-checked mathematics. ~ Assia Mahboubi. #ITP #Coq #Math
Extracting functional programs from Coq, in Coq. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq
The undecidability of first-order logic over small signatures. ~ Johannes Hostert (Advisors: Andrej Dudenhefner and Dominik Kirst). #BSc_Thesis #ITP #Coq #Logic #Math
Modeling Peano Arithmetic in constructive type theory (Undecidability and Tennenbaum’s theorem). ~ Marc Hermes (Advisors: Dominik Kirst and Moritz Weber). #MSc_Thesis #ITP #Coq #Logic #Math
Extracting smart contracts tested and verified in Coq. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq
Undecidability, incompleteness, and completeness of second-order logic in Coq. ~ Mark Koch, Dominik Kirst. #ITP #Coq #Logic #Math
Formalising metamathematics in constructive type theory. ~ Dominik Kirst. #ITP #Coq #Logic #Math
Formalizing implicative algebras in Coq. ~ Étienne Miquey. #ITP #Coq
Realizabilidad clásica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard. ~ Étienne Miquey. #Logic #CompSci
Curry-Howard: unveiling the computational content of proofs. ~ Étienne Miquey. #Logic #CompSci
The benefits of sequent calculus. ~ Étienne Miquey. #Logic #CompSci

27-Dic-21

An excursion in formal verification with Coq. ~ Oliver Nash. #ITP #Coq #Math

26-Dic-21

How Gödel discovered his incompleteness theorems. ~ Jan von Plato. #Logic #Math
Windmills of the minds: an algorithm for Fermat’s Two Squares Theorem. ~ Hing Lun Chan. #ITP #HOL4 #Math

25-Dic-21

Meta-analysis of type theories with an application to the design of formal proofs. ~ Anja Petković Komel (Adviser: Andrej Bauer). #PhD_Thesis #TypeTheory #ITP
A computational and abstract approach to Gödel’s first incompleteness theorem. ~ Benjamin Peters. #Logic #Math
Synthetic undecidability and incompleteness of first-order axiom systems in Coq. ~ Dominik Kirst, Marc Hermes. #ITP #Coq #Logic #Math
CertiCAN: Certifying CAN analyses and their results. ~ Pascal Fradet, Xiaojie Guo, Sophie Quinton. #ITP #Coq
L-types for resource awareness: an implicit name approach. ~ Silvia Ghilezan, Jelena Ivetić, Simona Kašterović, Pierre Lescanne. #Haskell #Agda #FunctionalProgramming
Fermat’s Christmas Theorem: Fixed points come in pairs. ~ John Lawrence Aspden. #Clojure #FunctionalProgramming #Math

24-Dic-21

A manifesto for applicable formal methods. ~ Mario Gleirscher, Jaco van de Pol, Jim Woodcock. #FormalMethods
Composing transformers: ~ Felix Springer. #Haskell #FunctionalProgramming
Parser combinators in Haskell. ~ Heitor Toledo Lassarote de Paula. #Haskell #FunctionalProgramming
The year in math and computer science. ~ Bill Andrews. #Math CompSci

23-Dic-21

Readability in proofs: the mean value theorem (in Isabelle/HOL). ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
Research groups working on formal proofs in Europe. #FormalMethods #ITP

22-Dic-21

A machine-checked direct proof of the Steiner-Lehmus theorem. ~ Ariel Kellison. #ITP #Nuprl #Math

21-Dic-21

Constructive and mechanised meta-theory of intuitionistic epistemic logic. ~ Christian Hagemeier, Dominik Kirst. #ITP #Coq #Logic
Accurate calculation of euclidean norms using double-word arithmetic. ~ Vincent Lefèvre, Nicolas Louvet, Jean-Michel Muller, Joris Picot, Laurence Rideau. #ITP #Coq
A Haskell implementation for a dependent type theory with definitions. ~ Qufei Wang. #MSc_Thesis #Haskell #FunctionalProgramming
Functional approaches to programming (Lisp / Haskell: the diff tutorial). ~ Didier Verna (@didierverna). #Lisp #Haskell #FunctionalProgramming
Learning to navigate the maze! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming

20-Dic-21

Functional programming in Coq theorem prover (Lecture 3: induction on natural numbers). ~ Mukesh Tiwari (@mukesh_tiwari). #ITP #Coq

19-Dic-21

CertiStr: A certified string solver (technical report). ~ Shuanglong Kan, Anthony W. Lin, Philipp Rümmer, Micha Schrader. #ITP #IsabelleHOL
Formalization of Euclid’s elements book 1 in Dedukti. ~ Karnaj. #Math #ITP #Dedukti #Coq, #HOL_Light, #Lean, #Matita, #OpenTheory #PVS
On homotopy of walks and spherical maps in homotopy type theory. ~ Jonathan Prieto-Cubides. #ITP #Agda #HoTT #Math
Formal semantics and formally verified validation for temporal planning. ~ M. Abdulaziz, L. Koller. #ITP #IsabelleHOL

18-Dic-21

GeoCoq: A formalization of geometry in Coq. ~ Julien Narboux (@jnarboux). #ITP #Coq #Math
Verified compilation of quantum oracles. ~ Liyi Li, Finnegan Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, Michael Hicks. #ITP #Coq
Verifying a minimalist reverse-mode AD library. ~ Paulo Emílio de Vilhena, François Pottier. #ITP #Coq
On planarity of graphs in homotopy type theory. ~ Jonathan Prieto-Cubides, Håkon Robbestad Gylterud. #ITP #Agda #HoTT #Math
Fifty years of P vs. NP and the possibility of the impossible. ~ Lance Fortnow. #CompSci
Declarative machine learning systems. ~ Piero Molino, Christopher Ré. #MachineLearning #AI
Will AI destroy education? ~ Moshe Y. Vardi. #AI #Education

17-Dic-21

Semantic cut elimination for the logic of bunched implications, formalized in Coq. ~ Dan Frumin. #ITP #Coq
Semantics and contextual equivalence for probabilistic programs with nested queries and recursion. ~ Yizhou Zhang, Nada Amin. #ITP #Coq
Johan Commelin interviews Yaël Dillies. #ITP #LeanProver #MathLib
Type-level sharing in Haskell, now. ~ Edsko de Vries, Andres Löh, Adam Gundry, Sam Derbyshire. #Haskell #FunctionalProgramming
Game rules with a Free Monad DSL. ~ Rogan Murley (@RoganMurley). #Haskell #FunctionalProgramming
Understanding space leaks from StateT. ~ Ziyang Liu. #Haskell #FunctionalProgramming
Do you know where Haskell is used? (Examples of how Haskell is used in different industries). ~ Catherine Galkina. #Haskell #FunctionalProgramming

16-Dic-21

Materiales para el estudio de la programación funcional con Haskell. #Haskell #ProgramaciónFuncional
Deducción automática (Vol. 1: Construcción lógica de sistemas lógicos). ~ José A. Alonso y Joaquín Borrego. ~ #Prolog #ProgramaciónLógica #Lógica #DAT
HOWTO: Get started with Agda. ~ Jan Malakhovski. #Agda #FunctionalProgramming
The decent way to learn functional programming. ~ Jan Malakhovski. #FunctionalProgramming #Haskell #Agda

15-Dic-21

Completeness theorems for first-order logic analysed in constructive type theory. ~ Yannick Forster, Dominik Kirst, Dominik Wehr. #ITP #Coq #Logic
Cómo factorizó Euler F5. ~ M.A. Morales (@gaussianos). #Matemáticas

14-Dic-21

Formalization in Lean of IMO 2005 Q4. ~ Heather Macbeth. #ITP #LeanProver #Math #IMO
CoSMed: A confidentiality-verified social media platform (in Isabelle/HOL). ~ Thomas Bauereiss, Andrei Popescu. #ITP #IsabelleHOL
Formalising the foundations of discrete reinforcement learning in Isabelle/HOL. ~ Mark Chevallier, Jacques Fleuriot. #ITP #IsabelleHOL #MachineLearning #AI
Mechanized verification of a fine-grained concurrent queue from Meta’s Folly Library. ~ S.F. Vindum, D Frumin, L Birkedal. #ITP #Coq
Do Gödel’s incompleteness theorems matter?. ~ Lawrence Paulson #Logic #Math #ITP
Implementation: Creating a maze environment. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #Gloss

13-Dic-21

Foundation of geometry in planes, and some complements: Excluding the parallel axioms (in Isabelle/HOL). ~ Fumiya Iwama. #ITP #IsabelleHOL #Math
Formalizing higher-order termination in Coq. ~ Deivid Vale, Niels van der Weide. #ITP #Coq
Simplicial complexes and boolean functions (in Isabelle/HOL). ~ Jesús Aransay, Alejandro del Campo, Julius Michaelis. #ITP #IsabelleHOL #Math
An impossible asylum. ~ Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki. #ATP #Vampire #Logic
“The genuine sieve of Eratosthenes” in Clojure. ~ Gary Verhaegen. #Clojure #FunctionalProgramming

11-Dic-21

Certified abstract machines for skeletal semantics. ~ Guillaume Ambal, Sergueï Lenglet, Alan Schmitt. #ITP #Coq #OCaml #FunctionalProgramming
Semilinear maps (in Lean). ~ Frédéric Dupuis. #ITP #LeanProver #Math
A specification for typed template Haskell. ~ Matthew Pickering, Andres Löh, Nicolas Wu. #Haskell #FunctionalProgramming

10-Dic-21

Formalising Lie algebras. ~ Oliver Nash. #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
QRC1 in Coq (Formalizing a quantified modal logic). ~ Ana de Almeida Borges. #ITP #Coq #Logic
Haskell’s type system standing alone. ~ Vitez. #Haskell #FunctionalProgramming

09-Dic-21

Formalization of forcing in set theory. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, Matías Steinberg. #ITP #IsabelleZF #Logic #Math #SetTheory
Type-checking plugins, Part II: GHC’s constraint solver. ~ Sam Derbyshire. #Haskell #FunctionalProgramming

07-Dic-21

ALEXANDRIA: Large-scale formal proof for the working mathematician. ~ Lawrence Paulson. #ITP #IsabelleHOL #Coq #LeanProver
Fundamentals of logic and computation (With practical automated reasoning and verification). Zhe Hou. #eBook #Logic #CompSci #ITP #IsabelleHOL
Validating safety arguments with Lean. ~ Logan Murphy, Torin Viger, Alessio Dia Sandro, Ramy Shahin, Marsha Chechik. #ITP #LeanProver
This month in mathlib (Nov 2021)./#ITP #LeanProver #MahLib
Normalization for Fitch-style modal calculi. ~ Nachiappan Valliappan , Fabian Ruch, Carlos Tomé Cortiñas. #ITP #Agda
El lamento de un matemático. ~ Paul Lockhart. #Matemática #AI #MachineLearning #Math
Discrete mathematics (An open introduction, 3rd edition). ~ Oscar Levin. #eBook #Math

06-Dic-21

Why formalize mathematics? ~ Patrick Massot. #ITP #LeanProver #Math
From World to Environment: Open AI Gym Primer. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI

05-Dic-21

Functional programming in Coq theorem prover: Lecture 2. ~ Mukesh Tiwari (@mukesh_tiwari). #ITP #Coq #FunctionalProgramming
Demystifying the state monad. ~ Hugo Peters. #Haskell #FunctionalProgramming

04-Dic-21

Using Coq to enforce the checks-effects-interactions pattern in DeepSEA smart contracts. ~ D. Britten, V. Sjöberg, S. Reeves. #ITP #Coq
Formalization of dependent type theory: The example of CaTT. ~ Thibaut Benjamin. #ITP #Agda
TacticToe: Learning to prove with tactics. ~ Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, Michael Norrish. #ITP #HOL4 #MachineLearning
What’s that Typeclass: Foldable. ~ Alyona Antonova. #Haskell #FunctionalProgrammiang
A 7 lecture Haskell Crash Course. #Haskell #FunctionalProgramming
Muḥammad ibn Mūsā al-Khwārizmī. ~ Chris Simms. #Math #CompSci

02-Dic-21

What is the point of computers? A question for pure mathematicians. ~ Kevin Buzzard. #ITP LeanProver #Math
Formally verified derivation of an executable and terminating CEK machine from call-by-value calculus. ~ Wojciech Rozowski. #ITP #Agda
Haskelling the Advent of Code 2021 - Day 0. #Haskell #FunctionalProgramming
Haskelling the Advent of Code 2021 - Day 1. #Haskell #FunctionalProgramming
Graspable math activities: Assign algebra tasks to your students and see live feedback of their step-by-step work. Discover, create, and share engaging math activities for 4th to 12th graders. #Math

01-Dic-21

The HoTT Game. ~ Joseph Hua. #HoTT #ITP #Agda
Assessing Haskell. ~ @nyeogmi. #Haskell #FunctionalProgramming
Artificial intelligence aids intuition in mathematical discovery. ~ Christian Stump. #AI #Math
Domain-specific languages and code synthesis using Haskell. ~ Andy Gill. #Haskell #FunctionalProgramming
RankNTypes via lambda calculus. ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming

November 2021

30-Nov-21

On relational compilation. ~ Clément Pit-Claudel (@cpitclaudel). #ITP #Coq
See and believe: Visualizing with Gloss. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming

28-Nov-21

A complete axiom system for 1-free Kleene star expressions under bisimilarity: An elementary proof. ~ Allan van Hulst. #ITP #Coq
Coherence for monoidal and symmetric monoidal groupoids in Homotopy Type Theory. ~ Stefano Piceghello. #PhD_Thesis #ITP #Coq #HoTT

27-Nov-21

Simple formally verified compiler in Lean. ~ Leo Okawa Ericson. #ITP #LeanProver
Using Isabelle in two courses on logic and automated reasoning. ~ Jørgen Villadsen, Frederik Krogsdal Jacobsen. #ITP #IsabelleHOL #Logic #ATP
[[http://lcs.ios.ac.cn/fm2021/recordings/fm_tea/Avigad.mp4][Teaching logic and mechanized reasoning with Lean 4 [Video]]]. ~ Jeremy Avigad. #ITP #LeanProver #Logic
[[http://lcs.ios.ac.cn/fm2021/recordings/fm_tea/Tobias.mp4][Teaching algorithms and data structures with a proof assistant [Video]]]. ~ Tobias Nipkow. #ITP #IsabelleHOL #Algorithms
SeCaV: A sequent calculus verifier in Isabelle/HOL. ~ AH From, FK Jacobsen, J Villadsen. #ITP #IsabelleHOL #Logic

23-Nov-21

Dijkstra’s most powerful lessons. ~ Eliran Turgema. #Dijkstra #CompSci
Lean 4 Hackers. ~ J Kenneth King. #Lean4 #FunctionalProgramming
AI revisited: Breaking down BFS. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
Dedekind domains and class number in Lean. ~ Anne Baanen. #ITP #LeanProver #Math

21-Nov-21

Functional programming in Coq theorem prover - Lecture 1. ~ Mukesh Tiwari (@mukesh_tiwari). #ITP #Coq #FunctionalProgramming
An introduction to Lean 4, a functional programming language. ~ Adolfo Neto (@adolfont). #ITP #LeanProver #FunctionalProgramming
Programming with tactics. ~ Reed Mullanix. #Haskell #FunctionalProgramming

20-Nov-21

cryptolib: Security proofs in the Lean theorem prover. ~ Joey Lup. #MSc_Thesis #ITP #LeanProver
‘Amazing’ Math bridge extended beyond Fermat’s Last Theorem. ~ Erica Klarreich. #Math
Modelling and proving safety in autonomous cars scenarios in HOL-CSP. ~ Burkhart Wolff, Safouan Taha. #ITP #IsabelleHOL

18-Nov-21

Competitive programming in Haskell: BFS, part 4 (implementation via STUArray). ~ Brent Yorgey. #Haskell #FunctionalProgramming

17-Nov-21

Toward a quantum programming language for higher-level formal verification. ~ Finn Voichick, Michael Hicks. #ITP #Coq #QuantumProgramming
Competitive programming in Haskell: Enumeration. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Solving linear algebra by program synthesis. ~ Iddo Drori, Nakul Verma. #AI #MachineLearning #Math

16-Nov-21

A mechanized investigation of an axiomatic system for Minkowski spacetime. ~ Mathis Gerdes. #MSc_Thesis #ITP #IsabelleHOL
A beginner’s guide to Haskell and its ecosystem. ~ Alejandro Serrano (@trupill).s#1 #Haskell #FunctionalProgramming
A sequent calculus for first-order logic formalized in Isabelle/HOL. ~ Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
Exploring Euler’s differentials of trigonometric functions in Isabelle using nonstandard analysis. ~ Alice Johansen. #ITP #IsabelleHOL #Math
Verified quadratic virtual substitution for real arithmetic. ~ Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer. #ITP #IsabelleHOL #Logic #Math

15-Nov-21

An experiment: The Cauchy–Schwarz inequality. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
Verified optimization. ~ Alexander Bentkamp, Jeremy Avigad. #ITP #LeanProver #Math

14-Nov-21

Verified decision procedures for modal logics. ~ Minchao Wu, Rajeev Goré. #ITP #LeanProver #Logic
Automating public announcement logic and the wise men puzzle in Isabelle/HOL. ~ Christoph Benzmüller, Sebastian Reiche. #ITP #IsabelleHOL
Factorization of polynomials with algebraic coefficients (in Isabelle/HOL). ~ Manuel Eberl, René Thiemann. #ITP #IsabelleHOL #Math

13-Nov-21

Conditional independence in functional probabilistic programming. ~ Wink van Zon. #MSc_Thesis #Haskell #FunctionalProgramming
The axiom of choice and descriptions. ~ Lawrence Paulson. #Logic #Math #IsabelleHOL

12-Nov-21

Answer set programming made easy. ~ Jorge Fandinno, Seemran Mishra, Javier Romero, Torsten Schaub. #LogicProgramming #ASP
Should Type Theory replace Set Theory as the foundation of Mathematics? ~ Thorsten Altenkirch. #Logic #Math #TypeTheory #SetTheory

11-Nov-21

Towards tractable mathematical reasoning: Challenges, strategies, and opportunities for solving math word problems. ~ Keyur Faldu, Amit Sheth, Prashant Kikani, Manas Gaur, Aditi Avasthi. #AI #Math #MachineLearning

10-Nov-21

Real exponents as the limits of sequences of rational exponents (in Isabelle/HOL). ~ Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
Löb and möb: strange loops in Haskell. ~ David Luposchainsky (@quch3n). #Haskell #FunctionalProgramming

08-Nov-21

Szemerédi’s regularity lemma (in Isabelle/HOL). ~ Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
Formalization in Lean of IMO 1994 Q1. ~ Antoine Labelle. #ITP #LeanProver #Math #IMO
The principles of deep learning theory (An effective theory approach to understanding neural networks). ~ Daniel A. Roberts, Sho Yaida, Boris Hanin. #eBook #DeepLearning #NeuralNetwork #AI #Math
Coffee corner: are deep learning’s returns diminishing?. #DeepLearning #AI

07-Nov-21

A Coq formalization of abstract algebra using a functional programming style. ~ Larry Darryl Lee Jr. #ITP #Coq #Math
Formalization of some elementary mathematical theories in Coq. ~ Evgeny Ivashkevich. #ITP #Coq #Math

06-Nov-21

A course on formal verification at CS Club. ~ Anton Trunov (@falsenov). #ITP #Coq #MathComp #SSReflect
Programs and proofs (Mechanizing mathematics with dependent types). ~ Ilya Sergey (@ilyasergey). #ITP #Coq #MathComp #SSReflect #Math
Coq Winter School 2018-2019 (SSReflect & MathComp). ~ Yves Bertot, Cyril Cohen, Laurence Rideau, Enrico Tassi and Laurent Thery. #ITP #Coq #MathComp #SSReflect

05-Nov-21

1001 representations of syntax with binding. ~ Jesper Cockx (@agdakx). #ITP #Agda

04-Nov-21

This month in mathlib (Oct 2021). #ITP #LeanProver #MathLib #Math
A formalization of Kolmogorov complexity in synthetic computability theory. ~ Nils Lauermann. #BSc_Thesis #ITP #Coq #CompSci
Modular specification and compositional soundness of abstract interpreters. ~ Sven Keidel. #PhD_Thesis #Haskell #FunctionalProgramming
Conflict resolution for data updates by multiple bidirectional transformations. ~ Mikiya Habu, Soichiro Hidaka. #ITP #Coq
Predicate transformer semantics for hybrid systems (Verification components for Isabelle/HOL). ~ Jonathan Julián Huerta y Munive, Georg Struth. #ITP #IsabelleHOL
7 useful tools written in Haskell. ~ Nikolay Rulev. #Haskell #FunctionalProgramming
Sturdy: a library for developing sound static analyses in Haskell. ~ Sven Keidel. #Haskell #FunctionalProgramming
It is declarative (On declarative programming in Prolog). ~ Włodzimierz Drabent. #Prolog #LogicProgramming
It is declarative (On declarative programming in Prolog) 2nd part. ~ Włodzimierz Drabent. #Prolog #LogicProgramming

03-Nov-21

Hydras & Co.: Formalized mathematics in Coq for inspiration and entertainment. ~ Pierre Castéran, Jérémy Damour, Karl Palmskog, Clément Pit-Claudel, Théo Zimmermann. #ITP #Coq #Math
Hydras, Ordinals & Co. A library in Coq of entertaining formal mathematics. ~ Pierre Castéran. #ITP #Coq #Math
Contributions to mathlib from LTE about normed groups. ~ Riccardo Brasca. #ITP #LeanProver #Math
Challenges in the collaborative evolution of a proof language and its ecosystem. ~ Théo Zimmermann. #PhDThesis #ITP #Coq
Can mathematics be done by machine? I. ~ Michael Harris. #ITP #Math #AI
Avances en la resolución de los problemas diofánticos. ~ Rachel Crowell. #Matemáticas

02-Nov-21

NG de Bruijn and AUTOMATH. ~ Lawrence Paulson @Cambridge_CL #ITP #AutoMath #Math
Getting started with OCaml in 2021. ~ Tim McGilchrist. #OCaml #FunctionalProgramming
Mathematical components. ~ Assia Mahboubi, Enrico Tassi. #ITP #Coq #Math
Lean versus Coq: The cultural chasm. ~ Ramkumar Ramachandra (@artagnon). #ITP #LeanProver #Coq #Logic #Math
Design of quantum optical experiments with logic artificial intelligence. ~ Alba Cervera-Lierta, Mario Krenn, Alan Aspuru-Guzik. #AI #Logic #SAT #QuantumPhysics

01-Nov-21

Structures algébriques fondamentales. ~ Patrick Massot. #Math
Coq exercises for beginners. ~ Ömer Sinan Ağacan. #ITP #Coq #Math
Packaging mathematical structures. ~ François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau. #ITP #Coq #Math
Type classes for mathematics in type theory. ~ Bas Spitters, Eelis van der Weegen.3# #ITP #Coq #Math
Group theory in Lean. ~ Mitchell Rowet. #ITP #LeanProver #Math

October 2021

31-Oct-21

X86 instruction semantics and basic block symbolic execution (in Isabelle/HOL). ~ Freek Verbeek, Abhijith Bharadwaj, Joshua Bockenek, Ian Roessle, Timmy Weerwag, Binoy Ravindran. #ITP #IsabelleHOL
A formal verification of reversible primitive permutations. ~ Giacomo Maletto. #BSc_Thesis #ITP #LeanProver #Logic #Math
#SEP: Natural deduction systems in logic. ~ Francis Jeffry Pelletier, Allen Hazen. #Logic

30-Oct-21

Modelling puzzles in first order logic ~ Adrian Groza. #ATP #Prover9
Competitive programming in Haskell: BFS, part 3 (implementation via HashMap). ~ Brent Yorgey. #Haskell #FunctionalProgramming
AI has cracked a key mathematical puzzle for understanding our world. ~ Karen Hao. #AI #MachineLearning #Math

29-Oct-21

Formalization in Lean of IMO 2021 Q1. ~ Mantas Bakšys. #ITP #LeanProver #Math #IMO
Demostración asistida por ordenador. ~ Jesús María Aransay Azofra, César Domínguez Pérez. #DAO #IsabelleHOL #Matemáticas
Tutorial to locales and locale interpretation. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math
Haskell-style type classes with Isabelle/Isar. ~ Florian Haftmann. #ITP #IsabelleHOL
Mathematical Logic, Lecture 14 (Presburger arithmetic). ~ Artem Chernikov (@archernikov). #Logic #Math

28-Oct-21

Why explain mathematics to computers? ~ Patrick Massot. #ITP #LeanProver #Math

27-Oct-21

Irrationality and transcendence criteria for infinite series in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
On proving lists infinite. ~ Li-yao Xia (@lysxia). #ITP #Coq
Mathematical Logic, Lecture 12 (Quantifier elimination). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 13 (Quantifier elimination in algebraically closed fields). ~ Artem Chernikov (@archernikov). #Logic #Math

26-Oct-21

Technical perspective: On proofs, entanglement, and games. ~ Dorit Aharonov, Michael Chapman. #CompSci

25-Oct-21

Monad transformers – Part 1: An introduction. ~ @rezigned. #Haskell #FunctionalProgramming
Quantum physics in Lean. ~ Mario Krenn (@MarioKrenn6240). #ITP #LeanProver #Physics

24-Oct-21

On logical formalisms. ~ Lawrence Paulson. #Logic #ITP
Integrating automated theorem provers in proof assistants. ~ Yacine El Haddad. #PhDThesis #ITP #ATP
Belief revision theory (in Isabelle/HOL). ~ Valentin Fouillard, Safouan Taha, Frédéric Boulanger, Nicolas Sabouret. #ITP #IsabelleHOL
Proof complexity of modal resolution. ~ Sarah Sigley, Olaf Beyersdorff. #ATP #Logic #Automated_reasoning

23-Oct-21

A formalisation of abstract argumentation in higher-order logic. ~ Alexander Steen, David Fuenmayor. #ITP #IsabelleHOL
Towards an accessible mathematics working environment in education. ~ K Miesenberger, W Neuper, B Stöger, M Wenzel. #ITP #IsabelleHOL #Math
Make Isabelle accessible!. ~ R. Koutny, K. Miesenberger, W. Neuper, B. Stöger. #ITP #IsabelleHOL
From conduit to streamly. ~ Julian Ospald. #Haskell #FunctionalProgramming
Learn from errors: Overlapping instances. ~ Sandeep Chandrika. #Haskell #FunctionalProgramming

22-Oct-21

Mathematical Logic, Lecture 11 (Upward Löwenheim-Skolem and expansions by definition). ~ Artem Chernikov (@archernikov). #Logic #Math
Algebras for iteration, infinite executions and correctness of sequential computations. ~ Walter Guttmann. #ITP #IsabelleHOL
Verified quadratic virtual substitution for real arithmetic. ~ Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer. #ITP #IsabelleHOL #Math
Emacs as a tool for modern science. ~ Timothy Johnson. #Emacs #OrgMode

21-Oct-21

Introductory example: Fibonacci numbers (in Isabelle/HOL). ~ Lawrence Paulson @Cambridge_CL #ITP #IsabelleHOL #Math
More on Fibonacci numbers, with equational reasoning (in Isabelle/HOL). ~ Lawrence Paulson @Cambridge_CL #ITP #IsabelleHOL #Math
Formalizing ordinal partition relations using Isabelle/HOL. ~ Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
Induction without core-size blow-up a.k.a. Large records: anonymous edition. ~ Edsko de Vries, Adam Gundry. #Haskell #FunctionalProgramming
Proving commutativity of polysemy interpreters. ~ Sandy Maguire. #Haskell #FunctionalProgramming
Type-checking plugins, Part I: Why write a type-checking plugin?. ~ Sam Derbyshire. #Haskell #FunctionalProgramming
Custom type errors using TypeError. ~ Richard Eisenberg (@RaeHaskell). #Haskell #FunctionalProgramming
Co-Applicative programming style. ~ Gabriella Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
Using program synthesis and inductive logic programming to solve Bongard problems. ~ Atharv Sonwane, Sharad Chitlangia, Tirtharaj Dash, Lovekesh Vig, Gautam Shroff, Ashwin Srinivasan. #MachineLearning #ILP

20-Oct-21

Initial and final encodings of free monads. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming #ITP #Coq
The graphs game, version 0.1. ~ Barrie Cooper. #ITP #LeanProver #Math
Mathematical Logic, Lecture 10 (Axiomatizability and the diagram method). ~ Artem Chernikov (@archernikov). #Logic #Math
TrieMap that match (a programming pearl). ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
Competitive programming in Haskell: BFS, part 2 (alternative APIs). ~ Brent Yorgey. #Haskell #FunctionalProgramming
Is the twin prime conjecture independent of Peano Arithmetic? ~ Alessandro Berarducci, Antongiulio Fornasiero. #Logic #Math
Teaching notes, slides, & handouts. ~ Colin McLear (@mclearc). #Emacs #OrgMode

19-Oct-21

Efficient extensional binary tries. ~ Andrew Appel, Xavier Leroy. #ITP #Coq
Toward SMT-based refinement types in Agda. ~ Gan Shen, Lindsey Kuper. #ITP #Agda #FunctionalProgramming
Toward hole-driven development with Liquid Haskell. ~ Patrick Redmond, Gan Shen, Lindsey Kuper. #Haskell #LiquidHaskell #FunctionalProgramming
Template Haskell — Use cases. #Haskell #FunctionalProgramming
Naive descriptive set theory. ~ M. Foreman. #SetTheory
Mathematical Logic, Lecture 1 (First-order logic: languages, structures and formulas). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 2 (Semantics of first-order formulas). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 3 (Substitution of terms into formulas). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 4 (Universally valid formulas and propositional calculus). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 5 (Formal proofs). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 6 (More on formal proofs and Gödel’s completeness theorem). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 7 (Proof of Gödel’s completeness theorem). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 8 (Finishing the proof of Gödel’s completeness theorem). ~ Artem Chernikov (@archernikov). #Logic #Math
Mathematical Logic, Lecture 9 (Model theory: compactness, Löwenheim-Skolem, elementary substructure). ~ Artem Chernikov (@archernikov). #Logic #Math
UCLA Math 220A, Mathematical Logic.~ Artem Chernikov (@archernikov). #Logic #Math

18-Oct-21

Haskell Lenses From Scratch. #Haskell #FunctionalProgramming

16-Oct-21

Correct by construction language implementations. ~ Arjen Rouvoet (@ArjenRouvoet). #PhD_Thesis #ITP #Agda #FunctionalProgramming via @PerezJorgeA_
Verification for dummies: SMT and induction. ~ Adrien Champion. #eBook #Logic #SMT #FormalVerification
OCaml Programming: Correct + Efficient + Beautiful. ~ Michael R. Clarkson et als. #eBook #OCaml #FunctionalProgramming
Un parser en una docena de lineas en Haskell. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming

15-Oct-21

New year, new teaching material. ~ Kevin Buzzard. #ITP #LeanProver #Math
Competitive programming in Haskell: BFS, part 1. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Denotational homomorphic testing. ~ Divesh Otwani. #Haskell #FunctionalProgramming
La conjetura diabólica. ~ Juan Arias de Reyna. #Matemáticas
Advice for aspiring bloggers. ~ Gabriella Gonzalez (@GabrielG439). #Blogs

14-Oct-21

Proving correctness of a Chez Scheme compiler pass. ~ Ian Atol. #MSc_Thesis #ITP #Coq

12-Oct-21

Introduction to University Mathematics 2021: Logic in Lean, video 3 (and, or, iff). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic #Math
Proof theory, proof search, and logic programming. ~ Dale Miller. #eBook #Logic #LogicProgramming
Experiences from exporting major proof assistant libraries. ~ Michael Kohlhase, Florian Rabe. #ITP #HOL_Light #Coq #IsabelleHOL #IMPS #PVS #Mizar
When Alan Turing and Ludwig Wittgenstein discussed the liar paradox. ~ Paul Austin Murphy. #Logic #Math
copy-as-org-mode: A Firefox Add-on (WebExtension) to copy selected web page into Org-mode formatted text!. #Emacs #OrgMode #Firefox

11-Oct-21

Haskelling in Hackerrank!!: Episode 1: Competitive coding. #Haskell #FunctionalProgramming
Haskelling in Hackerrank!!: Episode 2: Mini-Max Sum. #Haskell #FunctionalProgramming

10-Oct-21

Logic programming for XAI: A technical perspective. ~ Laura State. #LogicProgramming #AI #XAI
Kernels and small quasi-kernels in digraphs. ~ Allan van Hulst. #ITP #Coq #Math
Mechanizing second-order logic in Coq. ~ Mark Koch. #BSc_Thesis #ITP #Coq #Logic #Math

08-Oct-21

Formalizing geometric algebra in Lean. ~ Eric Wieser, Utensil Song. #ITP #LeanProver #Math
Introduction to University Mathematics 2021: Logic in Lean, video 2 (true, false, not). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic #Math
Tuple Prelude. ~ Mitchell Vitez. #Haskell #FunctionalProgramming

07-Oct-21

An overview of functional reactive programming. ~ F. Kockelke. #FunctionalProgramming #Haskell

05-Oct-21

Soundness and completeness of an axiomatic system for first-order logic (in Isabelle/HOL). ~ Asta Halkjær From. #ITP #IsabelleHOL #Logic #Math
Learning to reason. ~ Fredrik Rømming. #Logic #ATP #MachineLearning
Logic in Lean, video 1. ~ Kevin Buzzard. #ITP #LeanProver #Logic

03-Oct-21

Mathlib statistics. #ITP #LeanProver #Math
Isabelle’s AFP statistics. #ITP #IsabelleHOL #Math

02-Oct-21

This month in mathlib (Sep 2021). ~ Mathlib community. #ITP #LeanProver #Math
Testing the Red-Black tree implementation of the Linux kernel against a formally verified variant. ~ Mete Polat. #ITP #IsabelleHOL
Verified Lustre normalization with node subsampling. ~ Timothy Bourke, Paul Jeanmaire, Basile Pesin, Marc Pouzet. #ITP #Coq

01-Oct-21

A verified online monitor for metric temporal logic with quantitative semantics. ~ Agnishom Chattopadhyay. #ITP #Coq
How to market Haskell to a mainstream programmer. ~ Gabriella Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
Nested strict data in Haskell. ~ Tom Ellis. #Haskell #FunctionalProgramming

September 2021

30-Sep-21

Specification and verification of a transient stack. ~ A. Moine, A. Charguéraud, F. Pottier. #ITP #Coq
A verified algebraic representation of Cairo program execution. ~ Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titleman. #ITP #LeanProver
Meta-metaprogramming. ~ James Koppel. #PhD_Thesis #Haskell #FunctionalProgramming
Structures algébriques fondamentales (Définitions, constructions et propriétés universelles). ~ Patrick Massot. #eBook #Math
A new medium for communicating research on programming languages. ~ Will Crichton. #CompSci
Can you make heterogeneous lists in Haskell? Sure — as long your intent is clear. ~ Laurent P. René de Cotret. #Haskell #FunctionalProgramming

29-Sep-21

Using lens to set a value based on another. ~ Magnus Therning. #Haskell #FunctionalProgramming
A short overview of typed template Haskell. ~ Heitor Toledo Lassarote de Paula. #Haskell #FunctionalProgramming
Not another computer algebra system: Highlighting wxMaxima in calculus. ~ N. Karjanto, H. S. Husain. #CAS #Math

28-Sep-21

Automated, efficient, and sound verification of integer multipliers. ~ Mertcan Temel. #PhD_Thesis #ITP #ACL2
Making LLVM GEP safer in Haskell. ~ Luc Tielen (@luctielen). #Haskell #FunctionalProgramming
Abstraction, reasoning and deep learning: A Study of the “Look and Say” sequence. ~ Wlodek W. Zadrozny. #AI #MachineLearning #Math
Use Emacs for systems thinking. ~ Junji Zhi. #Emacs #OrgMode

27-Sep-21

The Radon-Nikodym theorem in Lean. ~ Kexing Ying. #ITP #LeanProver #Math
A formalization of weighted path orders and recursive path orders (in Isabelle/HOL). ~ Christian Sternagel, René Thiemann. #ITP #IsabelleHOL
Category theory ilustrated: Logic. ~ Boris Marinov (@AlexanderKatt). #CategoryTheory #Logic #Math

26-Sep-21

What the industrial coder misses. ~ Zoltán Tóth. #eBook #Haskell #FunctionalProgramming
Big missing undergraduate theorems (in Lean mathlib). ~ Patrick Massot. #ITP #LeanProver #Math

25-Sep-21

A certified library of ordinal arithmetic. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #Logic #Math #SetTheory
How AI can be surprisingly dangerous for the philosophy of mathematics and of science. ~ Walter Carnielli. #AI #MachineLearning #Math #ITP
A functional quantum programming language. ~ Matilda Blomqvist et als. #Haskell #FunctionalProgramming

24-Sep-21

Beyond the tactic-state automaton. ~ Daniel Selsam. #ITP #LeanProver #MachineLearning
Presentation by Jeremy Avigad at the opening of the Hoskinson Center for Formal Mathematics at CMU. ~ Jeremy Avigad. #ITP #LeanProver #Math
Conflict-driven satisfiability for theory combination: Lemmas, modules, and proofs. ~ Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar. #ATP #Logic
Lambda calculus - Step by step. ~ Helmut Brandl. #LambdaCalculus
A new programming game, Swarm. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Game
Swarm: a 2D programming and resource gathering game. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Game
Functional data pipelines with funflow2. ~ Dorran Howell, Guillaume Desforges, Vince Reuter. #Haskell #FunctionalProgramming #DataScience

23-Sep-21

The promise of formal mathematics. ~ Jeremy Avigad. #ITP #LeanProver #Math
Voting theory in the Lean theorem prover. ~ Wesley H. Holliday, Chase Norman, Eric Pacuit. #ITP #LeanProver #Math
Much ADO about failures: A fault-aware model for compositional verification of strongly consistent distributed systems. ~ W. Honoré, J. Kim, J.Y. Shin, Z. Shao. #ITP #Coq
Introducción a la programación funcional usando Haskell y Agda. ~ Camilo Chacón Sartori (@camilo_chacon_s). #ProgramaciónFuncional #Haskell #Agda
Introduction to neural network verification. ~ Aws Albarghouthi. #eBook #NeuralNetwork #MachineLearning #Logic
Trustworthy AI. ~ Jeannette M. Wing. #AI #FormalMethods
AI futures: Fact and fantasy. ~ Devdatt Dubhashi. #AI
La inteligencia artificial y la solución de problemas. ~ Juan Arias de Reyna. #IA #Matemáticas
Online course on Category theory: 4. Adjoint functors. ~ Richard E. Borcherds. #CategoryTheory
VideoArxiv: a searchable repository of links to math videos. #Math

22-Sep-21

There was no formal methods winter. ~ Hillel Wayne (@hillelogram). #FormalMethods via @LogicPractice
Connecting constructive notions of ordinals in homotopy type theory. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #ITP #Agda #Logic #Math #HoTT
Competitive programming in Haskell: Codeforces Educational Round 114. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Symmetry. ~ Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson. #eBook #Univalent_mathematics
Primos que generan primos: el teorema de Scherk. ~ M.A. Morales (@gaussianos). #Matemáticas
Online course on Category theory: 1. Introduction. ~ Richard E. Borcherds. #CategoryTheory
Online course on Category theory: 2. Functors. ~ Richard E. Borcherds. #CategoryTheory
Online course on Category theory: 3. Natural transformations. ~ Richard E. Borcherds. #CategoryTheory

21-Sep-21

The Lean 4 theorem prover and programming language (System description). ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver
Continuous partitions of unity (in Lean). ~ Patrick Massot. #ITP #LeanProver #Math
Verifying AVL trees in Lean. ~ Sofia Konovalova. #ITP #LeanProver #Algorithms
Type theory by example. ~ Carl Joshua Quines. #TypeTheory #Logic #CompSci

20-Sep-21

Closed-expression of a sum with proof in Coq. ~ Boro Sitnikovski (@BSitnikovski). #ITP #Coq #Math
Verified optimization (work in progress). ~ Alexander Bentkamp, Jeremy Avigad.f#ITP #LeanProver #Math
Complex bounded operators in Isabelle/HOL. ~ José Manuel Rodríguez Caballero, Dominique Unruh. #ITP #IsabelleHOL #Math
Learning Haskell by building a static blog generator. ~ Gil Mizrahi (@_gilmi). #eBook #Haskell #FunctionalProgramming

18-Sep-21

Automatically updated, cached views with lens. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Proof editor for natural deduction. ~ Freddy Abrahamsson, Therese Andersson, Axel Forsman, Lo Ranta, Michael Åkesson. #BSc_Thesis #Logic #PureScript #FunctionalProgramming
Natural deduction proof editor and checker. #Logic #PureScript #FunctionalProgramming
Existence of Nash equilibria in 2-player simultaneous games and priority games proven in Isabelle. ~ S Le Roux, É Martin-Dorel, JG Smaus. #ITP #IsabelleHOL #Math
Formalized soundness and completeness of epistemic logic. ~ AH From, AB Jensen, J Villadsen. #ITP #IsabelleHOL #Logic

17-Sep-21

GHC rewrite rules. ~ Jonathan Dowland. #Haskell #FunctionalProgramming
Haskell series part 4 (This is the fourth article of a series on the functional language Haskell for beginners). ~ Pierre Guillemot. #Haskell #FunctionalProgramming

16-Sep-21

Distributed knowledge proofs in the Coq proof assistant. ~ Michiel Philipse #BSc_Thesis #ITP #Coq
Univalent Mathematics: This Coq library aims to formalize a substantial body of mathematics using the univalent point of view. #ITP #Coq #Math

15-Sep-21

Infinity category theory offers a bird’s-eye view of mathematics. ~ Emily Riehl. #Math #CategoryTheory
Unprovability in mathematics: A first course on ordinal analysis. ~ Anton Freund. #Logic #Math

14-Sep-21

LISA: Language models of ISAbelle proofs. ~ Albert Q. Jiang, Wenda Li, Jesse M. Han, Yuhuai Wu. #ITP #IsabelleHOL
Category theory for ZFC in HOL I: Foundations: Design patterns, set theory, digraphs, semicategories. #ITP #IsabelleHOL #Math
Category theory for ZFC in HOL II: Elementary theory of 1-categories. #ITP #IsabelleHOL #Math
Category theory for ZFC in HOL III: Universal constructions. #ITP #IsabelleHOL #Math
Extension of types-to-sets. #ITP #IsabelleHOL #Math
IDE: Introduction, destruction, elimination. #ITP #IsabelleHOL #Math
Conditional transfer rule. #ITP #IsabelleHOL #Math
Conditional simplification. #ITP #IsabelleHOL #Math
Como está hecho este blog. #Emacs #OrgMode
My experience with book writing. ~ Marcin Borkowski (@marcin_mbork). #Emacs #OrgMode #Elisp
Modelling and verifying dynamic properties of neuronal networks in Coq. ~ Abdorrahim Bahrami. #PhDThesis #ITP #Coq #NeuralNetwork
Penrose kite and dart tilings with Haskell Diagrams. ~ Chris Reade. #Haskell #FunctionalProgramming #Math

13-Sep-21

Mining counterexamples for wide-signature algebras with an Isabelle server. ~ Boris Shminke, Wesley Fussner. #ITP #IsabelleHOL
Symbolic computation in software science: My personal view. ~ Bruno Buchberger. #CompSci
Proceedings 18th International Conference on Quantum Physics and Logic. #Logic #Math #Physics

12-Sep-21

Hasse derivative of polynomials (in Lean).~ Johan Commelin. #ITP #LeanProver #Math
Taylor expansions of polynomials (in Lean). ~ Johan Commelin. #ITP #LeanProver #Math
A survey of practical formal methods for security. ~ Tomas Kulik et als. #FormalMethods

11-Sep-21

Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
GSOL: A confluence checker for Haskell rewrite rules. ~ Yao Faustin Date Makoto Hamana. #Haskell #FunctionalProgramming
Announcing Evoke, a GHC plugin for deriving type class instances quickly. ~ Taylor Fausak (@taylorfausak). #Haskell #FunctionalProgramming
Deferred derivation. ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming
Symbolic computation and Common Lisp. ~ Neil T. Dantam. #CommonLisp
New math book rescues landmark topology proof. ~ Kevin Hartnett (@KSHartnett). #Math

10-Sep-21

Implementing Hindley-Milner with the unification-fd library. ~ Brent Yorgey. #Haskell #FunctionalProgramming
An introduction to type level programming. ~ Rebecca Skinner. #Haskell #FunctionalProgramming
Optics for the working mathematician. ~ Bartosz Milewski (@BartoszMilewski). #CategoryTheory
Leibniz coercion. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming

09-Sep-21

Learned provability likelihood for tactical search. ~ Thibault Gauthier. #ITP #HOL4 #MachineLearning
Conjectures, tests and proofs: An overview of theory exploration. ~ Moa Johansson, Nicholas Smallbone. #Haskell #FunctionalProgramming
Vinyl-style extensible graphs. ~ Daniel Firth. #Haskell #FunctionalProgramming
Optics are monoids. ~ Gabriella Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
Competitive programming in Haskell: Kadane’s algorithm. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Leibniz equality in Haskell, part 2: heterogeneous equality. ~ Ryan Scott. #Haskell #FunctionalProgramming
Cayley representation of … monads? ~ Konrad Kleczkowski. #Haskell #FunctionalProgramming

08-Sep-21

A data flow analysis algorithm for computing dominators (in Isabelle/HOL). ~ Nan Jiang. #ITP #IsabelleHOL
Inductive and coinductive predicate liftings for effectful programs. ~ Niccolò Veltri, Niels Voorneveld. #ITP #Agda
Mutating lenses. ~ Tarmean. #Haskell #FunctionalProgramming
How dependent Haskell can improve industry projects. ~ Danya Rogozin, Vladislav Zavialov. #Haskell #FunctionalProgramming

07-Sep-21

Two mechanisations of WebAssembly 1.0. ~ Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin, Philippa Gardner. #ITP #IsabelleHOL #Coq
A reasoning engine for the gamification of loop-invariant discovery. ~ Andrew Walter, Seth Cooper, Panagiotis Manolios. #ATP #ACL2 #Program_verification
Course: Logic Programming (2020-2021). ~ Manuel Hermenegildo et als. #LogicProgramming #Prolog

06-Sep-21

Schutz’ independent axioms for Minkowski spacetime (in Isabelle/HOL). Richard Schmoetten, Jake Palmer, Jacques Fleuriot. #ITP #IsabelleHOL #Math
Vandermonde’s identity (in Lean). ~ Johan Commelin. #ITP #LeanProver #Math
A survey of the proof-theoretic foundations of logic programming. ~ Dale Miller. #LogicProgramming

05-Sep-21

Creating Haskell notebooks with org-mode. ~ Laura Viglioni (@LauraViglioni). #Emacs #OrgMode #Haskell #FunctionalProgramming
Embedded pattern matching. ~ Trevor L. McDonell, Joshua D. Meredith, Gabriele Keller. #Haskell #FuncionalProgramming

04-Sep-21

On the role of automated proof-assistants in the formalization of upper ontologies. ~ João R. M. Nicola, Giancarlo Guizzardi. #ITP #IsabelleHOL
Programming with proofs. ~ Thorsten Altenkirch. #ITP #Agda #FunctionalProgramming
The design of mathematical language. ~ Jeremy Avigad. #Logic #Math
Parsing layout, or: Haskell’s syntax is a mess. ~ Abigail (@plt_abbie). #Haskell #FunctionalProgramming
Why fintech companies use Haskell. ~ Roman Alterman. #Haskell #FunctionalProgramming
Dependent optics. ~ Bartosz Milewski (@BartoszMilewski). #FunctionalProgramming #CategoryTheory

03-Sep-21

Solving cubic and quartic equations (in Isabelle/HOL). ~ René Thiemann. #ITP #IsabelleHOL #Math
Family values. ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming

02-Sep-21

A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory. ~ Andreas Lochbihler. #ITP #IsabelleHOL #Math
Inverse function theorem. Part I. ~ K. Nakasho, Y. Futa. #ITP #Mizar #Math
Elementary number theory problems. Part II. ~ A. Korniłowicz, D. Surowik. #ITP #Mizar #Math
Derivation of commutative rings and the Leibniz formula for power of derivation. ~ Y. Watase, S. Matsunoki. #ITP #Mizar #Math
Algebraic extensions. ~ C. Schwarzweller, A. Rowińska-Schwarzweller. #ITP #Mizar #Mat #ITP #Mizar #Math
Miscellaneous graph preliminaries. Part I. ~ S. Koch. #ITP #Mizar #Math
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ~ Kunhao Zheng, Jesse Michael Han, Stanislas Polu. #ITP #LeanProver #IsabelleHOL #Metamath #Math
Theorem proving in Lean 4. #ITP #LeanProver
From Euclid to Hilbert to Lean. ~ Tianchen Zhao. #ITP #LeanProver #Math
Formalising nilpotent groups in Lean. ~ Ines Wright. #ITP #LeanProver #Math
Formalising the fundamental group. ~ Shing Tak Lam. #ITP #LeanProver #Math
Proving Dedekind’s Theorem in Lean. ~ Paul Lezeau. #ITP #LeanProver #Math
Formalizing Thomae’s function in Lean. ~ Frick Hazard. #ITP #LeanProver #Math
Ax-Grothendieck theorem in Lean. ~ Joseph Hua. #ITP #LeanProver #Math
Conformal maps, Liouville’s theorem and random stuffs in Lean. ~ Yourong Zang. #ITP #LeanProver #Math
Probability in Lean: a new begnining. ~ Kexing Ying. #ITP #LeanProver #Math
Combinatorial design theory in Isabelle/HOL. ~ Chelsea Edmonds, Lawrence Paulson. #ITP #IsabelleHOL

01-Sep-21

Formally verified defensive programming (efficient Coq-verified computations from untrusted ML oracles). ~ Sylvain Boulmé. #ITP #Coq #OCaml #FunctionalProgramming
The theorem of three circles (in Isabelle/HOL). ~ Fox Thomson, Wenda Li #ITP #IsabelleHOL #Math
Dependency analysis of Haskell declarations. ~ Artem Kuznetsov. #Haskell #FunctionalProgramming

August 2021

31-Aug-21

New Software Foundations release. ~ Benjamin C. Pierce et als. #ITP #Coq
Modal logic S5 satisfiability in answer set programming. ~ Mario Alviano,a Sotiris Batsakis, George Baryannis. #Logic #ASP #LogicProgramming
The Dao of Functional Programming (Last updated: August 30, 2021). ~ Bartosz Milewski (@BartoszMilewski). #Haskell #FunctionalProgramming #CategoryTheory
HIW (The Haskell Implementors’ Workshop) 2021 videos. #Haskell #FunctionalProgramming
A data-centered user study for proof assistant tools. ~ Hanneli C.A. Tavante. #ITP #Coq#LeanProver
Latent effects for reusable language components: Extended version. ~ Birthe van den Berg, Tom Schrijvers, Casper Bach-Poulsen, Nicolas Wu. #Haskell #FunctionalProgramming
Formalising algebraic effects with non-recoverable failure. ~ Timotej Tomandl, Dominic Orchard. #Haskell #FunctionalProgramming
Sound and automated verification of real-world RTL multipliers. ~ Mertcan Temel, Warren A. Hunt Jr. #ITP #ACL2

30-Aug-21

Computer algebra in Julia. ~ Dmitry S. Kulyabov, Anna V. Korolkova. #CAS #JuliaLang #Math
Dijkstra: O homem que tornou a computação uma ciência. ~ Adriano Santos (@adrianolcp). #CompSci

29-Aug-21

What is category theory and why is it trendy? ~ Katerina Hristova. #Math #CategoryTheory

28-Aug-21

Geometry in Lean, a report for mathematicians. ~ Nicolò Cavalleri, Anthony Bordg. #ITP #LeanProver #Math
Formalizing the Gromov-Hausdorff space. ~ Sébastien Gouëzel. #ITP #LeanProver #Math

27-Aug-21

Leibniz equality in Haskell, part 1. ~ Ryan Scott. #Haskell #FunctionalProgramming
Magical Haskell (modern functional programming and type theory in a fun and accessible way). ~ Anton Antich (@aantich). #Haskell #FunctionalProgramming #eBook
Nascent GHC proposal: Source rewrite rules and optional constraints. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming
Life as a logician (An interview with Martin Davis by Allyn Jackson). #Logic #Math #CompSci #AI #MachineLearning

26-Aug-21

Une idée assez folle, l’Intelligence Artificielle … (un film sur le parcours d’Alain Colmerauer). #AI #LogicProgramming #Prolog

25-Aug-21

Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. ~ Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
Scalar actions in Lean’s mathlib. ~ Eric Wieser. #ITP #LeanProver #Math
AI ethics: A call to faculty. ~ Illah Reza Nourbakhsh. #AI

24-Aug-21

Multiplicative induction principles for ℕ. ~ Eric Rodriguez. #ITP #LeanProver #Math

23-Aug-21

Formalizing Fibonacci squares. ~ Harun Khan. #ITP #LeanProver #Math
Programación literaria para sysadmins / devops. ~ drymer. #Emacs #OrgMode

21-Aug-21

Faster smarter proof by induction in Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL
Formalization in Lean of IMO 2006 Q3. ~ Tian Chen. #ITP #LeanProver #Math #IMO
Verifying C11-style weak memory libraries via refinement. ~ Sadegh Dalvandi, Brijesh Dongol. #ITP #IsabelleHOL

20-Aug-21

The design of mathematical language. ~ Jeremy Avigad. #Logic #Math
Verified optimization. ~ Alexander Bentkamp, Jeremy Avigad. #ITP #LeanProver #Math
Automatically generalizing theorems using typeclasses. ~ Alexander Best. #ITP #LeanProver
Formal ML: A LEAN library for proving foundational results in measure theory, probability, statistics, and machine learning, based upon mathlib. #ITP #LeanProver #Math #MachineLearning

19-Aug-21

Formalization of Ostrowski theorems in Lean theorem prover. ~ Ryan Lahfad†, Julien Marquet, Hadrien Barral. #ITP #LeanProver #Math
On correctness and completeness of an n queens program. ~ Włodzimierz Drabent. #LogicProgramming #Prolog
Colisiones matemáticas que muestran cómo confundir al algoritmo Neural Hash. ~ @Alvy. #AI #MachineLearning
XAI methods for neural time series classification: A brief review. ~ Ilija Šimić, Vedran Sabol, Eduardo Veas. #DeepLearning #XAI
A framework for understanding AI-induced field change: How AI technologies are legitimized and institutionalized. ~ Benjamin Cedric Larsen. #AI
A first course in Artificial Intelligence. ~ Osondu Oguike #eBook #AI

18-Aug-21

Machine learning and the continuum hypothesis (How the unprovable concerns the unlearnable). ~ Robert Passmann. #MachineLearning #Math
Announcing Spectacle – A language for writing and checking formal specifications in Haskell. ~ Jacob Leach. #Haskell #FunctionalProgramming

17-Aug-21

The Oxford Invariants Puzzle Challenges (Summer 2021, Week 3, Problem 1) in Lean. ~ Yaël Dillies, Bhavik Mehta. #ITP #LeanProver #Math

16-Aug-21

Ideas that created the future: Classic papers of Computer Science. ~ Harry R. Lewis. #eBook #CompSci
Core Haskell tools. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming
How Lisp became God’s own programming language. ~ @TwoBitHistory. #Lisp #Programming
Natural deduction calculus for first-order logic. ~ Yazeed Alrubyli. #Logic #Math

14-Aug-21

Assimilating the structure of formal and informal proof. ~ Kensho Tsurusaki, Akiko Aizawa. #ITP #LeanProver
Balancing the formal and the informal in user-centred design. ~ JC Campos, MD Harrison, P Masci. #ITP #PVS
Extracting functional programs from Coq, in Coq. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq
Formal methods for security knowledge area. ~ David Basin. #FormalMethods
HaskellFL: A tool for detecting logical errors in Haskell. ~ Vanessa Vasconcelos, Mariza A. S. Bigonha. #Haskell #FunctionalProgramming
Abstraction in Reflex and CodeWorld. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld #FunctionalProgramming
That one cool reader trick. ~ Solomon. #Haskell #FunctionalProgramming
Namespaced De Bruijn indices. ~ Gabriella Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
Deep Learning: A critical appraisal. ~ Gary Marcus. #DeepLearning
A functional reboot for Deep Learning. ~ Conal Elliott (@conal). #DeepLearning #FunctionalProgramming #Haskell
Symbolic and automatic differentiation of languages. ~ Conal Elliott (@conal). #Agda #FunctionalProgramming

13-Aug-21

What is the point of Lean’s maths library? ~ Kevin Buzzard. #ITP #LeanProver #Math
Counting cardinalities. ~ Mitchell Vitez. #Haskell #FunctionalProgramming

12-Aug-21

Skipping the binder bureaucracy with mixed embeddings in a semantics course (Functional Pearl). ~ Adam Chlipala. #ITP #Coq
The Hoare State Monad (Proof Pearl). ~ Wouter Swierstra. #ITP #Coq
Competitive programming in Haskell: monoidal accumulation. ~ Brent Yorgey. #Haskell #FunctionalProgramming

11-Aug-21

Formalization in Lean of IMO 2001 Q6. ~ Sara Díaz, Johan Commelin. #ITP #LeanProver #Math #IMO

10-Aug-21

Reasoning about iteration and recursion uniformly based on big-step semantics. ~ Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan. #ITP #Coq
A secure and formally verified commodity multiprocessor hypervisor. ~ Shih-Wei Li. #PhD_Thesis #ITP #Coq
Kronecker product of matrices (in Lean). ~ Filippo A. E. Nuccio, Eric Wieser. #ITP #LeanProver #Math
Depth-first and breadth-first search in Haskell. ~ Malvin Gattinger (@m4lvin). #Haskell #FunctionalProgramming
Left and right folds (Comparison of a mathematical definition and a programmatic one). ~ Philip Schwarz (@philip_schwarz). #Haskell #Scala #FunctionalProgramming
Elementary recursive algorithms. ~ Yiannis N. Moschovakis. #Algorithms #Logic #Math #CompSci

09-Aug-21

Extracting functional programs from Coq, in Coq. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq
A toy WASM symbolic interpreter. ~ Simon Marechal et als. #Haskell #FunctionalProgramming

08-Aug-21

Relational forests (in Isabelle/HOL). ~ Walter Guttmann. #ITP #IsabelleHOL

07-Aug-21

Theorem proving in classical logic. ~ David Davies. #Haskell #FunctionalProgramming #Logic
Automatically generalizing theorems using typeclasses. ~ Alex J. Best. #ITP #LeanProver
A brief intro to monad transformers. ~ Solomon. #Haskell #FunctionalProgramming
Elements of differential geometry in Lean: A report for mathematicians. ~ Anthony Bordg, Nicolò Cavalleri. #ITP #LeanProver #Math

06-Aug-21

Plotting in a formally verified way. ~ Guillaume Melquiond. #ITP #Coq
Edukera: Teach Logic and Math with a proof assistant. #ITP #Coq #Edukera #Logic #Math
Archetype, a DSL for Tezos. ~ Benoit Rognier. #ITP #Coq #Edukera #Archetype
A logic theory pattern for linearized control systems. ~ Andrea Domenici, Cinzia Bernardeschi. #ITP #PVS
Verifying time complexity of binary search using Dafny. ~ Shiri Morshtein, Ran Ettinger, Shmuel Tyszberowicz. #ATP #FormalVerification #Dafny
Explaining counterexamples with giant-step assertion checking. ~ Benedikt Becker, Cláudio Belo Lourenço, Claude Marché. #ATP #Why3 #FormalVerification
VeriFly: On-the-fly assertion checking with CiaoPP (extended abstract). ~ Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, Víctor Pérez, Jose F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo./#EPTCS338.13 #Prolog #CiaoPP
Haskell for the Elm enthusiast. ~ No Red Ink. #Haskell #Elm #FunctionalProgramming
Haskell series part 2 (This is the second article of a series on the functional language Haskell for beginners). ~ Pierre Guillemot. #Haskell #FunctionalProgramming
fromMaybe is Just a fold. ~ Dan Soucy (@ninedotnine). #Haskell #FunctionalProgramming
When Howard Met Curry. ~ Rob Rix (@rob_rix). #Haskell #FunctionalProgramming

05-Aug-21

Axiomatic Minkowski spacetime in Isabelle/HOL. ~ Richard Schmoetten. #MSc_Thesis #ITP #IsabelleHOL
Archive of Formal Proofs. #ITP #IsabelleHOL
Archive of Formal Proofs redesign. ~ Carlin MacKenzie. #ITP #IsabelleHOL

04-Aug-21

Lean proof of Thomaes (popcorn) function. ~ Ender Doe. #ITP #LeanProver #Math

03-Aug-21

Proof and computation: Perspectives for mathematics, computer science, and philosophy. ~ Klaus Mainzer. #Logic #Math #CompSci #ITP
Oblivious Algebraic Data Types. ~ Qianchuan Ye, Benjamin Delaware. #ITP #Coq
GHC curiosities: Equality constraints in kinds. ~ Ryan Scott. #Haskell #FunctionalProgramming

02-Aug-21

Egglog 2: Automatically proving the pullback of a monic is monic. ~ Philip Zucke. #CategoryTheory
Writing academic papers with org-mode. ~ Wouter Spekkink (@wouterspekkink). #Emacs #OrgMode
Tying shoes with GADTs. ~ MorrowM. #Haskell #FunctionalProgramming

July 2021

31-Jul-21

Formalisation of interval methods for nonlinear root-finding. ~ Daniel Seidl. #BSc_Thesis #ITP #IsabelleHOL #Math
New algebraic normative theories for ethical and legal reasoning in the LogiKEy framework. ~ Ali Farjami. #ITP #IsabelleHOL
The categorical origin of monads in Haskell. ~ Marien Matser. #BSc_Thesis #Haskell #FunctionalProgramming #CategoryTheory
What separates AI from an idiot savant is common sense: Hector Levesque. #AI #KRR
Computer theorem prover verifies sophisticated new result. ~ David H Bailey. #ITP #ATP #Math #AI

30-Jul-21

Ethical AI for Social Good. ~ Ramya Akula, Ivan Garibay. #AI
Composable data validation with Haskell. ~ Ben Levy, Christian Charukiewicz. #Haskell #FunctionalProgramming
Ode to a streaming ByteString (Or: lazy I/O without shooting yourself in the foot). ~ Patrick Thomson. #Haskell #FunctionalProgramming
Strictness of foldr’ from containers. ~ Marcin Szamotulski (@me_coot). #Haskell #FunctionalProgramming
Formalization of Gambler’s Ruin Problem in Isabelle/HOL. ~ Zibo Yang. #ITP #IsabelleHOL #Math
Formalization of RBD-based Cause Consequence Analysis in HOL. ~ Mohamed Abdelghany, Sofiene Tahar. #ITP #HOL4
Inductive Benchmarks for Automated Reasoning. ~ Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov. #ATP
Formalizing the Gromov-Hausdorff Space. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
Formalizing rotation number and its properties in Lean. ~ Yury Kudryashov. #ITP #LeanProver #Math
Scalar actions in Lean’s Mathlib. ~ Eric Wieser. #ITP #LeanProver #Math

29-Jul-21

A formalization of the (compositional) Z property. ~ Flávio L. C. de Moura,a Leandro O. Rezende. #ITP #Coq
Confluence via the Z property in Coq. ~ Flávio L. C. de Moura, Leandro O. Rezende. #ITP #Coq
The who in explainable AI: How AI background shapes perceptions of AI explanations. ~ Upol Ehsan, Samir Passi, Q. Vera Liao, Larry Chan, I-Hsiang Lee, Michael Muller, Mark O. Riedl. #AI #XAI
The QED Manifesto. #ATP #ITP
Proof assistant makes jump to big-league Math. ~ Kevin Hartnett (@KSHartnett). #ITP #LeanProver #Math
Integrating an automated prover for projective geometry as a new tactic in the Coq proof assistant. ~ Nicolas Magaud. #ITP #Coq #Math
Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? ~ Zoltán Kovács, Tomás Recio, Robert Vajda, M. Pilar Vélez. #GeoGebra #Math
[[https://www.researchgate.net/profile/Zoltan-Kovacs-3/publication/353466393_Is_computer_algebra_ready_for_conjecturing_and_proving_geometric_inequalities_in_the_classroom/links/60ff0d602bf3553b29142ca4/Is-computer-algebra-ready-for-conjecturing-and-proving-geometric-inequalities-in-the-classroom.pdf?origin=homeFeed_download&_iepl%5BactivityId%5D=1396227761647622&_iepl%5BactivityTimestamp%5D=1627257600&_iepl%5BactivityType%5D=person_publish_publication&_iepl%5Bcontexts%5D%5B0%5D=homeFeed&_iepl%5BrecommendationActualVariant%5D=&_iepl%5BrecommendationDomain%5D=&_iepl%5BrecommendationScore%5D=&_iepl%5BrecommendationTargetActivityCombination%5D=&_iepl%5BrecommendationType%5D=&_iepl%5BfeedVisitIdentifier%5D=&_iepl%5BpositionInFeed%5D=11&_iepl%5BsingleItemViewId%5D=KUZ4i5ThvdxaoZf1ctK2jh1s&_iepl%5BviewId%5D=mkX7HMc1c9d9Y7Hyr4ISW4R9&_iepl%5BhomeFeedVariantCode%5D=ncls&_iepl%5B__typename%5D=HomeFeedTrackingPayload&_iepl%5BinteractionType%5D=publicationDownload&_iepl%5BtargetEntityId%5D=PB%3A353466393][Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? [Slides]]] ~ Zoltán Kovács, Tomás Recio, Robert Vajda, M. Pilar Vélez. #GeoGebra #Math
A formalization of properties of continuous functions on closed intervals. ~ Yaoshun Fu, Wensheng Yu. #ITP #Coq #Math
Formal analysis in Coq. #ITP #Coq #Math
GeoLogic – Graphical interactive theorem prover for Euclidean geometry. ~ Miroslav Olsak. #ITP #Logic #Math
GeoLogic: Tool for euclidean geometry aware of logic. ~ Miroslav Olsak. #ITP #Logic #Math

27-Jul-21

Case studies in formal reasoning about lambda-calculus: Semantics, Church-Rosser, standardization and HOAS. ~ Lorenzo Gheri, Andrei Popescu. #ITP #IsabelleHOL
An introduction to the Naproche natural language proof checker. ~ Peter Koepke. #ITP #IsabelleHOL #Naproche #Logic #Math
Intuitionistic epistemic logic in Coq. ~ Christian Albert Hagemeier. #BSc_Thesis #ITP #Coq #Logic
What does saying that ‘Programming is hard’ really say, and about whom? ~ Brett A. Becker. #Programming

26-Jul-21

Formalization in Lean of IMO 2021 Q1. ~ Mantas Baksys. #ITP #LeanProver #Math #IMO
Formalizing Galois theory (in Lean). ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math
Hakyll how-to: pages without source files. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming
Why math is an art, not a science. ~ Peter Flom. #Math

25-Jul-21

Combinatorics in Lean. ~ Bhavik Mehta. #ITP #LeanProver #Math
First-order languages and structures in Lean. ~ Aaron Anderson, Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Logic #Math
Schur–Zassenhaus theorem in Lean. ~ Thomas Browning. #ITP #LeanProver #Math
Univalence from a computer science point-of-view. ~ Dan Licata. #Logic #Math #CompSci
Haskell (The most gentle introduction ever). ~ Mateusz Podlasin (@m_podlasin). #Haskell #FunctionalProgramming
A comparison of the mathematical proof languages Mizar and Isar. ~ Freek Wiedijk, Markus Wenzel. #ITP #Mizar #IsabelleHOL #Isar
The mathematical vernacular. ~ Freek Wiedijk. #ITP #Mizar #IsabelleIsar
The Krein-Milman theorem in Lean. ~ Yaël Dillies. #ITP #LeanProver #Math
Sets and logic in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Logic #Math
Functions and equivalence relations in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Logic #Math
A computer verified, monadic, functional implementation of the integral. ~ Russell O’Connor, Bas Spitters. #ITP #Coq #Math

24-Jul-21

Static analysis using Haskell and Datalog. ~ Luc Tielen (@luctielen). #Haskell #FunctionalProgramming
`forall`s in Data Types. ~ Brandon Chinn. #Haskell #FunctionalProgramming

23-Jul-21

Every group is a McCune group (in Lean). ~ Bhavik Mehta. #ITP #LeanProver #Math

22-Jul-21

Balancing automation and control for formal verification of microprocessors. #ITP #ACL2
Learning theorem proving components. ~ Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban. #ATP #MachineLearning
Connecting constructive notions of ordinals in Homotopy Type Theory. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #HoTT #ITP #Agda #Logic #Math
Artificial intelligence (A textbook). ~ Charu C. Aggarwal.3#v=onepage&q&f=false #eBook #AI

21-Jul-21

Announcing a new newsletter on mechanizing mathematics. ~ Michael Harris. #ITP #ATP #Math
Silicon Reckoner: an opinionated newsletter about the implications of mechanization of mathematics. ~ Michael Harris. #ITP #ATP #Math

20-Jul-21

IsaSAT and Kissat entering the EDA Challenge 2021. ~ Mathias Fleury. #ITP #IsabelleHOL #SATSolvers
Waterproof: an educational environment for writing mathematical proofs in interactive notebooks. #ITP #Coq #Math
Measure theory in Waterproof (Interactive theorem-proving for measure theory in an educational setting). ~ Jan Moraal. #ITP #Coq #Math
Compositional optimizations for CertiCoq. ~ Zoe Paraskevopoulou, John M. Li, Andrew W. Appel. #ITP #Coq
Noetherian induction for computer-assisted first-order reasoning. ~ Sorin Stratulat. #ITP #Coq #Logic #Math
Verification of linked data structures in Dafny. ~ Jorge Blázquez Saborido. #TFG #ATP #SMT #Dafny
Probability tree diagrams. Recursion schemes. Why finding the right solution is sometimes hard? ~ Robert Peszek. #Haskell #FunctionalProgramming
Purely-functional reverse-mode automatic differentiation with delimited continuations. ~ Marco Zocca (@ocramz_yo). #Haskell #FunctionalProgramming
Proceedings of ICML 2021 workshop on theoretic foundation, criticism, and application trend of explainable AI. #AI #MachineLearning #XAI

19-Jul-21

Publishing articles and books with Org Mode export. ~ Peter Prevos (@pprevos). #Emacs #OrgMode #LaTeX

18-Jul-21

The Hales-Jewett theorem (in Lean). ~ David Wärn. #ITP #LeanProver #Math
Emacs, el editor de texto libre con vocación de sistema operativo: sus ‘extensiones’ más usadas suplen toda clase de aplicaciones. ~ Marcos Merino (@MarcosMerino_B). #Emacs
Of all the programming languages in the world, why Haskell? ~ Charles Hoskinson. #Haskell #FunctionalProgramming #Cardano
Emacs Application Framework (EAF). #Emacs

17-Jul-21

Incremental vulnerability detection via back-propagating symbolic execution of insecurity separation logic. ~ Toby Murray, Pengbo Yan, Gidon Ernst. #ITP #IsabelleHOL
Integrating an automated prover for projective geometry as a new tactic in the Coq proof assistant. ~ Nicolas Magaud. #ITP #Coq #Math
Reasoning on figures of theoretical geometry theorems. ~ Eirini Vandorou. #MSc_Thesis #Clojure #FunctionalProgramming #Prolog #LogicProgramming #Math
Hspec hooks. ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming
Distributing intersection and union types with splits and duality (Functional pearl). ~ Xuejing Huang, Bruno C.D.S. Oliveira. #Haskell #FunctionalProgramming
A defense of logicism. ~ Hannes Leitgeb, Uri Nodelman, Edward N. Zalta. #Logic #Math

16-Jul-21

Facilitating meta-theory reasoning. ~ Giselle Reis. #Logic #CompSci #SELLF #TATU #QUATI #OCaml #FunctionalProgramming
Touring the MetaCoq project. ~ Matthieu Sozeau. #ITP #Coq
Automating induction by reflection. ~ Johannes Schoisswohl, Laura Kovács. #ATP #Logic
Automated induction by reflection. ~ Johannes Schoisswohl. #MSc_Thesis #ATP #Logic
Countability of inductive types formalized in the object-logic level. ~ Qinxiang Cao, Xiwei Wu. #ITP #Coq
SMLtoCoq: Automated generation of Coq specifications and proof obligations from SML programs with contracts. ~ Laila El-Beheiry, Giselle Reis, Ammar Karkour. #ITP #Coq #SML #FunctionalProgramming
Systematic translation of formalizations of type theory from intrinsic to extrinsic style. ~ Florian Rabe, Navid Roux. #MMT #LogicalFramework
A reinforcement learning environment for mathematical reasoning via program synthesis. ~ Joseph Palermo, Johnny Ye, Alok Singh. #AI #MachineLearning #Math
Explainable AI: current status and future directions. ~ Prashant Gohel, Priyanka Singh, Manoranjan Mohanty. #XAI #AI #MachineLearning
Cheap interpreter, part 4: stack machines. ~ Gary Verhaegen. #Haskell #FunctionalProgramming
Haskell series part 1. ~ Pierre Guillemot (@hnb_02). #Haskell #FunctionalProgramming
Template Haskell performance tips. ~ Matt Parsons. #Haskell #FunctionalProgramming
Artificial Intelligence, Robotics & Data Science (CSIC Scientific Challenges: Towards 2030, Volume 11). #AI #DataScience #MachineLearning

15-Jul-21

Copilot, el asistente de AI de GitHub recibió fuertes críticas de la comunidad open source. ~ Darkcrizt. #AI #Copilot #Programación
HR’s role in understanding and mitigating AI bias. ~ Laura Baldwin. #AI
(Risp (in (Rust) (Lisp))). ~ Stepan Parunashvili (@stopachka). #Rust #Lisp
Writing an (overly) idiomatic Fizzbuzz with Rust. ~ Ryan Frazier. #RustLang
Is Rust used safely by software developers? ~ Ana Nora Evans, Bradford Campbell, Mary Lou Soffa. #RustLang
Explainability and auditability in ML: Definitions, techniques, and tools. ~ Ejiro Onose. #AI #MachineLearning #XAI
Reinforcement learning for interactive theorem proving (Creating an artificial student). ~ Jolijn Cottaar. #ITP #Coq #MachineLearning
Game development in Haskell. ~ Jan Rychlý. #BSc_Thesis #Haskell #FunctionalProgramming

14-Jul-21

A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. ~ Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke. #ITP #Coq #CompSci
A classification of artificial intelligence systems for mathematics education. ~ Steven Van Vaerenbergh, Adrián Pérez-Suay. #AI #Math
GHC: Dependency analysis of Haskell declarations. ~ Artyom Kuznetsov. #Haskell #FunctionalProgramming
Finitely generated abelian groups (in Isabelle/HOL). ~ Joseph Thommes, Manuel Eberl. #ITP #IsabelleHOL #Math
Formalizing the Gromov-Hausdorff space. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
A flexible approach to argumentation framework analysis using theorem proving. ~ David Fuenmayor, Alexander Steen.f#page=26 #ITP #IsabelleHOL
Express: Applications of dynamically typed Haskell expressions. ~ Rudy Matela. #Haskell #FunctionalProgramming
Learning about proof with the theorem prover Lean: the abundant numbers task. ~ Athina Thoma, Paola Iannone. #ITP #LeanProver #Math

12-Jul-21

Haskell books: a tagged index of English books related to the Haskell programming language. ~ Travis Cardwell. #Haskell #FunctionalProgramming

11-Jul-21

General automation in Coq through modular transformations. ~ Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial. #ITP #Coq
Synthetic undecidability of MSELL via FRACTRAN mechanised in Coq. ~ Dominique Larchey-Wendling. #ITP #Coq
Type-theoretic constructions of the final coalgebra of the finite powerset functor. ~ Niccolò Veltri. #ITP #Agda
Alethe: Towards a generic SMT proof format. ~ Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine. #ATP #SMT
Conjectures, tests and proofs: An overview of theory exploration. ~ Moa Johansson, Nicholas Smallbone. #Haskell #FunctionalProgramming #QuickSpec
A framework for proof-carrying logical transformations. ~ Quentin Garchery. #FunctionalProgramming #OCaml #Why3

10-Jul-21

Isabelle’s metalogic: Formalization and proof checker. ~ Tobias Nipkow, Simon Roßkopf.f#page=104 #ITP #IsabelleHOL
Reliable reconstruction of fine-grained proofs in a proof assistant. ~ Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais.f#page=459 #ATP #SMT #ITP #IsabelleHOL
The Isabelle/Naproche natural language proof assistant. ~ Adrian De Lon et als.f#page=619 #ITP #IsabelleHOL
Turing machines in Lean. ~ Mario Carneiro et als. #ITP #LeanProver #CompSci
Exploring linear Traversable using generics. ~ Sjoerd Visscher. #Haskell #FunctionalProgramming
What OpenAI and GitHub’s “AI pair programmer” means for the software industry. ~ Ben Dickson. #AI #Programming #Copilot
Using AI to Drill Down in Physics. ~ Bennie Mols. #AI
Matemáticas dinámicas: estupendas visualizaciones a partir de código abierto. ~ @Alvy. #Matemáticas #Computación
Dynamic mathematics (Interactive mathematical applets & animations). ~ Juan Carlos Ponce. #Math

09-Jul-21

Formalización del teorema de existencia de modelo en Isabelle/HOL. ~ Sofı́a Santiago Fernández. #TFM #ITP #IsabelleHOL #Lógica #Matemática
Formalized signature extension results for confluence, commutation and unique normal forms. ~ A. Lochmann, F. Mitterwallner, A. Middeldorp. #ITP #IsabelleHOL
Answers to some open questions of Ulrich & Meredith. ~ Matthew Walsh, Branden Fitelson. #ATP #Otter #Logic #Math
SpecCheck: Specification-based testing for Isabelle/ML. ~ Kevin Kappelmann, Lukas Bulwahn. #ITP #IsabelleHOL
Coq meets CλaSH (Proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages). ~ Fritjof Bornebusch. #PhD_Thesis #ITP #Coq
Models for software verification: Proving program correctness. ~ Boro Sitnikovski, Lidija Goracinova-Ilieva, Biljana Stojcevska. #FormalVerification #Coq #Dafny
Using LSTM to predict tactics in Coq. ~ X. Luan, X. Zhang, M. Sun. #ITP #Coq #MachineLearning #NeuralNetwork
A theory of higher-order subtyping with type intervals. ~ Sandro Stucki, Paolo G. Giarrusso. #ITP #Agda
Curry-Howard correspondence: An intuitive language for mathematics. ~ Xiao Tan. #MSc_Thesis #Logic #CompSci
Practical suggestions for mathematical writing. ~ R. Bell, B. Kadets, P. Srinivasan, N. Triantafillou, I. Vogt. #Math

07-Jul-21

Complementing the digital programming tutor Ask-Elle with program synthesis. ~ Gustav Engsmyre, Karl Wikström. #MSc_Thesis #Haskell #FunctionalProgramming

06-Jul-21

Code Lean contenant les preuves d’un cours standard sur les espaces métriques. ~ Frederic Le Roux. #ITP #LeanProver #Math
Function application: Using the dollar sign ($). ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
A brief introduction to Template Haskell. ~ Heitor Toledo Lassarote de Paula. #Haskell #FunctionalProgramming
Will AI rewrite coding? ~ Samuel Greengard. #AI

05-Jul-21

Groups I. Omar Harhara. #ITP #LeanProver #Math
[[https://www.iiia.csic.es/sat2021/program/Slides39.pdf][Chinese remainder encoding for hamiltonian cycles [Slides]]]. ~ Marijn Heule. #ATP #SATSolvers #Math
[[https://www.iiia.csic.es/sat2021/program/Presentation39.mp4][Chinese remainder encoding for hamiltonian cycles [Video]]]. ~ Marijn Heule. #ATP #SATSolvers #Math
[[https://www.iiia.csic.es/sat2021/program/Slides48.pdf ][DiMo: Discrete modelling using propositional logic [Slides]]]. ~ Norbert Hundeshagen, Martin Lange and Georg Siebert. #Logic #Math
[[https://www.iiia.csic.es/sat2021/program/Presentation48.mp4][DiMo: Discrete modelling using propositional logic [Video]]]. ~ Norbert Hundeshagen, Martin Lange and Georg Siebert. #Logic #Math
DiMo: A tool for discrete modelling using propositional logic (version 0.2.2). ~ Martin Lange. #Logic #Math
Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs. ~ Dixit Sabharwal, Jesper G.H. Cockx, Lucas F.B. Escot. #ITP #Agda #Haskell #FunctionalProgramming
Security verification in the context of 5G sensor networks. ~ Piotr Remlein, Urszula Stachowiak. #Haskell #FunctionalProgramming
Deriving a symbolic executor for definitional interpreters suitable for the study of heuristics. ~ Laura-Ana Pîrcalaboiu, Casper Bach Poulsen, Cas van der Rest. #Haskell #FunctionalProgramming
Goodbye C developers: The future of programming with certified program synthesis. ~ Kiran Gopinathan (@Gopiandcoshow). #ITP #Coq
Certifying the synthesis of heap-manipulating programs. ~ Y. Watanabe, K. Gopinathan, George Pîrlea, Nadia Polikarpova, I. Sergey. #ITP #Coq

03-Jul-21

Formalizing higher-order termination in Coq. ~ Deivid Vale, Niels van der Weide.f#page=71 #ITP #Coq
Formalization of a sign determination algorithm in real algebraic geometry. ~ Cyril Cohen. #ITP #Coq #Math
The Cantor-Schröder-Bernstein for homotopy types, or ∞-groupoids, in Agda. ~ Martin Escardo. #ITP #Agda #Logic #Math
The Cantor–Schröder–Bernstein Theorem for ∞-groupoids. ~ Martin Escardo. #Logic #Math
Practical verification of the Haskell ranged-sets library. ~ Ioana Savu, Jesper Cockx, Lucas Escot. #ITP #Agda #Haskell #FunctionalProgramming
Producing a verified implementation of sequences using agda2hs. ~ Shashank Anand, Jesper Cockx, Lucas Escot. #ITP #Agda #Haskell #FunctionalProgramming
Reflective programs in tree calculus. ~ Barry Jay (@Jay59009444). #eBook #ITP #Coq
Proofs in Coq for the book “Reflective programs in tree calculus”. ~ Barry Jay (@Jay59009444). #ITP #Coq
A tutorial implementationof a dependently typed lambda calculus. ~ Andres Löh, Conor McBride, Wouter Swierstra. #ITP #Agda
Formalising contemporary mathematics in simple type theory. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math

02-Jul-21

Isabelle’s metalogic: Formalization and proof checker. ~ Tobias Nipkow, Simon Roßkopf. #ITP #IsabelleHOL
Arming polysemy with Arrows. ~ Robert Peszek. #Haskell #FunctionalProgramming
Functors and monads for people who have read too many “Tutorials”. ~ Jeremy Bowers. #Haskell #FunctionalProgramming

June 2021

30-Jun-21

A Perron–Frobenius theorem for deciding matrix growth. ~ RenéThiemann. #ITP #IsabelleHOL #Math
CoqQFBV: A scalable certified SMT quantifier-free bit-vector solver. ~ Xiaomu Shi et als. #ITP #Coq
On a machine-checked proof for an optimized method to multiply polynomials. ~ S.D. Meshveliani.f#page=88 #ITP #Agda #Math
Augmenting the human mathematician. ~ H.K. Sørensen, M.W. Johansen, R. Hoekzema, H. Breman. #ITP #ATP #Math
Towards finding longer proofs. ~ Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban. #ATP #MachineLearning
Towers of Hanoi from a random start. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming

29-Jun-21

Well-founded recursion. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Math

28-Jun-21

A modular formalisation of finite group theory. ~ Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, LaurentThéry. #ITP #Coq #Math
SAT solver-prover in Lean 4. ~ Siddhartha Gadgil. #ITP #LeanProver #Logic
ProvingGround: Automated Theorem proving by learning. ~ Siddhartha Gadgil. #ITP #LeanProver #MachineLearning
Automating Mathematics? ~ Siddhartha Gadgil.l#/ #Math #ATP #ITP #AI
Euclidean geometry by high-performance solvers? ~ Siddhartha Gadgil, Anand Tadipatri. #Math #ATP #SAT #SMT
A formally verified proof of the central limit theorem. ~ Luke Serafin. #PhD_Thesis #ITP #IsabelleHOL #Math
A formally verified proof of Kruskal’s tree theorem in Lean. ~ Minchao Wu. #ITP #LeanProver #Math

27-Jun-21

Typed programs don’t leak data. ~ Mistral Contrastin. #Haskell #FunctionalProgramming
Historia de desafíos matemáticos. Cómo ganar un millón de dólares. ~ Antonio Pérez (@aperezsanz). #Matemáticas vía @manuel_de_leon

26-Jun-21

La prova del software (in Italian). ~ Riccardo Brasca et als. #ITP #LeanProver #Math
Groundwork for a fallibilist account of Mathematics. ~ Silvia De Toffoli. #Math
Associated types in two different ways. #Haskell #FunctionalProgramming

25-Jun-21

Creación artística y creación matemática. ~ Juan Arias de Reyna. #Matemáticas #ITP #LeanProver
Abstract algebra: Theory and applications. ~ Thomas W. Judson et als. #eBook #Math #Sage
Taller de Sage. ~ Antonio Behn. #Sage #Matemáticas
MiniSail: A kernel language for the ISA specification language SAIL in Isabelle/HOL. ~ Mark Wassell. #ITP #IsabelleHOL
Public announcement logic (in Isabelle/HOL). ~ Asta Halkjær From (@astahfrom). #ITP #IsabelleHOL
Formalized soundness and completeness of epistemic logic. ~ Asta Halkjær From (@astahfrom) et als. #Logic #ITP #IsabelleHOL
Results in modal and dynamic epistemic logic (A formalization in Lean). ~ Paula Neeley. #Logic #ITP #LeanProver
Hito de las demostraciones asistidas por ordenador en Nature. ~ Nerea Diez López. #DAO #LeanProver #Matemáticas
Embedding Youtube videos with org-mode links. ~ Artur Malabarba. #OrgMode #Emacs

24-Jun-21

Verified model checking for conjunctive positive logic. ~ Alex Abuin et als. #ITP #Dafny
CoStar: a verified ALL (*) parser. ~ Sam Lasser et als. #ITP #Coq
Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8. ~ Kyeongmin Cho et als. #ITP #Coq
Las matemáticas que estudian los límites de los ordenadores. ~ Daniel Graça, Ágata A. Timón. #Matemáticas #Computación
A formalization of elementary group theory in the proof assistant Lean. ~ Andrew Zipperer. #ITP #LeanProver #Math
Types versus sets in math and programming languages. ~ Brent Yorgey. #Haskell #FunctionalProgramming
The dawn of formalized mathematics. ~ Andrej Bauer (@andrejbauer). #ITP #Math

23-Jun-21

Van der Waerden’s theorem in Isabelle/HOL. ~ Katharina Kreuzer, Manuel Eberl. #ITP #IsabelleHOL #Math
Deconstructing classes. ~ Nicholas Clarke. #Haskell #FunctionalProgramming

22-Jun-21

A formally verified checker for first-order proofs. ~ Seulkee Baek. #ITP #Agda #Logic
Reaching for the star: Tale of a monad in Coq. ~ Pierre Nigron, Pierre-Évariste Dagand. #ITP #Coq
Mechanising complexity theory: The Cook-Levin theorem in Coq. ~ Lennard Gäher, Fabian Kunze. #ITP #Coq
A mechanized proof of the max-flow min-cut theorem for countable networks. ~ Andreas Lochbihler. #ITP #IsabelleHOL
Formalization of basic combinatorics on words. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
Proof Pearl: Playing with the Tower of Hanoi formally. ~ Laurent Théry. #ITP #Coq
The CakeML project’s quest for ever stronger correctness theorems. ~ Magnus O. Myreen. #ITP #HOL4
A natural formalization of the mutilated checkerboard problem in Naproche. ~ Adrian De Lon, Peter Koepke, Anton Lorenzen. #ITP #Naproche
Verified progress tracking for timely dataflow. ~ M. Brun, S. Decova, A. Lattuada, D. Traytel. #ITP #IsabelleHOL
Ptolemy’s Theorem in Lean. ~ Manuel Candales, Benjamin Davidson. #ITP #LeanProver #Math
Formal software verification measures up. ~ Samuel Greengard. #FormalVerification
Program verification: Vision and reality. ~ Moshe Y. Vardi. #FormalVerification
Consequence relations (An introduction to the Tarski-Lindenbaum method). ~ Alex Citkin, Alexey Muravitsky. #eBook #Logic #Math

21-Jun-21

From proof theory to proof assistants (Challenges of responsible software and AI). ~ Klaus Mainzer. #ITP #Coq #AI
A shorter compiler correctness proof for language IMP. ~ Pasquale Noce. #ITP #IsabelleHOL
Isabelle community conventions. #ITP #IsabelleHOL
FindFacts: Experimental search platform for Isabelle and the AFP./# #ITP #IsabelleHOL
Isabelle quick access links. #ITP #IsabelleHOL
HMock: first rate mocks in Haskell. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming
A new kind of programming: Tactic metaprogramming in Haskell. ~ Sandy Maguire. #Haskell #FunctionalProgramming
Testing smart contracts with QuickCheck. ~ John Hughes. #Haskell #FunctionalProgramming
Lift unliftable (and unlift liftable). ~ Veronika Romashkina (@vrom911). #Haskell #FunctionalProgramming

20-Jun-21

Algebras for weighted search. ~ Donnacha Oisín Kidney, Nicolas Wu. #Haskell #FunctionalProgramming
Competitive programming in Haskell: folding folds. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Molecular dynamic simulations in Haskell. ~ Sascha Bubeck (@SaschaBubeck). #Haskell #FunctionalProgramming

19-Jun-21

Mathematicians welcome computer-assisted proof in ‘grand unification’ theory. ~ Davide Castelvecchi. #ITP #LeanProver #Mat
Formal verification of composable security proofs. ~ Seyed Reza Sefidgar. #PhDThesis #ITP #IsabelleHOL
An alternative axiomatic presentation of Nelson algebras. ~ Juan Manuel Cornejo, Andrés Gallardo, Luiz Monteiro, Ignacio Viglizzo. #ATP #Prover9 #Mace4 #Math

17-Jun-21

La gran familia de los números. ~ Raúl Ibáñez. #Matemáticas
Computer says ‘I don’t know’ (The case for Honest AI). ~ Peter Flach. #AI via @hakankj

15-Jun-21

Finite abstract algebra in Haskell. ~ Ben Selfridge. #Haskell #FunctionalProgramming #Math
Undecidability and incompleteness of second-order logic. ~ Mark Koch. #ITP #Cog #Logic #Math
Integration verification across software and hardware for a simple embedded system. ~ A. Erbsen, S. Gruetter, J. Choi, C. Wood, A. Chlipala. #ITP #Coq
Don’t mind the formalization gap: The design and usage of Hs-to-Coq. ~ Antal Spector-Zabusky. #PhD_Thesis #ITP #Coq #Haskell #FunctionalProgramming

14-Jun-21

Hybrid systems verification with Isabelle/HOL: Simpler syntax, better models, faster proofs. ~ Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth. #ITP #IsabelleHOL

13-Jun-21

Median heaps in Haskell. ~ Micah Cantor. #Haskell #FunctionalProgramming
Theorem proving and Artificial Intelligence (A brief introduction). ~ Josef Urban. #ATP #ITP #AI #MachineLearning
Towards a human-like reasoning system. ~ Mateja Jamnik. #ATP #AI
Mathematical reasoning in humans. ~ Jay McClelland. #AI #Math
From Hammer to Scalpel: Progress in Automated Theorem Proving. ~ Markus Rabe. #ATP #AI
Training a first-order theorem prover from synthetic data. ~ Vlad Firoiu et als. #ATP #AI #MachineLearning
Training a first-order theorem prover from synthetic data. ~ Vlad Firoiu et als. #ATP #AI #MachineLearning
Proof artifact co-training for theorem proving with language models. ~ Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu. #ITP #LeanProver #MachineLearning
Neural theorem proving in Lean using proof artifact co-training and language models. ~ Jesse Michael Han. #ITP #LeanProver #MachineLearning
Video series “Haskell by Example”. ~ Michael Oswald. #Haskell #FunctionalProgramming

12-Jun-21

Formalisation du théorème de décomposition de Hahn avec le démonstrateur interactif Isabelle. ~ Marie Cousin. #ITP #IsabelleHOL #Math
Synthetic completeness for a terminating Seligman-Style tableau system. ~ Asta Halkjær From. #ITP #IsabelleHOL #Logic #Math
Teaching computers about numbers. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Towards a verified compiler from Cogent to LLVM. ~ Harrison Jay Scott. #BsC_Thesis #ITP #Coq
Birkhoff’s completeness theorem for multi-sorted algebras formalized in Agda. ~ Andreas Abel. #ITP #Agda #Math
Global optimisation with constructive reals. ~ Dan R. Ghica, odd Waugh Ambridge. #ITP #Agda #Math
Haskell and the elegant attack. ~ Tony Day (@tonyday567). #Haskell #FunctionalProgramming
Demostración del teorema de Cantor-Schröder-Bernstein. ~ Urtzi Buijs (@archimedestub). #Matemáticas
The fixed point. ~ Rebecca Skinner. #Haskell #FunctionalProgramming

11-Jun-21

What the rec? Types dependent on terms, Lean eliminators, and threshold concepts. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver
Practical Haskell use cases. #Haskell #FunctionalProgramming
Introducing Haskell in Soisy. ~ Marco Perone. #Haskell #FunctionalProgramming
Programming puzzles. ~ Tal Schuster, Ashwin Kalyan, Oleksandr Polozov, Adam Tauman Kalai. #Programming #Python
Python Programming Puzzles (P3). #Programming #Python
Des bibliothèques aux logiciels: une histoire d’amour! ~ Sabrina Granger. #Programming
Jornada sobre Inteligencia Artificial de los Institutos de Investigación de la Universidad de Zaragoza. #IA

10-Jun-21

Certified quantum computation in Isabelle/HOL. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL
Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. ~ Julien Narboux, Viviane Durand-Guerrier. #ITP #Coq #Math
A framework for certified program synthesis. ~ Yasunari Watanabe. #PhDThesis #ITP #Coq

09-Jun-21

Learning to guide a saturation-based theorem prover. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning
Learning set theory through Coq (part 1). ~ Kyle Stemen. #ITP #Coq #Math
Learning set theory through Coq (part 2). ~ Kyle Stemen. #ITP #Coq #Math
Learning set theory through Coq (part 3). ~ Kyle Stemen. #ITP #Coq #Math

08-Jun-21

Formally verified convergence of policy-rich DBF routing protocols. ~ Matthew L. Daggitt, Timothy G. Griffin. #ITP #Agda
Teaching a HOL course: experience report. ~ Konrad Slind et als. #ITP #HOL4
Why A.I. Moonshots Miss (Ambitious predictions about the future powers of computers keep turning out to be wrong). ~ Jeffrey Funk, Gary Smith. #AI
Online machine learning techniques for Coq: a comparison. ~ #ITP #Coq #MachineLearning
Learning proofs for the classification of nilpotent semigroups. ~ Carlos Simpson. #ATP #MachineLearning #Math
Re-inventing the Monad wheel. ~ Boro Sitnikovski (@BSitnikovski). #Haskell #FunctionalProgramming

07-Jun-21

Why Kleisli arrows matter. ~ Douglas M. Auclair (geophf). #Haskell #FunctionalProgramming
TypeFunc: This repository collects some links and resources for learning about type theory, functional programming, and related subjects. ~ Avatar William DeMeo. #ITP #FunctionalProgramming #Agda #Coq #Haskell #Idris #LeanProver #Scala

06-Jun-21

Roger Penrose explains Godel’s incompleteness theorem in 3 minutes. #Logic #Math
Half a year of the Liquid Tensor Experiment: Amazing developments. ~ Peter Scholze. #ITP #LeanProver #Math

05-Jun-21

A formalization of dynamic epistemic logic. ~ Paula Neeley. #ITP #LeanProver #Logic
Verified quadratic virtual substitution for real arithmetic. ~ Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer. #ITP #IsabelleHOL #Logic #Math
Verifying value iteration and policy iteration in Coq. ~ David M. Masters. #MSc_Thesis #ITP #Coq #MachineLearning
A toolbox for mechanised first-order logic. ~ Johannes Hostert, Mark Koch, Dominik Kirst. #ITP #Coq #Logic #Math
The role of entropy in guiding a connection prover. ~ Zsolt Zombori, Josef Urban, Miroslav Olšák. #ATP #MachineLearning
Declaration groups: where order of declarations suddenly matters in Haskell. ~ Artyom Kazak. #Haskell #FunctionalProgramming
Final tagless encodings have little to do with typeclasses. ~ Ben Levy. #Haskell #FunctionalProgramming
Getting started with Haskell projects using Scotty. ~ Juan Pedro Villa Isaza. #Haskell #FunctionalProgramming
Phantom types and globbing bugs. ~ Patrick Brisbin. #Haskell #FunctionalProgramming
Probability for Slay the Spire fanatics. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming #Math
Bach as mathematician. ~ David H Bailey. #Math #Music #Bach

04-Jun-21

El Teorema de Cantor-Schröder-Bernstein. ~ Urtzi Buijs @archimedestub. #Lógica #Matemática
Mathematicians identify threshold at which shapes give way. ~ Mordechai Rorvig. #Math

03-Jun-21

Using dependent types to write proofs in Haskell. ~ Jan Mas Rovira. #Haskell #FunctionalProgramming #Logic

02-Jun-21

Functional Programming - the True Silver Bullet. ~ Ilya Suzdalnitski. #FunctionalProgramming

01-Jun-21

How a simple arithmetic puzzle can guide discovery. ~ Pradeep Mutalik. #Math
Relations in Lean. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Math
Decidable propositions I. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Math
Decidable propositions II. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Math
Decidable propositions III. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Math
Vectors and dependent function types. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Math
The limits of computation. ~ A. Powell. #CompSci #LambdaCalculus #TypeTheory
Practical normalization by evaluation for EDSLs. ~ N. Valliappan, A. Russo, S. Lindley. #Haskell #FunctionalProgramming
Hook: An embedded domain-specific language for fusing implicit interactions to explicit event handlers. ~ Tomoki Shibata, Usamatthew Ahrens, Usarobert J.K. Jacob. #Haskell #FunctionalProgramming
Some axioms for mathematics. ~ Frédéric Blanqui et als. #Logic #Math
Set of support, demodulation, paramodulation: a historical Perspective. ~ Maria Paola Bonacina. #ATP #Logic #Math
Lifting the exponent. ~ Jakub Kądziołka. #ITP #IsabelleHOL #Math

May 2021

31-May-21

¿Pueden las máquinas ser creativas? ~ Ramón López de Mántaras. #IA

30-May-21

Fun with category theory and dynamical systems. ~ Chris Smith (@cdsmithus). #CategoryTheory
Representable functors: Practical examples. ~ Siddharth Bhat. #Haskell #FunctionalProgramming

29-May-21

Quantum and classical registers. ~ Dominique Unruh. #ITP #IsabelleHOL
Proof repair. ~ Talia Ringer. #PhD_Thesis #ITP #Coq
CoCEC: An automatic combinational circuit equivalence checker based on the interactive theorem prover. ~ Wilayat Khan, Farrukh Aslam Khan, Abdelouahid Derhab, Adi Alhudhaif. #ITP #Coq
Some formal tools for computer arithmetic: Flocq and Gappa. ~ S. Boldo, G. Melquiond. #ITP #Coq
A beginner guide to Iris, Coq and separation logic. ~ Elizabeth Dietrich. #ITP #Coq
Mechanized type safety for gradual information flow. ~ Tianyu Chen, Jeremy G. Siek. #ITP #Agda
Actions you can handle: Dependent types for AI plans. ~ Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, Ronald P. A. Petrick. #ITP #Agda #AI
Formal synthesis of filter components for use in security-enhancing architectural transformations. ~ David S. Hardin, Konrand L. Slind. #ITP #ACL2

28-May-21

A combinator library for taxes. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming
Haskell: Applicative. ~ Vlad P. Luchian (@Cstml1). #Haskell #FunctionalProgramming
Testing smart contracts with QuickCheck. ~ John Hughes. #Haskell #FunctionalProgramming #QuickCheck
Proof-oriented programming in F*. #ITP #FunctionalProgramming

26-May-21

Separation logic foundations (Software Foundations, Volume 6). ~ Arthur Charguéraud. #ITP #Coq
The Natural Number Game. ~ Brent Yorgey. #ITP #LeanProver #Math
Combinatorics on words basics. ~ Štěpán Holub, Martin Raška, Štěpán Starosta. #ITP #IsabelleHOL
Graph lemma. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
Lyndon words. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
Functors and monads for people who have read too many “tutorials”. ~ Jeremy Bowers. #Haskell #FunctionalProgramming
Tying the Knot in Haskell. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming

25-May-21

Verifying time complexity of binary search using Dafny. ~ Shiri Morshtein et als. #Dafny #Algorithms
Two new ways to formally prove Dandelin-Gallucci’s theorem. ~ D. Braun, N. Magaud, P. Schreck. #ITP #Coq #Math
A logic theory pattern for linearized control systems. ~ A. Domenici, C. Bernardeschi. #ITP #PVS

24-May-21

Fix(ity) me. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming

23-May-21

Translating LaTeX to Coq: A recurrent neural network approach to formalizing natural language proofs. ~ Benjamin A. Carman. #PhD_Thesis #ITP #Coq #NeuralNetwork
A novel proof of shuffle: Exponentially secure cut-and-choose. ~ Thomas Haines, Johannes Müller. #ITP #Coq
Verbatim: A verified lexer generator. ~ D. Egolf, S. Lasser, K. Fisher. #ITP #Coq
miniF2F: Formal to Formal Mathematics Benchmark consisting of exercise statements from olympiads (AMC, AIME, IMO). #ITP #LeanProver #Math
A complete bibliography of publications in the Journal of Functional Programming. ~ Nelson H.F. Beebe. #FunctionalProgramming

21-May-21

Annotations in GHC. ~ Shayne Fletcher. #Haskell #FunctionalProgramming
Mathematicians answer old question about odd graphs. ~ Kevin Hartnett (@KSHartnett). #Maths
Silver Oak: Formal specification and verification of hardware, especially for security and privacy. #ITP #Coq
An AI has disproved five mathematical conjectures with no human help. #AI #Math
Constructions in combinatorics via neural networks. ~ Adam Zsolt Wagner. #AI #Math #MachineLearning #NeuralNetwork

20-May-21

Module organization guidelines for Haskell projects. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
A collection of OEIS sequences in Haskell. ~ Debdut Karmakar (@KarmakarDebdut). #Haskell #FunctionalProgramming #Math

18-May-21

Formally verified simulations of state-rich processes using interaction trees in Isabelle/HOL. ~ Simon Foster, Chung-Kil Hur, Jim Woodcock. #ITP #IsabelleHOL
Formalization of ring theory in PVS (Isomorphism theorems, principal, prime and maximal ideals, chinese remainder theorem). ~ Thaynara Arielly de Lima et als. #ITP #PVS #Math
Computable analysis and notions of continuity in Coq. ~ H. Thies, L. Thery, F. Steinberg. #ITP #Coq #Math

17-May-21

Fixed point construction on complete lattices. ~ Johannes Hölzl et als. #ITP #LeanProver #Math

16-May-21

Constructions in combinatorics via neural networks. ~ Adam Zsolt Wagner. #MachineLearning #Math

15-May-21

On preserving the computational content of mathematical proofs: toy examples for a formalising strategy. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
Hensel’s Lemma for the p-adic integers (in Isabelle/HOL). ~ Aaron Crighton. #ITP #IsabelleHOL #Math
The Haskell Phrasebook. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
Haskell MOOC University of Helsinki. ~ Joel Kaasinen, John Lång. #Haskell #FunctionalProgramming
Counterexamples in type systems. ~ Stephen Dolan. #TypeTheory
Qué son los algoritmos y cómo aprenden de nosotros. | BBC Mundo. #Algoritmos

14-May-21

Enigma GPT-2: ¿Puedes distinguir un artículo real de otro falso generado mediante inteligencia artificial simplemente leyendo el resumen?. ~ @Alvy. #IA
Regreso al futuro de las matemáticas: Si Hipatia levantara la cabeza. ~ Patricia Contreras Tejada (@_PatriciaCT). #Matemáticas

12-May-21

The Genuine Sieve of Eratosthenes. ~ Jeremy Gibbons (@jer_gib). #Haskell #FunctionalProgramming
Type-guided development and garden paths. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming
Why you should learn functional programming: Type classes vs. interfaces. ~ @forketyfork #Java #Haskell #FunctionalProgramming
How mathematicians use homology to make sense of topology. ~ Kelsey Houston-Edwards. #Math

11-May-21

Automated conjecturing in QuickSpec. ~ Moa Johansson, Nicholas Smallbone. #Haskell #FuncionalProgramming

10-May-21

Functional algorithms, verified! ~ Tobias Nipkow et als. #eBook #ITP #IsabelleHOL #Algorithms
Construction of an algebraic number that is not solvable by radicals. ~ Thomas Browning. #ITP #LeanProver #Math

09-May-21

Slides and exercises of the Lean 4 course “Theorem prover lab: applications in programming languages”. ~ Jakob von Raumer, Sebastian Ullrich (@derKha). #ITP #Lean4
Lean 4 Metamath verifier. ~ Mario Carneiro. #ITP #Lean4 #Metamath
The type theory of Lean. ~ Mario Carneiro. #ITP #LeanProver #TypeTheory

06-May-21

Books: Inquiry-Based Learning Guides. #eBooks #Math

05-May-21

The beauty of functional languages in Deep Learning — Clojure and Haskell. ~ Jun Wu. #Clojure #Haskell #FunctionalProgramming #DeepLearning
The IMO Grand Challenge. ~ Daniel Selsam. #ITP #LeanProver
The trick to avoid deeply-nested error-handling code. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming

04-May-21

Regression test selection. ~ Susannah Mansky. #ITP #IsabelleHOL #Math
Itauto: an extensible intuitionistic SAT solver. ~ Frédéric Besson. #ITP #Coq #Logic #SAT_Solver
Programming in Z3 by learning to think like a compiler. ~ Marianne Bellotti. #SMT #Z3

03-May-21

Formalizing the face lattice of polyhedra. ~ Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. #ITP #Coq #Math
Lean Together 2021: Panel on teaching with proof assistants. #ITP #LeanProver
Quick and dirty backpropagation in Haskell. ~ Francesco Mazzoli (@trascendentale). #Haskell #FunctionalProgramming #NeuralNetwork

02-May-21

Feferman’s virtual book: Logic, Mathematics, and Conceptual Structuralism. ~ Peter Smith (@PeterSmith). #Logic #Math

01-May-21

A formalised theorem in the partition calculus. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL. ~ Martin Raška, Štěpán Starosta. #ITP #IsabelleHOL
Reliable reconstruction of fine-grained proofs in a proof assistant. ~ HJ Schurr, M Fleury, M Desharnais. #ITP #IsabelleHOL
LEO: A programming language for formally verified, zero-knowledge applications. ~ C. Chin et als. #ITP #ACL2
Formal verification of termination criteria for first-order recursive functions. ~ C.A. Muñoz et als. #ITP #PVS
Verifying the semantics of disambiguation rules (Using parse tree repairing for showing safety and completeness of associativity and priority rules). ~ L. Miljak. #ITP #Coq

April 2021

30-Apr-21

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

29-Apr-21

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

28-Apr-21

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

27-Apr-21

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

26-Apr-21

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

25-Apr-21

Grandes ideas de la Filosofía: Lógica. #Lógica
Formalization in Lean of IMO 2001 Q2. ~ Tian Chen. #ITP #LeanProver #Math #IMO

24-Apr-21

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

23-Apr-21

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 (@epoberezkin). #Haskell #FunctionalProgramming
15 graphs you need to see to understand AI in 2021. ~ Eliza Strickland. #AI

22-Apr-21

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 (@GabrielG439). #Programming

20-Apr-21

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 (@cdsmithus). #Haskell #FunctionalProgramming
A random tour of typeclass in Haskell. ~ Ong Yi Ren. #Haskell #FunctionalProgramming
Writing technical documentation with Emacs. #Emacs #OrgMode

18-Apr-21

Induction on equality. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math

17-Apr-21

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

16-Apr-21

Type theory. ~ Thierry Coquand. #TypeTheory
More on types, typeclasses and the foldable typeclass. ~ Marty Stumpf. #Haskell #FunctionalProgramming
The movement principle. ~ Chris Done (@christopherdone). #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 (@EricaKlarreich). #Math

15-Apr-21

Formalization in Lean of IMO 1977 Q6. ~ Tian Chen. #ITP #LeanProver #Math
Heron’s Formula (in Lean). ~ Matt Kempster. #ITP #LeanProver #Math

14-Apr-21

¿Para qué sirven las matemáticas? ~ Marta Macho Stadler (@MartaMachoS). #Matemáticas

13-Apr-21

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 (@jonascarpay). #Haskell #FunctionalProgramming
Things I wish someone had explained about functional programming (Part 1: Faulty assumptions). ~ James Sinclair (@jrsinclair). #FunctionalProgramming
Things I wish someone had explained about functional programming (Part 2: Algebraic structures). ~ James Sinclair (@jrsinclair). #FunctionalProgramming
Things I wish someone had explained about functional programming (Part 3: Type classes). ~ James Sinclair (@jrsinclair). #FunctionalProgramming
Things I wish someone had explained about functional programming (Part 4: Algebraic data types). ~ James Sinclair (@jrsinclair). #FunctionalProgramming
Generative art using Haskell. ~ David Luposchainsky (@quch3n). #Haskell #FunctionalProgramming
Programar es de pobres: por qué el mundo del ‘software’ está roto en España. ~ Eduardo Manchón (@eduardomanchon). #Programación #Informática

12-Apr-21

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 (@BartoszMilewski). #Haskell #FunctionalProgramming #CategoryTheory
The beauty of programming. ~ Linus Torvalds. #Programming
Gnus Emacs as email client in IMAP with ProtonMail. ~ Joseph Vidal-Rosset. #Emacs #ProtonMail

11-Apr-21

Products and sums, named and anonymous. ~ Ömer Sinan Ağacan. #Haskell #FunctionalProgramming

10-Apr-21

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 (@MarkusTriska). #Prolog #LogicProgramming

09-Apr-21

Grothendieck’s Schemes in Algebraic Geometry. ~ Anthony Bordg, Lawrence Paulson, Wenda Li. #ITP #IsabelleHOL #Math
Continued fractions in Haskell. ~ Chris Smith (@cdsmithus).l#P7oZc6pbWBK6wRaBBMm0goA #Haskell #FunctionalProgramming #Math
Algorithmic puzzle: Continuous increasing subsequences. ~ Boro Sitnikovski (@BSitnikovski). #Haskell #FunctionalProgramming
How to replace Proxy with AllowAmbiguousTypes. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming

08-Apr-21

Formalization in Lean of IMO 2008 Q4. ~ Manuel Candales. #ITP #LeanProver #Math
Giml’s type inference engine. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming
Scrabbλe: A one- or two-player implementation of Scrabble for teaching functional programming. ~ Jim Burton. #eBook #Haskell #FunctionalProgramming

06-Apr-21

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 (@BSitnikovski). #Haskell #FunctionalProgramming #Math
Auto build and publish emacs org configuration as a website. ~ Erick Navarro (@erickgnavar). #Emacs
Division by zero in Logic and Computing. ~ Jan Bergstra. #Logic #Math #CompSci

05-Apr-21

Induction, and inductive types. ~ Kevin Buzzard (@XenaProject). #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

04-Apr-21

ProverX: Rewriting and extending Prover9. ~ Ivo Robert. #PhDThesis #ATP #Prover9

03-Apr-21

SSProve: A foundational framework for modular cryptographic proofs in Coq. ~ Carmine Abate et als. #ITP #Coq

02-Apr-21

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 (@stschiff). #Haskell #FunctionalProgramming
Category theory illustrated. ~ Boris Marinov (@AlexanderKatt). #CategoryTheory
#SEP: Category theory. ~ Jean-Pierre Marquis. #CategoryTheory #Logic #Math

March 2021

31-Mar-21

Abstract modeling of systems communication in constructive cryptography using CryptHOL. ~ D. Basin, A. Lochbihler, U. Maurer, S.R. Sefidgar. #ITP #IsabelleHOL
Verified software units. ~ Lennart Beringer. #ITP #Coq
linear-logic: a version of intuitionistic linear logic on top of linear Haskell. ~ Edward Kmett (@kmett). #Haskell #FunctionalProgramming #Logic
Do judge a test by its cover: Combining combinatorial and property-based testing. ~ Harrison Goldstein, John Hughes, Leonidas Lampropoulos, Benjamin C. Pierce. #Haskell #FunctionalProgramming

30-Mar-21

Varieties of mathematical understanding. ~ Jeremy Avigad. #ITP #Math
A formal proof of the Lax equivalence theorem for finite difference schemes. ~ Mohit Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin. #ITP #Coq #Math
Verifying min-plus Computations with Coq (extended version with appendix). ~ Lucien Rakotomalala, Pierre Roux, Marc Boyer. #ITP #Coq
For a few dollars more: Verified fine-grained algorithm analysis down to LLVM. ~ Maximilian P.L. Haslbeck, Peter Lammich. #ITP #IsabelleHOL
Certifying proofs in the first-order theory of rewriting. ~ Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer. #ITP #IsabelleHOL
Limits of real numbers in the binary signed digit representation. ~ Franziskus Wiesnet, Nils Köpp. #Haskell #FunctionalProgramming #Math
El Análisis complejo y una exploración de los conjuntos de Mandelbrot y Julia con código abierto. ~ @Alvy. #Matemáticas #Programación
Análisis complejo (Una introducción visual e interactiva). ~ Juan Carlos Ponce Campuzano. #eBook #Matemáticas
Lógica de programação funcional: Pense em Hope (Exercícios de programação funcional com Hope). ~ José Augusto N. G. Manzano, José A. Alonso Jiménez, María J. Hidalgo Doblado. #eBook #Hope #FunctionalProgramming

29-Mar-21

Strong typing. ~ M-J. Dominus (1999). #Programming
Why functional programming matters. ~ John Hughes. #FunctionalProgramming
The dawning of a new era in applied mathematics. ~ Weinan E. #Math via @emulenews
La inteligencia artificial nunca será como la humana. ~ Ramón López de Mántaras. #IA
EmacsTutorial01: Semantic keybindings to memorize hundreds of keys instantly. #Emacs

27-Mar-21

SSProve: A foundational framework for modular cryptographic proofs in Coq. ~ C. Abate, P.G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Hritcu, K. Maillard, B. Spitters. #ITP #Coq
A well-known representation of monoids and its application to the function “vector reverse”. ~ Wouter Swierstra. #Agda #FunctionalProgramming
Functional Pearl: Witness me - Constructive arguments must be guided with concrete witness. ~ Hiromi Ishii. #Haskell #FunctionalProgramming
Combining folds using semigroups. ~ Luc Tielen (@luctielen). #Haskell #FunctionalProgramming
Many faces of internal functions. ~ Veronika Romashkina (@vrom911). #Haskell #FunctionalProgramming

26-Mar-21

Alectryon: a collection of tools for writing technical documents that mix Coq code and prose. ~ Clément Pit-Claudel. #ITP #Coq via @jjcarett2
Building a personal website with org-mode. ~ Rafael Fernández (@ereslibre). #Emacs #OrgMode
Weblorg: A static HTML generator for Emacs and Org-Mode. #Emacs #OrgMode

25-Mar-21

An introduction to typeclass metaprogramming. ~ Alexis King (@lexi_lambda). #Haskell #FunctionalProgramming
How to build hybrid Haskell and Java programs. ~ Facundo Domínguez, Andreas Hermann. #Haskell #Java

24-Mar-21

Course: Programming languages. ~ Zach Tatlock, Leonardo De Moura. #CompSci #ITP #LeanProver
Coq fundamentals. ~ Zach Tatlock. #ITP #Coq
Leaning into Spivak’s calculus. ~ Tom Houle (@_tomhoule). #ITP #LeanProver #Math

23-Mar-21

IsarStep: A benchmark for high-level mathematical reasoning. ~ W. Li, L. Yu, Y. Wu, L.C. Paulson. #ITP #IsabelleHOL #Math #MachineLearning
Formal verification of Zagier’s one-sentence proof. ~ Guillaume Dubach, Fabian Muehlboeck. #ITP #Coq #Math
Programmer learning list. ~ Michael Snoyman (@snoyberg). #Programming
Install GHC, Cabal and Haskell Language Server IDE on Windows 10. ~ Will Gould. #Haskell #FunctionalProgramming

21-Mar-21

Diagrams for Penrose tiles. ~ Chris Reade. #Haskell #FunctionalProgramming #Math

20-Mar-21

Quantum projective measurements and the CHSH inequality in Isabelle/HOL. ~ Mnacho Echenim, Mehdi Mhalla. #ITP #IsabelleHOL
Reasoning about the garden of forking paths. ~ Yao Li, Li-yao Xia, Stephanie Weirich. #ITP #Coq
Plotting in a formally verified way. ~ Guillaume Melquiond. #ITP #Coq
Classical (co)recursion: Programming. ~ Paul Downen, Zena M. Ariola. #Agda #Scheme #Python #Java
Partial evaluation of logic programs in vector spaces. ~ Chiaki Sakama, Hien D. Nguyen, Taisuke Sato, Katsumi Inoue. #LogicProgramming #Math

18-Mar-21

Verified quantitative analysis of imperative algorithms. ~ Maximilian P.L. Haslbeck. #PhDThesis #ITP #IsabelleHOL
Constructive cryptography in HOL: the communication modeling aspect. ~ Andreas Lochbihler, S. Reza Sefidgar. #ITP #IsabelleHOL
Introduction to lambda calculus. ~ John Lång. #LambdaCalculus #FunctionalProgramming
Pioneers linking Math and Computer Science win the Abel Prize. ~ Kevin Hartnett (@KSHartnett). #Math #CompSci
László Lovász: Working mathematical miracles. ~ Marianne Freiberger. #Math #CompSci
Avi Wigderson: “It’s good to have hard problems”. ~ Rachel Thomas. #Math #CompSci
Cryptography and pseudorandomness. ~ Avi Wigderson. #Math #CompSci
Mathematics and computation (A theory revolutionizing technology and science). ~ Avi Wigderson. #eBook #Math #CompSci via @mbelcrypt_vasco

17-Mar-21

The Agda universal algebra library, Part 2: Structure. ~ William DeMeo. #ITP #Agda #Math
Formal methods for the informal engineer (Tutorial 2: The Coq theorem prover). ~ Cody Roux. #ITP #Coq
The bottom of the Haskell Pyramid. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming
The history and concept of mathematical proof. ~ Steven G. Krantz. #Logic #Math via @mathematicsprof
Historia visual de los lenguajes de programación. ~ Jordi Cabot (@ingdesoftware). #Programación vía @fernand0

16-Mar-21

Synthetic undecidability and incompleteness of first-order axiom systems in Coq. ~ Dominik Kirst, Marc Hermes. #ITP #Coq #Logic #Math
Functional Pearls: Heterogeneous binary random-access lists. ~ Wouter Swierstra. #Agda #FunctionalProgramming
Haskell knowledge map. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
Evaluación perezosa en Python. Parte 5: Formalización de la secuencia perezosa. ~ Chema Cortés (@chemacortes). #Python #Programación

15-Mar-21

Formalising mathematics: workshop 8 (group cohomology). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation (in Isabelle/HOL). ~ Ralph Bottesch, Jose Divason, Rene Thiemann. #ITP #IsabelleHOL #Math
Hyperfunctions. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
List of formulae involving π. #Math via @mathematicsprof

14-Mar-21

(((Wait a moment .) .) .) - Composing functions with multiple arguments. ~ Philip K. Dick. #Haskell #FunctionalProgramming

13-Mar-21

Flycheck and HLS. ~ Magnus Therning. #Emacs #LSPmode #Haskell #HLS via @jneira

12-Mar-21

The Hermite–Lindemann–Weierstraß transcendence theorem (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
Order theory for computer scientists. ~ Matt Might (@mattmight). #Math #CompSci #Haskell #FunctionalProgramming via @CompSciFact
What is mathematics? ~ Alec Wilkinson. #Math
An infinite descent into pure mathematics. ~ Clive Newstead. #eBook #Math
How to write proofs: a quick guide. ~ Eugenia Cheng (@DrEugeniaCheng). #Logic #Math

11-Mar-21

Emacs y lsp-mode. #Emacs #LSPmode

10-Mar-21

The Agda universal algebra library - Part 1: Foundation (Equality, extensionality, truncation, and dependent types for relations and algebras). ~ William DeMeo. #ITP #Agda #Math
A replication crisis in mathematics? ~ Anthony Bordg. #Math #ITP
Contrastando dos códices matemáticos iluminados. ~ Ángel Requena Fraile. #Matemáticas

09-Mar-21

Programming and proving in Agda. ~ Jesper Cockx (@dregntael). #ITP #Agda #FunctionalProgramming #Haskell
Formal verification of authenticated, append-only skip lists in Agda: Extended version. ~ Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. #ITP #Agda
Symbolic and automatic differentiation of languages. ~ Conal Elliott. #ITP #Agda
Quantum projective measurements and the CHSH inequality (in Isabelle/HOL). ~ Mnacho Echenim. #ITP #IsabelleHOL
Bernoulli polynomials (in Lean prover). ~ Ashvni Narayanan. #ITP #LeanProver #Math
Pruning unused Haskell dependencies. ~ Dan Fithian. #Haskell #FunctionalProgramming
Logical foundations: Personal perspective. ~ Yuri Gurevich. #Logic #Math #CompSci
Recreational Mathematics. ~ Paul Yiu. #eBook #Math
Five principles for programming languages for learners. ~ Mark Guzdial (@guzdial). #CompSci #Teaching #Programming
Fifteen awesome cross-platform math apps. ~ Jason Polak. #Math #CompSci #Programming

08-Mar-21

Formalizing graph trail properties in Isabelle/HOL. ~ Laura Kovacs, Hanna Lachnitt, Stefan Szeider. #ITP #IsabelleHOL #Math
Training a first-order theorem prover from synthetic data. ~ Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, Shibl Mourad. #ATP #MachineLearning
Measuring mathematical problem solving with the MATH dataset. ~ Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, Jacob Steinhardt. #MachineLearning #ITP #Math

07-Mar-21

Theorems for free from separation logic specifications. ~ Lars Birkedal et als. #ITP #Coq
Mereology (in Isabelle/HOL). ~ Ben Blumson. #ITP #IsabelleHOL #Logic

06-Mar-21

Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOL. ~ Asta Halkjær From, Jørgen Villadsen. #Logic #FunctionalProgramming #ITP #Agda #IsabelleHOL
Formalization and verification of reconfigurable discrete-event system using model driven engineering and Isabelle/HOL. ~ S. Soualah, Y. Hafidi, M. Khalgui, A. Chaoui, L. Kahloul. #ITP #IsabelleHOL
Generalized universe hierarchies and first-class universe levels. ~ András Kovács. #ITP #Agda
Roosterize: Suggesting lemma names for Coq verification projects using deep learning. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq #DeepLearning
Neural theorem proving in Lean using Proof Artifact Co-training and language models. ~ Jason Rute. #ITP #LeanProver #MachineLearning
Neural theorem proving in Lean using Proof Artifact Co-training and language models. [Slides] ~ Jason Rute. #ITP #LeanProver #MachineLearning
Proving theorems about regular languages and DFAs in Lean. ~ Noam Atar. #ITP #LeanProver
Boolean rings (in Lean prover). ~ Bryan Gin-ge Chen. #ITP #LeanProver #Math
HGeometry: Computational Geometry in Haskell. #Haskell #FunctionalProgramming #Math

05-Mar-21

Formalising mathematics: workshop 7 (quotients). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Tutorial: Cellular automata and comonads. ~ Siddharth Bhat. #Haskell #FunctionalProgramming
These are the 10 toughest math problems ever solved. ~ Dave Linkletter. #Math
L’informatique, quelques questions pour se fâcher entre amis. ~ Serge Abiteboul, Inria Paris, Gilles Dowek. #CompSci

04-Mar-21

A brief history of Logic. ~ Moshe Y. Vardi (2003). #Logic #Math #CompSci via @prathyvsh
Experimental mathematics approach to Gauss diagrams realizability. ~ A. Khan, A. Lisitsa, A. Vernitski. #Prolog #LogicProgramming #Math

03-Mar-21

Short introduction to Topology (for Computer Science grad students). ~ Mark Jason Dominus (2010). #Math via @CompSciFact
Using Nix for Haskell development in Emacs with LSP. ~ Jonas Collberg. #Haskell #Emacs
Towards a notion of basis for knowledge-based systems - Applications. ~ Gonzalo A. Aranda, Joaquín Borrego, Juan Galán, Daniel Rodríguez. #Math #CompSci

02-Mar-21

[[https://youtu.be/UnYrWuOzOlc][AI and Theorem Proving [Video]]]. ~ Josef Urban. #ATP #ITP #MachineLearning #AI
[[https://cmsa.fas.harvard.edu/wp-content/uploads/2021/01/Urbanslides.pdf][AI and Theorem Proving [Slides]]]. ~ Josef Urban. #ATP #ITP #MachineLearning #AI
[[https://youtu.be/Y0hpHm74FYs][Language modeling for mathematical reasoning [Video]]]. ~ Christian Szegedy. #Logic #Math #AI
[[https://cmsa.fas.harvard.edu/wp-content/uploads/2021/01/Language-modeling-for-Mathematical-Reasoning-.pdf ][Language modeling for mathematical reasoning [Slides]]]. ~ Christian Szegedy. #Logic #Math #AI
Arrows Zoo. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
Introducing my fall 1987 course on Mathematical Methodology. ~ Edsger W.Dijkstra. #Math

01-Mar-21

The sunflower lemma of Erdős and Rado (in Isabelle/HOL). ~ René Thiemann. #ITP #IsabelleHOL #Math
12² beautiful mathematical theorems with short proofs. ~ Jörg Neunhäuserer. #Math via @@lizardbill
Proofs in Mathematics. ~ Alexander Bogomolny. #Math

February 2021

28-Feb-21

Proof verification technology and elementary physics. ~ Ernest Davis. #FormalVerification #Physics
How I use Dante. #Haskell #FunctionalProgramming #Emacs

27-Feb-21

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

26-Feb-21

Formalising mathematics: workshop 6 (limits). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
A verified imperative implementation of B-trees (in Isabelle/HOL). ~ Niels Mündle. #ITP #IsabelleHOL
Totality. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
Evaluación perezosa en Python. Parte 4: Evaluación perezosa avanzada. ~ Chema Cortés (@chemacortes). #Python #Programación

25-Feb-21

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

24-Feb-21

Rerecorded introduction to the Algebra of Programming research group. ~ Jeremy Gibbons (@jer_gib). #CompSci #Haskell #FunctionalProgramming

23-Feb-21

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

21-Feb-21

A formal proof of safegcd bounds. ~ Russell O’Connor, Andrew Poelstra. #ITP #Coq

20-Feb-21

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 (@manu_msr). #Haskell #FunctionalProgramming
Type classes: de aprendiz a maestro. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming

19-Feb-21

Formalizing groups in type theory. ~ Farida Kachapova. #Logic #Math #ITP
Formalising mathematics: workshop 5 (filters). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Filter (mathematics). ~ Wikipedia. #Math
Filters in topology. ~ Wikipedia. #Math
Set theory (in “The Stanford Encyclopedia of Philosophy”). ~ Joan Bagaria (@BagariaJoan). #Logic #Math
Set theory. ~ Joan Bagaria (@BagariaJoan). #Logic #Math
Models of set theory. ~ Joan Bagaria (@BagariaJoan). #Logic #Math #Set_theory
The mathematics of boolean algebra (in “The Stanford Encyclopedia of Philosophy”). ~ J. Donald Monk. #Logic #Math

18-Feb-21

Reflections on using Haskell for my startup. ~ Alistair Burrowes (@AlistairBuzz). #Haskell #FunctionalProgramming
Formalizing relations in type theory. ~ Farida Kachapova. #Logic #Math

17-Feb-21

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 (@chemacortes). #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

16-Feb-21

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

15-Feb-21

#SEP: Fallacies. ~ Hans Hansen. #Logic
#SEP: The algebra of logic tradition. ~ Stanley Burris, Javier Legris. #Logic

14-Feb-21

Kruskal’s algorithm implemented in Clojure. ~ Atabey Kaygun (@Atabey_Kaygun). #Clojure #Algorithms
Kruskal’s algorithm in Common Lisp. ~ Atabey Kaygun (@Atabey_Kaygun). #CommonLisp #Algorithms

13-Feb-21

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 (@EricaKlarreich). #Math #CompSci

12-Feb-21

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 (@chemacortes). #Python #Programming

11-Feb-21

The laws of large numbers (in Isabelle/HOL). ~ Manuel Eberl (@pruvisto). #ITP #IsabelleHOL #Math
Formalising mathematics: workshop 4 (topology). ~ Kevin Buzzard (@XenaProject). #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

10-Feb-21

IMO 2013 Q1 in Lean. ~ David Renshaw. #ITP #LeanProver #Math

09-Feb-21

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 (@chemacortes). #Python #Programming
The Ramanujan Machine is an intellectual fraud. #AI #Math

08-Feb-21

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 (@SandMouth). #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 (@HsinHaoYu). #Emacs

07-Feb-21

Folds are constructor substitution. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming

06-Feb-21

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

05-Feb-21

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

04-Feb-21

Formalising mathematics: Workshop 3 (Limits of sequences). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
What is a filter? How some computer scientists think about limits. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
What is a uniform space? How some computer scientists think about completions. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Superconnected left quasigroups and involutory quandles. ~ Marco Bonatto. #ATP #Prover9 #Math
Haskell’s @ symbol - Type application. ~ Zac Wood. #Haskell #FunctionalProgramming

03-Feb-21

The working programmer’s guide to setting up Haskell projects. ~ Jonas Carpay (@jonascarpay). #Haskell #FunctionalProgramming
El cifrado de los monjes cistercienses: de 0000 a 9999 con «símbolos raros». ~ @Alvy. #Matemáticas

02-Feb-21

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

01-Feb-21

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

January 2021

31-Jan-21

Paul Cohen, el matemático que por resolver un problema terminó creando dos mundos. ~ Dalia Ventura. #Matemáticas

30-Jan-21

HELIX: From math to verified code. ~ Vadim Zaliva. #PhD_Thesis #ITP #Coq #Math
Implementing the decomposition of soundness proofs of abstract interpreters in Coq. ~ Jens de Waard. #MSc_Thesis #ITP #Coq
Longest segment of balanced parentheses: an exercise in program inversion in a segment problem (Functional Pearl). ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming
A greedy algorithm for dropping digits (Functional Pearl). ~ Richard Bird, Shin-Cheng Mu. #Haskell #FunctionalProgramming

29-Jan-21

Formalising mathematics: Workshop 2 (Groups and subgroups). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Building a passphrase generator in Haskell. ~ Mathias Jean Johansen. #Haskell #FunctionalProgramming
What do we mean by equality? ~ Kevin Buzzard (@XenaProject). #Logic #Math
¿Cuántos infinitos existen?️ El teorema de Cantor. ~ Urtzi Buijs (@UrtziBuijs). #Matemáticas

28-Jan-21

IMO 2013 Q5 in Lean. ~ David Renshaw. #ITP #LeanProver #Math
Evolution of artificial intelligence languages, a systematic literature review. ~ Emmanuel Adetiba, Temitope John, Adekunle Akinrinmade, Funmilayo Moninuola, Oladipupo Akintade, Joke Badejo. #AI #Programming
Edición de textos científicos con LaTeX. (Composición, gráficos, Inkscape, Tikz y presentaciones Beamer). ~ Alexánder Borbón, Walter Mora. #LaTeX

27-Jan-21

IMO 2011 Q3 in Lean. ~ David Renshaw. #ITP #LeanProver #Math

26-Jan-21

Teaching algorithms and data structures with a proof assistant. ~ Tobias Nipkow. #ITP #IsabelleHOL
2-Adjoint equivalences in Homotopy Type Theory. ~ Daniel Carranza, Jonathan Chang, Krzysztof Kapulkin, Ryan Sandford. #ITP #LeanProver #HoTT
The Agda universal algebra library and Birkhoff’s theorem in Martin-Löf dependent type theory. ~ William DeMeo. #ITP #Agda #Math
Formal verification of authenticated, append-only skip lists in Agda. ~ Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. #ITP #Agda
A Haskell implementation of the Lyness-Moler’s numerical differentiation algorithm. ~ Weng Kin Ho, Chu Wei Lim. #Haskell #FunctionalProgramming #Math
Let’s not dumb down the history of computer science. ~ Donald E. Knuth, Len Shustek. #CompSci

25-Jan-21

Formalising mathematics: workshop 1. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math

24-Jan-21

Sums of consecutive reciprocals. ~ John D. Cook (@JohnDCook). #Math
Descubriendo la programación funcional: Lisp con Diego Sevilla (@diegosevilla). #Lisp #CommonLisp #ProgramaciónFuncional12

23-Jan-21

Las bases matemáticas de la programación funcional. ~ Héctor Iván Patricio Moreno. #ProgramaciónFuncional
Proceedings of the 2020 Scheme and Functional Programming Workshop. #FunctionalProgramming
Machine-learning mathematical structures. ~ Yang-Hui He. #MachineLearning #Math
Ten computer codes that transformed science. ~ Jeffrey M. Perkel. #CompSci via @vardi
Tablas para cálculos en org-mode. #Emacs #OrgMode

22-Jan-21

Teaching Haskell means teaching important concepts. ~ Jonathan Thaler (@JonathanThaler). #Haskell #FunctionalProgramming

21-Jan-21

Formalising mathematics: an introduction. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Capturing call stack with Haskell exceptions. ~ Maxim Koltsov (@maksbotan). #Haskell #FunctionalProgramming
[[https://lispcookbook.github.io/cl-cookbook][The Common Lisp Cookbook [in EPUB and PDF format]]]./#download-in-epub #eBook #CommonLisp
El número de Dottie. ~ M.A. Morales (@gaussianos). #Matemáticas

20-Jan-21

[[https://raw.githubusercontent.com/DSLsofMath/DSLsofMath/master/L/snapshots/DSLsofMathBook_snapshot_2021-01-17.pdf][Domain-specific languages of Mathematics [Draft of January 17, 2021]]]. ~ Patrik Jansson (@patrikja), Cezar Ionescu, Jean-Philippe Bernardy. #Haskell #FunctionalProgramming #Math
[[https://github.com/DSLsofMath/DSLsofMath][DSLsofMath: Domain-specific languages of Mathematics [Repo]]]. ~ Patrik Jansson (@patrikja) et als. #Haskell #FunctionalProgramming #Math

19-Jan-21

A novice-friendly induction tactic for Lean. ~ Jannis Limperg. #ITP #LeanProver
Towards Hoare logic for a small imperative language in Haskell. ~ Boro Sitnikovski (@BSitnikovski). #Haskell #FunctionalProgramming
Computer Science as the continuation of Logic by other means. ~ Georg Gottlob. #Logic #CompSci

18-Jan-21

[[https://leanprover-community.github.io/lt2021/slides/thomas-LT2021-Galois-Theory.pdf][Formalizing Galois Theory in Lean [Slides]]]. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math
[[https://youtu.be/-6z6qTD_vv8][Formalizing Galois Theory in Lean [Vídeo]]]. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math
Las Matemáticas son suficientes para mí. ~ Juan Arias de Reyna. #Matemáticas
org-special-block-extras (A unified interface for special blocks and links: defblock). ~ Musa Al-hassy./#Judgements-Inference-rules-and-proof-trees #Emacs #OrgMode

16-Jan-21

Model theory in Lean. ~ Vaibhav Karve. #ITP #LeanProver #Logic
Machine-checked computer-aided mathematics. ~ Assia Mahboubi. #ITP #Coq #Math
Towards efficient and verified virtual machines for dynamic languages. ~ Martin Desharnais, Stefan Brunthaler. #ITP #IsabelleHOL
From Aristotle to the iPhone. ~ Moshe Y. Vardi (@vardi). #Logic #CompSci

15-Jan-21

Axiomatic Geometry in Lean. ~ Vaibhav Karve, Lawrence Zhao, Edward Kong, Alex Dolcos, Nicholas Phillips. #ITP #LeanProver #Math
[[https://youtu.be/K-kLck8BvDM][Axiomatic Geometry in Lean [Video]]]. ~ Vaibhav Karve. #ITP #LeanProver #Math
[[https://github.com/vaibhavkarve/leanteach2020][Axiomatic Geometry in Lean [Code]]]. ~ Vaibhav Karve, Lawrence Zhao, Edward Kong, Alex Dolcos, Nicholas Phillips. #ITP #LeanProver #Math
Lebesgue integration. (Detailed proofs to be formalized in Coq). ~ François Clément, Vincent Martin. #ITP #Coq #Math
Permutate parsers, don’t validate. ~ Ju Liu (@arkh4m). #Haskell #FunctionalProgramming
An introduction to ghc-debug: precise memory analysis for Haskell programs. ~ Matthew Pickering. #Haskell #FunctionalProgramming
Why exactly I want Boring Haskell to happen. ~ Artyom Kazak (@availablegreen). #Haskell #FunctionalProgramming
Beginner’s guide to mathematical constructivism. ~ Jan Gronwald. #Math
En toute logique: une origine de l’ordinateur. ~ Frédéric Prost. #Logic #CompSci
Publicar HTML con Org-Mode. #Emacs #OrgMode

14-Jan-21

A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. ~ Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer. #ITP #IsabelleHOL
A formal proof of PAC learnability for decision stumps. ~ Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan. #ITP #LeanProver
The friendship theorem in Lean. ~ Aaron Anderson. #ITP #LeanProver #Math
CertRL: Formalizing convergence proofs for value and policy iteration in Coq. ~ Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry Trager, Nathan Fulton. #ITP #Coq
Abel-Ruffini Theorem as a Mathematical Component. ~ Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. #ITP #Coq #Math
Making an IO. ~ Lúcás Meier (@cronokirby). #Haskell #FunctionalProgramming

13-Jan-21

Contextual refinement of the Michael-Scott queue (Proof pearl). ~ Simon Friis Vindum, Lars Birkedal. #ITP #Coq
Reasoning about monotonicity in separation logic. ~ Amin Timany, Lars Birkedal. #ITP #Coq
Developing and certifying Datalog optimizations in Coq/MathComp. ~ Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin. #ITP #Coq
An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR. ~ Max W. Haslbeck, René Thiemann. #ITP #IsabelleHOL #Haskell
Certified quantum computation in Isabelle/HOL. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL

12-Jan-21

[[http://alexjbest.github.io/talks/lean-generalisation][Automatically generalising theorems using typeclasses in Lean [Slides]]]. ~ Alex J. Best./#/#ITP #LeanProver #Math
[[https://bostonu.zoom.us/rec/play/yPZ5hwU7T5C2wwAUYMKEwed7Y83lsvPEci6CP-AiIel8A9u05OHbOLcAy-mi__tqgg3vBDvhXc4wVY_p.B9N6zDkf2SMpf2Nh?startTime=1609940780000][Automatically generalising theorems using typeclasses in Lean [Video]]]. ~ Alex J. Best. #ITP #LeanProver #Math
Implementation of two layers type theory in Dedukti and application to Cubical Type Theory. ~ Bruno Barras, Valentin Maestracci. #ITP #Dedukti
Lean Together 2021. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Formalizing category theory in Agda. ~ Jason Z.S. Hu, Jacques Carette. #ITP #Agda #CategoryTheory #Math
Formal verification of semi-algebraic sets and real analytic functions. ~ J. Tanner Slagel, Lauren White, Aaron Dutle. #ITP #PVS #Math
On the formalisation of Kolmogorov complexity. ~ Elliot Catt, Michael Norrish. #ITP #HOL4
Haskell: (.) . (.) explained (Let’s get a grasp of composition equivalences in Haskell). #Haskell #FunctionalProgramming

11-Jan-21

Formalizing the ring of Witt vectors. ~ Robert Y. Lewis. #ITP #LeanProver #Math
Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading. ~ Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber. #ITP #HOL4
Object-level reasoning with logics encoded in HOL Light. ~ Petros Papapanagiotou, Jacques Fleuriot. #ITP #HOL_Light #Logic
Deductive systems and coherence for skew prounital closed categories. ~ Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. #ITP #Agda
Why Haskell is our first choice for building production software systems. ~ Christian Charukiewicz (@charukiewicz). #Haskell #FunctionalProgramming

10-Jan-21

144 is the largest square in the Fibonacci Sequence (A formalisation of Cohn’s Proof). ~ Harun Khan #ITP #LeanProver #Math via @XenaProject
The Eudoxus real numbers in Lean. ~ Xiang Li. #ITP #LeanProver #Math via @XenaProject
Set theory, type theory and the future of proof verification software. ~ James Palmer. #ITP #LeanProver #Math via @XenaProject
A formal proof of correctness of a recursive integer square root algorithm. ~ Mark Dickinson. #ITP #LeanProver #Math

09-Jan-21

Schemes in Lean. ~ Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, Scott Morrison. #ITP #LeanProver #Math
Performance aspects of correctness-oriented synthesis flows. ~ F. Bornebusch, C. Lüth, R. Wille, R. Drechsler. #ITP #Coq
An anti-locally-nameless approach to formalizing quantifiers. ~ Olivier Laurent. #ITP #Coq
Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2. ~ David M. Russinoff. #ITP #ACL2
Formalizing 100 theorems. ~ Freek Wiedijk. #ITP #Math
Formalizing 100 theorems in Lean. #ITP #Math #LeanProver
Trouble in paradise: Fibonacci. #Haskell #FunctionalProgramming
Indexed optics dilemma. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming
Algorithmic problem solving. ~ Johan Sannemo. #eBook #Programming #Algorithms
La saga del infinito, de Mates Mike. ~ M.A. Morales (@gaussianos). #Matemáticas

08-Jan-21

[[https://youtu.be/eSXiClL4COw][LeanStep: a dataset and environment for (interactive) neural theorem proving [Video]]]. ~ Jason Rute. #ITP #Leanprover #MachineLearning
[[https://docs.google.com/presentation/d/1poOu2gP9mSGAdAFvOupHvf4tpgD33jACQLJAVcphA1g/edit?usp=sharing][LeanStep: a dataset and environment for (interactive) neural theorem proving [Slides]]]. ~ Jason Rute. #ITP #Leanprover #MachineLearning
Theorem proving and algebra. ~ Joseph A. Goguen. #eBook #ITP #Math
Elementary programming. ~ Michael Peyton Jones. #Haskell #Programming
A first look at info table profiling. ~ Matthew Pickering, David Eichmann. #Haskell #FunctionalProgramming
Benchmarks of discrimination package. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming
CLP(FD) and CLP(ℤ): Prolog integer arithmetic. ~ Markus Triska (@MarkusTriska). #Prolog #LogicProgramming #CLP
ECLIPSE (A tutorial introduction). ~ Andrew M. Cheadle et als. #Prolog #LogicProgramming #CLP
Programación lógica con restricciones. #Prolog #CLP
Soluciones lógicas de problemas lógicos. #Prolog #ProgramaciónLógica #CLP

07-Jan-21

ACL2 induction heuristics. ~ J Strother Moore. #ITP #ACL2
Word problem for one-relator groups. ~ Chris Hughes. #ITP #LeanProver #Math
A Lean introduction to pure mathematics. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Logic #Math
MTH1001 (Mathematical structures) in Lean. ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Logic #Math
EMS reals (A project for investigating the real number system via the interactive theorem prover Lean). ~ Gihan Marasingha (@gihanmarasingha). #ITP #LeanProver #Logic #Math
Lassie: HOL4 tactics by example. ~ Heiko Becker et als.. #ITP #HOL4
Formalizing domain models of the typed and the untyped lambda calculus in Agda. ~ David Lidell. #MSc_Thesis #ITP #Agda

06-Jan-21

On the unreasonable effectiveness of SAT Solvers. ~ Vijay Ganesh, Moshe Y. Vardi. #Logic #ATP #SAT_Solvers
Riemann Hypothesis in Lean. ~ Brandon H. Gomes (@brandonhgomes), Alex Kontorovich. #ITP #LeanProver #Math
[[https://leanprover-community.github.io/lt2021/slides/Macbeth-slides.pdf][An example of a manifold [Slides]]]. ~ Heather Macbeth. #ITP #LeanProver #Math
[[https://youtu.be/deppJ2q_5a0][An example of a manifold [Video]]]. ~ Heather Macbeth. #ITP #LeanProver #Math
Symbolic computation in Maude: Some tapas. ~ José Meseguer. #ITP #Maude
Compile-time evaluation in Haskell. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
Predictions for 2021. | Gödel’s Lost Letter and P = NP. ~ R.J. Lipton & K.W. Regan. #CompSci

05-Jan-21

Formalizing Hall’s Marriage Theorem in Lean. ~ Alena Gusakov, Bhavik Mehta, Kyle A. Miller. #ITP #LeanProver #Math
Finiteness in cubical type theory. ~ Donnacha Oisín Kidney (@oisdk). #MSc_Thesis #ITP #Agda #HoTT
An overview of Lean 4. ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver
[[https://leanprover-community.github.io/lt2021/slides/floris-measure.pdf][Measure theory in Lean [slides]]]. ~ Floris van Doorn. #ITP #LeanProver #Math
[[https://youtu.be/yH3-zE0bYCU][Measure theory in Lean [video]]]. ~ Floris van Doorn. #ITP #LeanProver #Math
The visitor pattern is essentially the same thing as Church encoding. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
Functional Pearl: It’s easy as 1,2,3. ~ Graham Hutton. #Haskell #FunctionalProgramming
Trying to compose non-composable: monads. ~ Murat Kasimov. #Haskell #FunctionalProgramming
Learning TypeFamilies together! ~ Flavio Corpa (@FlavioCorpa). #Haskell #FunctionalProgramming

04-Jan-21

Tautology checkers in Isabelle and Haskell. ~ Jørgen Villadsen. #Logic #ITP #IsabelleHOL #Haskell #FunctionalProgramming
Theorem proving for Lewis logics of counterfactual reasoning. ~ Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato. #ATP #Logic #Prolog #LogicProgramming
Deterministic Finite Automata (DFA) in Lean. ~ Fox Thomson. #ITP #LeanProver
Nondeterministic Finite Automata (NFA) in Lean. ~ Fox Thomson. #ITP #LeanProver
Theory of iteration and recursion. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming
[[https://bindthegap.news/issues/02dec2020.html][Bind the gap (Monthly digital functional programming magazine) [Issue 2, Dec 2020]]]. #Haskell #FunctionalProgramming
Mirror mirror: Reflection and encoding via. ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming
Lessons learned from a year of writing Haskell. ~ Adam Wespiser (@wespiser). #Haskell #FunctionalProgramming
Coindexed optics. ~ Oleg Grenrus (@phadej).l#Haskell #FunctionalProgramming

03-Jan-21

Dihedral groups in Lean. ~ Shing Tak Lam. #ITP #LeanProver #Math

02-Jan-21

Verifying C11-style weak memory libraries. ~ Sadegh Dalvandi, Brijesh Dongol. #ITP #IsabelleHOL
Lean 4 manual. #Lean4 #FunctionalProgramming #ITP
Formalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu. #ITP #Coq #Math
A Coq formalization of data provenance. Véronique Benzaken et als. #ITP #Coq
Synthetic undecidability proofs in Coq. ~ Dominik Kirst. #ITP #Coq

01-Jan-21

Two reasons why you found learning haskell hard. ~ School of FP (@schooloffp). #Haskell #FunctionalProgramming
Learn just enough about linear types. ~ Artyom Kazak (@availablegreen). #Haskell #FunctionalProgramming

camilochs/Lecturas_GLC