Lecturas del año 2020.org

Lecturas del Grupo de Lógica Computacional durante el año 2020

Este repositorio es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el año 2020. La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

Contenido

• Diciembre de 2020
  • 31-Dic-20
  • 30-Dic-20
  • 29-Dic-20
  • 28-Dic-20
  • 27-Dic-20
  • 26-Dic-20
  • 24-Dic-20
  • 23-Dic-20
  • 22-Dic-20
  • 21-Dic-20
  • 20-Dic-20
  • 19-Dic-20
  • 18-Dic-20
  • 17-Dic-20
  • 16-Dic-20
  • 15-Dic-20
  • 14-Dic-20
  • 13-Dic-20
  • 12-Dic-20
  • 11-Dic-20
  • 10-Dic-20
  • 09-Dic-20
  • 08-Dic-20
  • 07-Dic-20
  • 06-Dic-20
  • 05-Dic-20
  • 04-Dic-20
  • 03-Dic-20
  • 02-Dic-20
  • 01-Dic-20
• Noviembre de 2020
  • 30-Nov-20
  • 29-Nov-20
  • 28-Nov-20
  • 27-Nov-20
  • 26-Nov-20
  • 25-Nov-20
  • 24-Nov-20
  • 22-Nov-20
  • 21-Nov-20
  • 20-Nov-20
  • 19-Nov-20
  • 18-Nov-20
  • 17-Nov-20
  • 15-Nov-20
  • 14-Nov-20
  • 13-Nov-20
  • 12-Nov-20
  • 11-Nov-20
  • 10-Nov-20
  • 09-Nov-20
  • 08-Nov-20
  • 07-Nov-20
  • 06-Nov-20
  • 05-Nov-20
  • 04-Nov-20
  • 03-Nov-20
  • 02-Nov-20
  • 01-Nov-20
• Octubre de 2020
  • 31-Oct-20
  • 30-Oct-20
  • 29-Oct-20
  • 28-Oct-20
  • 27-Oct-20
  • 25-Oct-20
  • 24-Oct-20
  • 22-Oct-20
  • 21-Oct-20
  • 20-Oct-20
  • 19-Oct-20
  • 18-Oct-20
  • 17-Oct-20
  • 16-Oct-20
  • 15-Oct-20
  • 14-Oct-20
  • 13-Oct-20
  • 12-Oct-20
  • 11-Oct-20
  • 10-Oct-20
  • 09-Oct-20
  • 08-Oct-20
  • 07-Oct-20
  • 06-Oct-20
  • 05-Oct-20
  • 04-Oct-20
  • 03-Oct-20
  • 02-Oct-20
  • 01-Oct-20
• Septiembre de 2020
  • 30-Sep-20
  • 29-Sep-20
  • 28-Sep-20
  • 26-Sep-20
  • 25-Sep-20
  • 24-Sep-20
  • 23-Sep-20
  • 22-Sep-20
  • 20-Sep-20
  • 19-Sep-20
  • 18-Sep-20
  • 17-Sep-20
  • 16-Sep-20
  • 15-Sep-20
  • 14-Sep-20
  • 13-Sep-20
  • 12-Sep-20
  • 11-Sep-20
  • 10-Sep-20
  • 09-Sep-20
  • 08-Sep-20
  • 06-Sep-20
  • 05-Sep-20
  • 03-Sep-20
  • 02-Sep-20
  • 01-Sep-20
• Agosto de 2020
  • 31-Ago-20
  • 29-Ago-20
  • 28-Ago-20
  • 27-Ago-20
  • 26-Ago-20
  • 25-Ago-20
  • 24-Ago-20
  • 23-Ago-20
  • 22-Ago-20
  • 21-Ago-20
  • 20-Ago-20
  • 19-Ago-20
  • 18-Ago-20
  • 17-Ago-20
  • 16-Ago-20
  • 15-Ago-20
  • 14-Ago-20
  • 13-Ago-20
  • 12-Ago-20
  • 11-Ago-20
  • 10-Ago-20
  • 09-Ago-20
  • 08-Ago-20
  • 05-Ago-20
  • 04-Ago-20
  • 03-Ago-20
  • 02-Ago-20
• Julio de 2020
  • 01-Jul-20
  • 02-Jul-20
  • 03-Jul-20
  • 04-Jul-20
  • 05-Jul-20
  • 06-Jul-20
  • 07-Jul-20
  • 09-Jul-20
  • 10-Jul-20
  • 11-Jul-20
  • 12-Jul-20
  • 13-Jul-20
  • 14-Jul-20
  • 15-Jul-20
  • 16-Jul-20
  • 17-Jul-20
  • 18-Jul-20
  • 19-Jul-20
  • 20-Jul-20
  • 21-Jul-20
  • 22-Jul-20
  • 23-Jul-20
  • 24-Jul-20
  • 24-Jul-20
  • 25-Jul-20
  • 25-Jul-20
  • 26-Jul-20
  • 28-Jul-20
  • 30-Jul-20
  • 31-Jul-20
• Junio de 2020
  • 01-Jun-20
  • 03-Jun-20
  • 04-Jun-20
  • 05-Jun-20
  • 06-Jun-20
  • 07-Jun-20
  • 08-Jun-20
  • 09-Jun-20
  • 10-Jun-20
  • 11-Jun-20
  • 12-Jun-20
  • 13-Jun-20
  • 14-Jun-20
  • 15-Jun-20
  • 16-Jun-20
  • 17-Jun-20
  • 18-Jun-20
  • 19-Jun-20
  • 20-Jun-20
  • 21-Jun-20
  • 22-Jun-20
  • 23-Jun-20
  • 24-Jun-20
  • 25-Jun-20
  • 26-Jun-20
  • 27-Jun-20
  • 28-Jun-20
  • 29-Jun-20
  • 30-Jun-20
• Mayo de 2020
  • 1-May-20
  • 2-May-20
  • 3-May-20
  • 4-May-20
  • 5-May-20
  • 6-May-20
  • 8-May-20
  • 9-May-20
  • 10-May-20
  • 11-May-20
  • 12-May-20
  • 14-May-20
  • 15-May-20
  • 16-May-20
  • 17-May-20
  • 18-May-20
  • 19-May-20
  • 20-May-20
  • 21-May-20
  • 22-May-20
  • 23-May-20
  • 24-May-20
  • 25-May-20
  • 26-May-20
  • 27-May-20
  • 28-May-20
  • 29-May-20
  • 30-May-20
  • 31-May-20
• Abril de 2020
  • 01-Abr-20
  • 02-Abr-20
  • 03-Abr-20
  • 04-Abr-20
  • 06-Abr-20
  • 07-Abr-20
  • 08-Abr-20
  • 09-Abr-20
  • 10-Abr-20
  • 11-Abr-20
  • 12-Abr-20
  • 13-Abr-20
  • 14-Abr-20
  • 16-Abr-20
  • 17-Abr-20
  • 18-Abr-20
  • 19-Abr-20
  • 21-Abr-20
  • 23-Abr-20
  • 25-Abr-20
  • 27-Abr-20
  • 28-Abr-20
  • 29-Abr-20
  • 30-Abr-20
• Marzo de 2020
  • 01-Mar-20
  • 02-Mar-20
  • 03-Mar-20
  • 04-Mar-20
  • 05-Mar-20
  • 06-Mar-20
  • 07-Mar-20
  • 08-Mar-20
  • 09-Mar-20
  • 10-Mar-20
  • 11-Mar-20
  • 12-Mar-20
  • 13-Mar-20
  • 14-Mar-20
  • 15-Mar-20
  • 18-Mar-20
  • 20-Mar-20
  • 21-Mar-20
  • 22-Mar-20
  • 23-Mar-20
  • 24-Mar-20
  • 26-Mar-20
  • 27-Mar-20
  • 28-Mar-20
  • 31-Mar-20
• Febrero de 2020
  • 01-Feb-20
  • 02-Feb-20
  • 03-Feb-20
  • 04-Feb-20
  • 05-Feb-20
  • 06-Feb-20
  • 07-Feb-20
  • 08-Feb-20
  • 09-Feb-20
  • 10-Feb-20
  • 11-Feb-20
  • 12-Feb-20
  • 13-Feb-20
  • 15-Feb-20
  • 16-Feb-20
  • 17-Feb-20
  • 18-Feb-20
  • 19-Feb-20
  • 20-Feb-20
  • 21-Feb-20
  • 22-Feb-20
  • 23-Feb-20
  • 24-Feb-20
  • 25-Feb-20
  • 26-Feb-20
  • 27-Feb-20
  • 28-Feb-20
  • 29-Feb-20
• Enero de 2020
  • 01-Ene-20
  • 02-Ene-20
  • 03-Ene-20
  • 04-Ene-20
  • 05-Ene-20
  • 06-Ene-20
  • 07-Ene-20
  • 08-Ene-20
  • 09-Ene-20
  • 10-Ene-20
  • 11-Ene-20
  • 12-Ene-20
  • 13-Ene-20
  • 14-Ene-20
  • 15-Ene-20
  • 16-Ene-20
  • 17-Ene-20
  • 18-Ene-20
  • 19-Ene-20
  • 20-Ene-20
  • 21-Ene-20
  • 22-Ene-20
  • 23-Ene-20
  • 24-Ene-20
  • 25-Ene-20
  • 26-Ene-20
  • 27-Ene-20
  • 28-Ene-20
  • 28-Ene-20
  • 30-Ene-20
  • 31-Ene-20

Diciembre de 2020

31-Dic-20

• Dijkstra monads forever: termination-sensitive specifications for interaction trees. ~ Lucas Silver, Steve Zdancewic. #ITP #Coq
• A minimalistic verified bootstrapped compiler (Proof Pearl). ~ Magnus O. Myreen. #ITP #HOL4
• Advent of Code 2020: Haskell solution reflections for all 25 days. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
• Haskell tutorial and cookbook, Second edition. ~ Mark Watson. #eBook #Haskell #FunctionalProgramming
• Examples for “Haskell tutorial and cookbook, Second edition”. ~ Mark Watson. #Haskell #FunctionalProgramming
• Functional programming: Enemy of the state. ~ Onur Gümüş (@OnurGumusDev). #FunctionalProgramming

30-Dic-20

• The simplest MonadFail instance. ~ Kazuki Okamoto (@kakkun61). #Haskell #FunctionalProgramming
• StateT vs IORef: a benchmark. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming

29-Dic-20

• Irrationality and transcendence criteria for infinite series in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence Paulson. #ITP #IsabelleHOL #Math
• Learnings from solving Advent of Code 2020 in Haskell. ~ Abhinav Sarkar (@abhin4v). #Haskell #FunctionalProgramming
• Haskell type-level functions shenanigans (An introduction to some useful language extensions). ~ Antoine Leblanc (@nicuveo). #Haskell #FunctionalProgramming
• Ephemeral purely functional data structure and linear type. ~ Kazuki Okamoto (@kakkun61). #Haskell #FunctionalProgramming
• Programming language families (Procedural, object oriented, logic, and functional languages). ~ Jobelle Firme, Nicolas Valera, Yunus Canemre, Stephen Burchill, Beenish Khurshid. #Programming

28-Dic-20

• Cofinality and the delta system lemma (in Isabelle). ~ Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic #Math
• Counting bits with Haskell (The bad and the good way). ~ Flavio Corpa (@FlavioCorpa). #Haskell #FunctionalProgramming
• (Haskell in Haskell) 3: Parsing. ~ Lúcás Meier (@cronokirby). #Haskell #FunctionalProgramming
• My first type theory. ~ Arved Friedemann. #TypeTheory

27-Dic-20

• Trees indexed by a Cayley Monoid. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming

26-Dic-20

• Lean prover: Frequently Asked Questions. #ITP #LeanProver
• Monad transformers and effects with Backpack. ~ Ollie Charles (@acid2). #Haskell #FunctionalProgramming
• Refactoring using type classes and optics. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming
• Santa Wrap. ~ Lucas Di Cioccio (@lucasdicioccio). #Haskell #FunctionalProgramming #MiniZinc
• Essential thinking. The art of creative thinking for problem solving. ~ Antoni Ligeza. #ProblemSolving #Prolog #CLP #AI
• A Lisp programmer living in Python-land: The Hy programming language. ~ Mark Watson (@mark_l_watson). #eBook #Lisp #Python #Programmig
• Python programming and scientific computation. ~ Tran Nam Trung. #eBook #Python #Programming
• Descubriendo la programación funcional: Elixir con Erick Navarro (@erickgnavar). #Elixir #ProgramaciónFuncional vía @republicawebes

24-Dic-20

• Formalization of Euler summation formula (in Lean). ~ Marc Masdeu (@marcmasdeu). #ITP #LeanProver #Math
• For a few dollars more (Verified fine-grained algorithm analysis down to LLVM). ~ Maximilian P. L. Haslbeck, Peter Lammich. #ITP #IsabelleHOL
• Towards formally verified compilation of tag-based policy enforcement. ~ CHR Chhak, Andrew Tolmach, Sean Anderson. #ITP #Coq
• λS: Computable semantics for differentiable programming with higher-order functions and datatypes. ~ Benjamin Sherman, Jesse Michel, Michael Carbin. #Haskell #FunctionalProgramming
• The year in Math and Computer Science. ~ Bill Andrews. #Math #CompSci
• Lisp, Slime y Emacs. #Lisp #Emacs

23-Dic-20

• Topological semantics for paraconsistent and paracomplete logics. ~ David Fuenmayor. #ITP #IsabelleHOL #Math
• Don’t think, just defunctionalize. ~ Joachim Breitner (@nomeata). #Haskell #FunctionalProgramming
• Sistemas deductivos proposicionales. ~ Fernando Sancho (@sanchocaparrini). #Lógica

22-Dic-20

• A concise sequent calculus for teaching first-order logic. ~ Asta Halkjær From, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
• The generalised continuum hypothesis implies the axiom of choice in Coq. ~ Dominik Kirst, Felix Rech. #ITP #Coq #Logic #Math
• GeoGebra reasoning tools for humans and for automatons. ~ Zoltán Kovács, Tomás Recio. #ATP #GeoGebra #Math
• Lower case Haskell. ~ @tonyday567. #Haskell #FunctionalProgramming #AdventOfHaskell
• Optics by example cheat sheets. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming

21-Dic-20

• Reconciling concepts from FP and OOP. ~ Thomas Mahler. #Haskell #FunctionalProgramming #AdventOfHaskell
• vector: Efficient packed-memory data representations. ~ @FPComplete. #Haskell #FunctionalProgramming
• Scripting the Hell out of Trello with Haskell. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming #AdventOfHaskell

20-Dic-20

• A Coq proof of the correctness of X25519 in TweetNaCl. ~ P. Schwabe, B. Viguier, T. Weerwag, F. Wiedijk. #ITP #Coq
• Dependently typed folds (folds that change type at each step!). ~ Ryan Orendorff. #Haskell #FunctionalProgramming #AdventOfHaskell
• Getting acquainted with Lens (part 1). ~ Pawel Szulc (@EncodePanda). #Haskell #FunctionalProgramming
• Foo to bar: Naming conventions in Haskell. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
• Descubriendo la programación funcional: Haskell con Héctor Navarro. #Haskell #ProgramaciónFuncional

19-Dic-20

• An experience report on writing usable DSLs in Coq. ~ Clément Pit-Claudel, Thomas Bourgeat. #ITP #Coq
• Hackage search: Regex-based online code search. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
• Haskell study plan. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming
• Classical programming topics with functional programming. ~ Visnovitz Márton #FunctionalProgramming #TypeScript
• Logic: A study guide. ~ Peter Smith (@PeterSmith). #Logic

18-Dic-20

• Formalization of PAL⋅S5 in proof assistant. ~ Jiatu Li. #ITP #LeanProver #Logic
• Formal proof of the main theorem for surreal. ~ Jiatu Li. #ITP #LeanProver
• An introduction to property-based testing with QuickCheck. ~ Jesper Cockx (@dregntael). #Haskell #FunctionalProgramming #QuickCheck
• Beauty and the bytestring. ~ Norman Liu. #Haskell #FunctionalProgramming #AdventOfHaskell
• Haskell memoization and evaluation model. ~ Boro Sitnikovski (@BSitnikovski). #Haskell #FunctionalProgramming

17-Dic-20

• A novice-friendly induction tactic for Lean. ~ Jannis Limperg. #ITP #LeanProver
• Talking about Toys. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming #AdventOfHaskell
• Haskell - Doomed to succeed? ~ Ari Fordsham. #Haskell #FunctionalProgramming

16-Dic-20

• A new perspective of paramodulation complexity by solving massive 8 puzzles. ~ Ruo Ando, Yoshiyasu Takefuji. #ATP #Otter
• The Fibonacci sequence as a functor. ~ Tai-Danae Bradley (@math3ma). #CategoryTheory
• A vivid christmas carol. #Haskell #FuncionalProgramming #AdventOfHaskell

15-Dic-20

• On the Lean proof assistant, Part 1. ~ Jason Polak. #ITP #LeanProver
• On the formal verification of the Stellar Consensus Protocol. ~ G. Losa, M. Dodds. #ITP #IsabelleHOL
• Authenticated data structures as functors in Isabelle/HOL. ~ A. Lochbihler, O. Marić. #ITP #IsabelleHOL
• On the use of formal methods to model and verify neuronal archetypes. ~ E. de Maria et als. #ITP #Coq
• Mechanized formal model of bitcoin’s blockchain validation procedures. ~ K. Rupić, L. Rožić, A. Derek. #ITP #Coq
• Enumerating trees. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming #Agda
• Pattern matching. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming
• At the interface of algebra and statistics. ~ Tai-Danae Bradley (@math3ma). #Math #CategoryTheory
• Personal website in org. #Emacs #OrgMode

14-Dic-20

• Precise typing implies functional programming. ~ Pavel Potoček. #Haskell #FunctionalProgramming
• Structure your errors. ~ Tikhon Jelvis (@tikhonjelvis). #Haskell #FunctionalProgramming #AdventOfHaskell

13-Dic-20

• Roll your own Holly Jolly streaming combinators with Free. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming #AdventOfHaskell

12-Dic-20

• Asymptotic reasoning in a proof assistant. ~ Manuel Eberl. #PhD_Thesis #ITP #IsabelleHOL #Math
• An answer to the Bose-Nelson sorting problem for 11 and 12 channels. ~ Jannis Harder. #ITP #IsabelleHOL
• Programmer = démontrer? La correspondance de Curry-Howard aujourd’hui. ~ Xavier Leroy. #Logic #Math #CompSci #ITP
• (Haskell in Haskell) 0. Introduction. ~ Lúcás Meier (@cronokirby). #Haskell #FunctionalProgramming
• (Haskell in Haskell) 1. Setup. ~ Lúcás Meier (@cronokirby). #Haskell #FunctionalProgramming
• (Haskell in Haskell) 2. Lexing. ~ Lúcás Meier (@cronokirby) #Haskell #FunctionalProgramming
• Functional Christmas (2020). #FunctionalProgramming
• Elm Christmas (2020). #Elm #FunctionalProgramming
• How the slowest computer programs illuminate math’s fundamental limits. ~ John Pavlus (@johnpavlus). #Math #CompSci
• Patterns that eventually fail. ~ John Baez (@johncarlosbaez). #Math
• Emacs family editors. #Emacs

11-Dic-20

• The future of Mathematics? ~ R.J. Lipton. #ITP #Math
• The ‘retry’ package. ~ Wander Hillen. #Haskell #FunctionalProgramming #AdventOfHaskell
• Haskell coreutils: tee. ~ Austin Gandalf. #Haskell #FunctionalProgramming
• Parser combinators: a walkthrough (Or: Write you a Parsec for great good). ~ Antoine Leblanc (@nicuveo). #Haskell #FunctionalProgramming
• The shrinks applicative. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• sydtest: An experimental testing framework for Haskell. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming

10-Dic-20

• A SAT-based resolution of Lam’s problem. ~ Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh. #ATP #SAT_Solvers #Math
• Extracting smart contracts tested and verified in Coq. ~ D. Annenkov, M. Milo, J.B. Nielsen, B. Spitters. #ITP #Coq
• Simpler and safer API design using GADTs. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming #AdventOfHaskell
• “A damn stupid thing to do” - the origins of C. ~ Richard Jensen. #Programming

09-Dic-20

• Denotational design. ~ Armando Santos (@_bolt12). #Haskell #FunctionalProgramming #AdventOfHaskell
• What is functional programming? ~ Mike Loukides (@mikeloukides). #FunctionalProgramming
• Favorite Emacs packages. ~ Bozhidar Batsov. #Emacs

08-Dic-20

• The relational method with message anonymity for the verification of cryptographic protocols. ~ Pasquale Noce. #ITP #IsabelleHOL
• Relational minimum spanning tree algorithms (in Isabelle/HOL). ~ Walter Guttmann, Nicolas Robinson-O’Brien. #ITP #IsabelleHOL #Algorithms
• Computable analysis for verified exact real computation. ~ M. Konečný, F. Steinberg, H. Thies. #ITP #Coq #Math
• Mechanized verification of a fine-grained concurrent queue from Facebook’s Folly library. ~ S.F. Vindum, D. Frumin, L. Birkedal. #ITP #Coq
• The Pigeonhole principle. ~ Jonathan Prieto-Cubides (@jonacubides). #ITP #Agda #Math
• The halting problem (part 1). ~ Callan McGill. #Haskell #FunctionalProgramming #Logic #Math
• The halting problem (part 2). ~ Callan McGill. #ITP #Agda #Logic #Math
• Voevodsky’s unachieved project. ~ Andrei Rodin. #ITP #Math
• Haskell documentation with Haddock: Wishes’n’tips. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming
• The development of proof theory. ~ Jan von Plato. #Logic #ATP
• Automated reasoning. ~ Frederic Portoraro. #ATP #ITP #Logic #Math #LogicProgramming
• Benefits of statically typed functional programming? Wrong question. ~ Mikael Tönnberg. #FunctionalProgramming #AdventOfHaskell
• Cultures of programming: Understanding the history of programming through controversies and technical artifacts. ~ Tomas Petricek (@tomaspetricek). #Programming #Emacs

07-Dic-20

• Whirlwind tour of Stack for beginners. ~ School of FP (@schooloffp). #Haskell #FunctionalProgramming
• Bits instance of Integer. ~ Ken T Takusagawa. #Haskell #FuncionalProgramming
• Capturing the magic of Prelude.interact. ~ Samuel (@haskell_cat). #Haskell #FuncionalProgramming #AdventOfHaskell

06-Dic-20

• Liquid tensor experiment. ~ Peter Scholze. #ITP #LeanProver #Math
• Named goals in Coq. ~ Joachim Breitner (@nomeata). #ITP #Coq
• The group-theory package. ~ Emily Pillmore (@pitopos). #Haskell #FunctionalProgramming #Math
• Building a bulletin board using Scotty and friend. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming
• Ambassadors of Logic. #Logic

05-Dic-20

• Lolisa: Formal syntax and semantics for a subset of the Solidity programming language in mathematical tool Coq. ~ Zheng Yang. #ITP #Coq
• The Haskell runtime is what sets it apart from the competition. ~ Harpo Roeder (@HarpoRoeder). #Haskell #FunctionalProgramming
• Processing CodeBlocks in Hakyll. ~ Mario Lang. #Haskell #FunctionalProgramming #Hakyll #AdventOfHaskell
• Una recopilación de algoritmos para calcular el valor del número π. ~ @Alvy. #Matemáticas #Algoritmos #Programación
• Yet another π computation algorithms. ~ Thomas Joly. #Math #Algorithms #Programming
• NandGame: un juego de lógica binaria en el que hay que construir circuitos cada vez más complejos. ~ @Alvy. #Lógica #Computación
• The Nand Game. #Logic #CompSci

04-Dic-20

• The Free Num is a Sequence of Bags. ~ Tony Day (@tonyday567). #Haskell #FunctionalProgramming #AdventOfHaskell
• Haskell, in Elm terms: Type Classes. ~ @terezk_a #Haskell #FuncionalProgramming #Elm

03-Dic-20

• Another tool in the box: Why use formal methods for autonomous systems? ~ Matt Luckcuck. #FormalMethods
• My journey into Haskell. ~ Gustavo Franke. #Haskell #FunctionalProgramming
• Complicated Haskell words - Isomorphism. ~ Ju Liu (@arkh4m). #Haskell #FunctionalProgramming
• Composition in trick-taking card games. ~ Ben Fiedler. #Haskell #FunctionalProgramming
• Advent of Code 2020 with Haskell. ~ Ariel Kwiatkowski (@RedTachyon). #Haskell #FunctionalProgramming #AdventOfCode
• An experience report on writing usable DSLs in Coq. ~ Clément Pit-Claudel, Thomas Bourgeat. #ITP #Coq

02-Dic-20

• Program = Proof. ~ Samuel Mimram. #eBook #Logic #Math #ITP #Agda
• Finite map extras (in Isabelle/HOL). ~ Javier Díaz. #ITP #IsabelleHOL
• Haskell solutions to Advent of Code 2020. #Haskell #FunctionalProgramming #AdventOfCode
• Haskell solutions to Advent of Code 2020. ~ Justin Le. #Haskell #FunctionalProgramming #AdventOfCode
• Advent of Code 2020 solutions in Lean 4. ~ Reid Barton. #LeanProver #ITP #FuncionalProgramming

01-Dic-20

• Machine-checking the universal verifiability of Election Guard. ~ Thomas Haines, Rageev Goré, Jack Stodart. #ITP #Coq
• A note on right abelian distributive AG-groupoids. ~ Bashar Khan et als. #ATP #Prover9 #Mace4 #Math

Noviembre de 2020

30-Nov-20

• #ForMatUS: Libro “Ejercicios de lógica proposicional con Lean”. #DAO #LeanProver #Lógica #Matemática #ProgramaciónFuncional
• Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL
• Formalising ordinal partition relations using Isabelle/HOL. ~ Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Bind the gap (Pilot issue, November 2020). #Haskell #FunctionalProgramming

29-Nov-20

• Proving theorems with computers. ~ Kevin Buzzard. #ITP #LeanProver #Math
• A formally verified compiler for a simple language with numbers and sums. ~ Jordan Scales. #ITP #LeanProver
• nuha: Multidimensional arrays, linear algebra, numerical analysis. ~ Johannes Kropp. #Haskell #FunctionalProgramming #Math
• An introduction to proof via inquiry-based learning. ~ Dana C. Ernst. #eBook #Logic #Math
• Introduction to infinity categories. (Some notes on a short introductory video on some foundational aspects of infinity categories). ~ Zack Garza (@dzackgarza). #CategoryTheory

28-Nov-20

• Gradualizing the Calculus of Inductive Constructions. ~ Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter. #ITP #Coq
• A brief introduction to Smtlink. ~ Carl Kwan. #ITP #ACL2 #SMT #Z3
• Hazel tutor: Guiding novices through type-driven development strategies. ~ Hannah Potter, Cyrus Omar. #FunctionalProgramming
• Hazel: a live functional programming environment featuring typed holes. #FunctionalProgramming

27-Nov-20

• Formalising ordinal partition relations using Isabelle/HOL. ~ Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL #Math
• Program correctness. ~ Graham Hutton. #Haskell #FunctionalProgramming
• Logic: A study guide — First order logic. ~ Peter Smith. #Logic
• Mathematics for human flourishing. ~ Francis Su. #Book #Math

26-Nov-20

• A modular Isabelle framework for verifying saturation provers. ~ Sophie Tourret, Jasmin Blanchette. #ITP #IsabelleHOL
• Virtual record fields using lenses. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
• Existential Haskell. ~ Patrick Thomson. #Haskell #FunctionalProgramming
• Haskell in the Real World. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• The history of Standard ML. ~ David Macqueen, Robert Harper, John Reppy. #SML #FunctionalProgramming

25-Nov-20

• Correctness of a compiler for arithmetic expressions in Lean. ~ Xi Wang. #ITP #LeanProver

24-Nov-20

• A queue for effectful breadth-first traversals (Part 10 of a 10-part series on breadth-first traversals). ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
• hs-to-coq and Data.Sequence. ~ Li-yao Xia (@lysxia). #Haskell #Coq #FunctionalProgramming #ITP
• Intuitionistic logic in Haskell. ~ Isaac van Bakel. #Logic #Haskell
• Theorem proving in Haskell. ~ Isaac van Bakel. #Logic #Haskell #ITP
• Haskell and the Curry-Howard isomorphism (Part 1). ~ Ben Sherman. #Haskell #Logic
• The Curry-Howard correspondence in Haskell. ~ Tim Newsham. #Logic #Haskell
• Adventures in Classical-Land. ~ Dan Piponi.f#page=17 #Logic #Haskell
• Curry-Howard isomorphism down-to-earth. ~ Jannis Grimm. #Logic #Haskell
• A survey into the Curry-Howard isomorphism & type systems. ~ Phillip Mates. #Logic #Haskell
• Lisp books (Most of Lisp books in one place). ~ Vsevolod Dyomkin. #Lisp #Programming

22-Nov-20

• Two applications of logic programming to Coq. ~ M. Manighetti, D. Miller, A. Momigliano. #ITP #Coq #LogicProgramming
• Untangling mechanized proofs. ~ Clément Pit-Claude. #ITP #Coq
• Coming to terms with your choices: An existential take on dependent types. ~ Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza, Viktor Kunčak. #ITP #Coq #Scala
• Shallowly embedding type theories as presheaf models in Agda. ~ J. Ceulemans, D. Devriese. #ITP #Agda
• List of important publications in mathematics. #Books #Math
• Best math books (A comprehensive reading list). #Book #Math

21-Nov-20

• Release of the NASA PVS Library (NASALib) v7.1. #ITP #PVS
• BioShake: a Haskell EDSL forbioinformatics workflows. ~ Justin Bedo. #Haskell #FunctionalProgramming
• Common Lisp by Example (A compilation of notes from various sources). ~ Ashok Khanna. #CommonLisp
• Le problème des 8 reines. ~ Maxime Amblard (@maximeamblard). #Algorithms via @interstices_eu

20-Nov-20

• Certified optimisation of stream operations using heterogeneous staging. ~ J. Lowenthal, J. Yallop. #ITP #Agda
• Verifying replicated data types with typeclass refinements in Liquid Haskell. ~ Yiyun Liu et als. #Haskell #FuncBl%C3%B6ndal.pdf #MSc_Thesis #Haskell #FunctionalProgramming #LiquidHaskelltionalProgramming #LiquidHaskell
• Deriving Via (Type-directed instances). ~ Baldur Blöndal. #MSc_Thesis #Haskell #FunctionalProgramming
• Superpowered keyword args in Haskell. ~ Ben Kovach. #Haskell #FunctionalProgramming
• Logical English. ~ Robert Kowalski. #LogicProgramming #Prolog

19-Nov-20

• Shuffling things up: Applying Group Theory in Advent of Code. ~ Justin Le (@mstk).l#.X7Vk_XYPDuk.twitter #Haskell #FunctionalProgramming #Math
• The type theory of Lean. ~ Mario Carneiro. #ITP #LeanProver #Logic #Math #TypeTheory
• Arithmetic and casting in Lean. ~ Paul-Nicolas Madelaine. #MSc_Thesis #ITP #LeanProver #Math
• Meta-programming with the Lean proof assistant. ~ Pablo Le Hénaff. #ITP #LeanProver
• Formulations and solutions of IMO problemsin Isabelle/HOL. Filip Marić, Sana Stojanović-Ðurđević. #ITP #IsabelleHOL #Math #IMO
• Selected problems from the International Mathematical Olympiad 2019. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Bibliografía sobre Lean. #ITP #LeanProver
• The significance of the Curry-Howard isomorphism. ~ Richard Zach. #Logic #CompSci
• Awesome-Lisp-companies: A list of companies using Lisp in production. #CommonLisp
• #SEP: Combinatory logic. ~ Katalin Bimbó. #Logic

18-Nov-20

• List of events for World Logic Day 2021. #Logic
• A verified optimizer for quantum circuits. ~ Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. #ITP #Coq
• Formas prenex, de Skolem y teorema de Herbrand. ~ Fernando Sancho (@sanchocaparrini). #Lógica

17-Nov-20

• Logic and Artificial Intelligence. ~ Richmond Thomason. #Logic #AI
• Formally verified SAT-based AI planning. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL
• Philosophy of mathematics — a reading list. ~ Peter Smith (@PeterSmith). #Math

15-Nov-20

• Untangling mechanized proofs. ~ Clément Pit-Claudel. #ITP #Coq
• Video: Untangling mechanized proofs. ~ Clément Pit-Claudel. #ITP #Coq
• De-mystifying Emacs, lsp-haskell and haskell-language-server Setup. ~ Guru Devanla (@grdvnl). #Haskell #Emacs

14-Nov-20

• AI planning languages semantics (in Isabelle/HOL). ~ Mohammad Abdulaziz, Peter Lammich. #ITP #IsabelleHOL #AI
• Verified SAT-based AI planning. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL #AI
• A formalisation of biochemical process languages in Lean. ~ Jonathan Coates. #ITP #LeanProver
• Mechanizing hyperdual numbers in Isabelle/HOL. ~ Filip Smola. #ITP #IsabelleHOL #Math
• Extending equational monadic reasoning with monad transformers. ~ Reynald Affeldt, David Nowak. #ITP #Coq
• Mathlib naming conventions. ~ Jeremy Avigad. #ITP #LeanProver

13-Nov-20

• IMO 1964 Q1 in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Ranas, pájaros … y la hipótesis de Riemann. ~ Juan Arias de Reyna. #Matemáticas
• Exotic programming ideas: Part 1 (Module systems). ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming

12-Nov-20

• Pure destination-passing style in Linear Haskell. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• Métodos numéricos básicos con Octave. ~ Antonia M. Delgado, Juanjo Nieto, Aureliano M. Robles, Óscar Sánchez. #Octave #Matemáticas
• Algoritmos básicos de Cálculo Científico programados con Octave. ~ Óscar Sánchez. #Octave #Matemáticas

11-Nov-20

• Programming metamorphic algorithms: An experiment in type-driven algorithm design. ~ Hsiang-Shang Ko. #ITP #Agda #FunctionalProgramming
• Formas normales, cláusulas y algoritmo DPLL. ~ Fernando Sancho (@sanchocaparrini). #Lógica

10-Nov-20

• Inside the secret math society known simply as Nicolas Bourbaki. ~ Kevin Hartnett (@KSHartnett). #Math
• Verified optimizations for functional languages. ~ Zoe Paraskevopoulou. #ITP #Coq #PhD_Thesis
• Generation and use of hints and feedback in a Hilbert-style axiomatic proof tutor. ~ Josje Lodder, Bastiaan Heeren, Johan Jeuring, Wendy Neijenhuis. #Logic #Teaching
• Separate your views; reify your reasoning. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Pretty-print syntax trees with this one simple trick. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming

09-Nov-20

• Opinionated Common Lisp resources 2020. ~ Shubhamkar Ayare. #Programming #CommonLisp
• Writing for reasons. ~ Robin Schroer.

08-Nov-20

• Category theory: The math behind mathematics. ~ Cole Persch. #Math #CategoryTheory

07-Nov-20

• A trustful monad for axiomatic reasoning with probability and nondeterminism. ~ Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. #ITP #Coq
• Towards a certified reference monitor of the Android 10 permission system. ~ Guido De Luca, Carlos Luna. #ITP #Coq
• ιDOT: A DOT calculus with object initialization. ~ Ifaz Kabir, Yufeng Li, Ondřej Lhoták. #ITP #Coq
• A mechanically assisted examinationof vacuity and question beggingin Anselm’s ontological argument. ~ John Rushby. #ITP #PVS
• Implementation of affine arithmetic in Haskell. ~ Joosep Jääger. #BSc_Thesis #Haskell #FunctionalProgramming #Math

06-Nov-20

• Your orphan instances are probably fine. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming
• A story of an arrow and a comma. ~ Murat Kasimov. #Haskell #FunctionalProgramming
• Construir un buscador (en espacios de estados) desde cero. ~ Fernando Sancho (@sanchocaparrini). #Algoritmos #IA

05-Nov-20

• Inference in Agda (a tutorial on how Agda infers things). ~ Andreas Abel. #ITP #Agda
• Clojure en production. ~ Mathieu Corbin. #Clojure
• How to define things by recursion. ~ Alex Kavvos. #Logic #Math
• Les assistants de preuve et applications à l’apprentissage du raisonnement mathématique. ~ Julien Narboux. #Logic #Math #ITP

04-Nov-20

• A new chapter for Haskell: The Haskell Foundation. #Haskell #FunctionalProgramming
• The Proof Manifesto. #Logic
• Quantifiers and quantification. ~ Gabriel Uzquiano. #Logic
• Más rompecabezas matemáticos con números. ~ Raúl Ibáñez (@mtpibtor). #Matemáticas
• Advent of Haskell 2020 (Call for participation). #Haskell #FunctionalProgramming
• The nature of infinity — and beyond (An introduction to Georg Cantor and his transfinite paradise). ~ Jørgen Veisdal (@JorgenVeisdal). #Logic #Math

03-Nov-20

• Formally verified SAT-based AI planning. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL #AI
• An analysis of implementing PVS in SPARK Ada. ~ A. Benjamin Hocking, Jonathan C. Rowanhill, Ben L Di Vito. #ITP #PVS
• Formal verification of Ethereum smart contracts using Isabelle/HOL. ~ Maria Saraiva de Campos Mendes Ribeiro. #ITP #IsabelleHOL
• Whole Haskell is best Haskell. ~ Ashley Yakeley. #Haskell #FunctionalProgramming

02-Nov-20

• Learning to prove theorems by learning to generate theorems. ~ Mingzhe Wang, Jia Deng. #ATP #ITP #MachineLearning
• Haskell LSP (bonus: for Vim). ~ Monique Oliveira (@moniquelive). #Haskell #FunctionalProgramming

01-Nov-20

• TacTok: Semantics-aware proof synthesis. ~ Emily First, Yuriy Brun, Arjun Guha. #ITP #Coq
• Big Math and the one-brain barrier: The tetrapod model of mathematical knowledge. ~ Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe. #Math #CompSci
• Efficient mixing of arbitrary ballots with everlasting privacy: How to verifiably mix the PPATC scheme . ~ Kristian Gjøsteen, Thomas Haines, Morten Rotvold Solberg. #ITP #Coq
• Glossy Haskell game. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming #Game
• Composable filters using Witherable optics. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming

Octubre de 2020

31-Oct-20

• Cellular automaton in Haskell (II). WireWorld. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming
• Accidentally-quadratic HashMaps. ~ Jack Kelly. #Haskell #FunctionalProgramming
• Handling of uncaught exceptions in Haskell. ~ Ivan Gromakovsky. #Haskell #FunctionalProgramming
• Plucking In, Plucking Out. ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming
• Formally verified constraints solvers (A guided tour). ~ Catherine Dubois. #ITP #Coq #CSP
• Competitive programming in Python (128 algorithms to develop your coding skills). ~ Christoph Dürr, Jill-Jênn Vie.1#v=onepage&q&f=false #Programming #Python

30-Oct-20

• Efficient automatic differentiation made easy via category theory. ~ Conal Elliott. #Haskell #CategoryTheory
• Teaching interactive proofs to mathematicians. ~ M. Ayala-Rincón, T.A. de Lima. #ITP #PVS #Math
• Isabelle/HOL as a meta-language for teaching logic. ~ Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn. #ITP #IsabelleHOL #Logic
• Formalizing IMO problems and solutions in Isabelle/HOL. ~ Filip Marić, Sana Stojanović-Đurđević. #ITP #IsabelleHOL #Math
• Formalization of IMO solutions in Isabelle/HOL. ~ Filip Marić. #ITP #IsabelleHOL #Math
• Haskell: The good parts. ~ Marc Scholten. #Haskell #FunctionalProgramming
• Rompecabezas matemáticos con números. ~ Raúl Ibáñez (@mtpibtor). #Matemáticas
• Quicksort in Haskell. ~ Alexander Vershilov. #Haskell #FunctionalProgramming
• How I use org-mode. ~ Yann Esposito (@yogsototh). #Emacs #OrgMode
• Tableros semánticos en lógica de primer orden. ~ Fernando Sancho (@sanchocaparrini). #Lógica
• Why I prefer functional programming. ~ G. Gonzalez (@GabrielG439). #FunctionalProgramming

29-Oct-20

• A sound type system for physical quantities, units, and measurements in Isabelle/HOL. ~ Simon Foster, Burkhart Wolff. #ITP #IsabelleHOL
• Tautology checkers in Isabelle and Haskell. ~ Jørgen Villadsen. #ITP #IsabelleHOL #Haskell #Logic
• IMO 1981 Q3 in Lean. ~ Kevin Lacker. #ITP #LeanProver #Math #IMO

28-Oct-20

• Haskell: The bad parts, part 1. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming

27-Oct-20

• Formal verification of a certified policy language. ~ Amir Eaman, Amy Felty. #ITP #Coq
• Actris 2.0: Asynchronous session-type based reasoning in separation logic. ~ Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers. #ITP #Coq
• Development method of three kinds of typical tree structure algorithms and Isabelle-based machine assisted verification. ~ Changjing Wang et als. #ITP #IsabelleHOL

25-Oct-20

• An infinite universe of number systems. ~ Kelsey Houston-Edwards. #Math
• Tableros semánticos en lógica proposicional. ~ Fernando Sancho (@sanchocaparrini). #Lógica #Matemática

24-Oct-20

• Automated theorem proving, fast and slow. ~ Michael Rawson, Giles Reger. #ATP #MachineLearning
• SeLFiE: Modular semantic reasoning for induction in Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL
• The Map of Mathematics. #Math

22-Oct-20

• A formalization of “Correctness of a compiler for arithmetic expressions” (McCarthy and Painter 1967) using the Lean theorem prover. ~ Xi Wang. #ITP #LeanProver
• Why fintech companies use Haskell. ~ Roman Alterman. #Haskell #FunctionalProgramming
• The coin change problem in Haskell. ~ Aron. #Haskell #FunctionalProgramming
• The greatest mathematician that never lived. ~ Pratik Aghor. #Math

21-Oct-20

• Quien utiliza Haskell?? ~ Emanuel Goette (@emanuelpeg). #Haskell #ProgramaciónFuncional

20-Oct-20

• IMO 1998 Q2 in Lean. ~ Oliver Nash. #ITP #LeanProver #Math #IMO
• Una colección de falacias lógicas ilustradas con ejemplos. ~ @Alvy. #Lógica
• Common logical fallacies (A handy collection of the most common logical fallacies for you to bookmark). #Logic
• EvoLogic: Sistema tutor inteligente para ensino de Lógica. ~ Cristiano Galafassi, Fabiane F.P. Galafassi, Eliseo B. Reategui, Rosa M. Vicari. #Logic #AI
• Emacs user survey. #Emacs
• crdt.el: a real-time collaborative editing environment for Emacs using Conflict-free Replicated Data Types. #Emacs
• nntwitter: A Gnus backend for Twitter. #Emacs #Twitter
• Awesome Elisp: a list of resources linked to Emacs LISP (Elisp) development. #Emacs #Elisp

19-Oct-20

• Verified textbook algorithms (A biased survey). #ITP #IsabelleHOL
• Theorem proving for Catlab 2: Let’s try Z3 this time. Nope. ~ Philip Zucker (@SandMouth) #CategoryTheory #JuliaLang
• Implementing cellular automata with comonads and dependent types. #Haskell #FunctionalProgramming
• Fun with Lambda Calculus. ~ Stepan Parunashvili (@stopachka). #Clojure #FunctionalProgramming #LambdaCalculus

18-Oct-20

• IMO 2019 problem 4 in Lean. ~ Floris van Doorn. #ITP #LeanProver #Math #IMO
• Fun with combinators. ~ Donnacha Oisín Kidney (@oisdk). #Logic #CompSci #Combinators
• Sintaxis y semántica de la lógica de primer orden. ~ Fernando Sancho (@sanchocaparrini). #Lógica #Matemática

17-Oct-20

• A formal correctness proof of Boruvka’s minimum spanning tree algorithm. ~ Nicolas Robinson-O’Brien. #MSc_Thesis #ITP #IsabelleHOL #Math
• Formalizing graph trail properties. ~ Hanna Elif Lachnitt. #Thesis #ITP #IsabelleHOL #Math
• Model structure on the universe of all types in interval type theory. ~ Simon Boulier, Nicolas Tabareau. #ITP #Coq
• Symbolic Artificial Intelligence (Lecture 1: Introduction to description logics and ontologies). ~ Natalia Díaz Rodríguez. #AI #Logic
• Logics and symbolic AI: Knowledge representation and reasoning. ~ Isabelle Bloch, Natalia Dı́az Rodrı́guez. #AI #Logic
• Course: Logics and symbolic AI. ~ Isabelle Bloch, Natalia Dı́az Rodrı́guez. #AI #Logic
• What is an algorithm? How computers know what to do with data. ~ Jory Denny. #Algorithms
• Drawing Git Graphs with Graphviz and Org-Mode. ~ Correl Roush (@correlr). #Emacs #OrgMode
• Things to do to an algorithm. ~ Bertrand Meyer. #Algorithms
• The pros and cons of online lab classes for Computer Science - 2020 pandemic edition. ~ Philip Guo. #CompSci
• Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda. ~ Sebastián Urciuoli, Álvaro Tasistro Nora Szasz. #ITP #Agda
• Resolución de los 99 ejercicios de Prolog. #Prolog #ProgramaciónLógica

16-Oct-20

• Formalisation and meta-theory of type theory. ~ Théo Winterhalter. #ITP #Coq #TypeTheory
• Refinement types: A tutorial. ~ Ranjit Jhala, Niki Vazou. #Haskell #FunctionalProgramming
• Production Haskell (Succeeding in industry with Haskell). ~ Matt Parsons (@mattoflambda). #Haskell #FunctionalProgramming
• Bottlenecked on Haskell’s text library. ~ Falco Peijnenburg. #Haskell #FunctionalProgramming
• Sintaxis y semántica de la lógica proposicional. ~ Fernando Sancho (@sanchocaparrini). #Lógica #Matemática

15-Oct-20

• Reflective programs in tree calculus. ~ Barry Jay (@Jay59009444). #ITP #Coq #Logic
• Silly job interview questions in Haskell. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
• The Hitchhiker’s Guide to Logical Verification (2020 Standard Edition (October 12, 2020)). ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl. #eBook #ITP #LeanProver

14-Oct-20

• The unreasonable effectiveness of the Julia programming language. ~ Lee Phillips. #JuliaLang #Programming

13-Oct-20

• Towards tactic metaprogramming in Haskell. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Normal forms. ~ Travis Whitaker. #Haskell #FunctionalProgramming
• What are algebraic data types? ~ @dicabrejas. #Haskell #FunctionalProgramming
• Emacs might not be doomed after all. ~ Oivvio Polite. #Emacs

12-Oct-20

• Inductive logic programming at 30: a new introduction. ~ Andrew Cropper, Sebastijan Dumančić. #ILP #MachineLearning #LogicProgramming
• Delivering with Haskell. ~ Sam Halliday (@fommil). #Haskell #FunctionalProgramming

11-Oct-20

• Dyadic deontic logic in HOL: Faithful embedding and meta-theoretical experiments. ~ Christoph Benzmüller, Ali Farjami, Xavier Parent. #ITP #IsabelleHOL #Logic
• Public announcement logic in HOL. ~ Sebastian Reiche, Christoph Benzmüller. #ITP #IsabelleHOL
• An antiquotation for locale graphs. ~ Clemens Ballarin. #ITP #IsabelleHOL
• Tutorial: Verify Haskell programs with hs-to-coq. ~ Li-yao Xia. #ITP #Coq #Haskell #FunctionalProgramming
• Embracing a mechanized formalization. ~ Li-yao Xia. #ITP #Coq #Haskell #FunctionalProgramming
• Separation logic-based verification atop a binary-compatible filesystem model. ~ Mihir Mehta, William Cook. #ITP #ACL2
• The anarchist abstractionist: Who was Alexander Grothendieck? ~ Jørgen Veisdal (@JorgenVeisdal). #Math

10-Oct-20

• A novice-friendly induction tactic for Lean (Draft). ~ Jannis Limperg. #ITP #LeanProver
• Proving quantum programs correct. ~ Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks. #ITP #Coq
• Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Logic #Math
• On the Nielsen-Schreier theorem in homotopy type theory. ~ Andrew W Swan. #ITP #Agda #Math #HoTT
• Digging for fold: Synthesis-aided API discovery for Haskell. ~ Michael B. James et als. #Haskell #FunctionalProgramming
• Mathematical fallacy proofs. ~ Xing Yuan. #Logic #Math

09-Oct-20

• Building problem solvers. ~ Kenneth D. Forbus, Johan de Kleer. #eBook #AI #CommonLisp
• Computer scientists break traveling salesperson record. ~ Erica Klarreich (@EricaKlarreich). #Algorithms #CompSci

08-Oct-20

• Reasoning about monotonicity in separation logic. ~ Amin Timany, Lars Birkedal. #ITP #Coq
• The Arcane Algorithm Archive (a collaborative effort to create a guide for all important algorithms in all languages). #Algorithms #Programming

07-Oct-20

• Formalizing the ring of Witt vectors. ~ Johan Commelin, Robert Y. Lewis. #ITP #LeanProver #Math
• On characterizing Nat in Agda. ~ Callan McGill. #ITP #Agda #Logic #Math
• Course: Higher-Dimensional Type Theory. ~ Favonia. #TypeTheory #ITP #Agda
• Higher-dimensional type theory (Lecture recordings). ~ Favonia. #TypeTheory
• Scientists solve 90-year-old geometry problem. ~ Byron Spice. #Math #ATP #SAT_solver
• Course “Functional Programming”. ~ Bob Atkey. #Haskell #FunctionalProgramming
• Collect in Rust, traverse in Haskell and Scala. Michael Snoyman (@snoyberg). #Haskell #Rust #Scala #FunctionalProgramming via @FPComplete
• Knowledge is good. ~ R.J. Lipton. #Logic #Math

06-Oct-20

• Smart induction for Isabelle/HOL (Tool paper). ~ Yutaka Nagashima. #ITP #IsabelleHOL
• Chain of events: Modular process models for the law. ~ Søren Debois et als. #ITP #IsabelleHOL
• Formalisation: Chain of events: Modular process models for the law. ~ Søren Debois #ITP #IsabelleHOL
• Combinatorial geometries in Lean. ~ Adam Topaz. #ITP #LeanProver #Math
• Proof repair across type equivalences. ~ Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman. #ITP #Coq
• All about strictness. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming via @FPComplete
• Starting Haskellings! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
• Blogging with Emacs & Org-mode. ~ Musa Al-hassy (@musa314). #Emacs #OrgMode
• Calculational Mathematics and CalcCheck. ~ Musa Al-hassy (@musa314). #Math #CalcCheck

05-Oct-20

• Mechanized logical relations for termination-insensitive noninterference. ~ S.O. Gregersen, J. Bay, A. Timany, L. Birkedal. #ITP #Coq
• Combinatorics in Lean. ~ Bhavik Mehta. #ITP #LeanProver #Math
• Optics and Kleisli arrows. ~ Alejandro Serrano. #Haskell #FunctionalProgramming

04-Oct-20

• Tool supported specification and verification of highly available applications. ~ Peter Zeller. #ITP #IsabelleHOL
• Generating mutually inductive theorems from concise descriptions. ~ Sol Swords. #ITP #ACL2
• Ethereum’s recursive length prefix in ACL2. ~ Alessandro Coglio. #ITP #ACL2 #Ethereum
• Isomorphic data type transformations. ~ Alessandro Coglio, Stephen Westfold. #ITP #ACL2
• Set theory from Cantor to Cohen. ~ Akihiro Kanamori. #Logic #Math vía @logicians

03-Oct-20

• Fixed points theorems for non-transitive relations. ~ Jérémy Dubut, Akihisa Yamada. #ITP #IsabelleHOL #Math
• Computing and proving well-founded orderings through finite abstractions. ~ Rob Sumners. #ITP #ACL2
• Quadratic extensions in ACL2. ~ Ruben Gamboa, John Cowles, Woodrow Gamboa. #ITP #ACL2 #Math
• Essential logic for computer science. ~ Rex Page, Ruben Gamboa.1#v=onepage&q&f=true #eBook #Logic #ITP #ACL2
• Grzegorczyk hierarchy. #Logic #Math #CompSci
• Matemáticas vs Coronavirus: recursos matemáticos para la docencia online. #Matemáticas
• Cambiando el blog a org-static-blog. #Emacs

02-Oct-20

• Learning-assisted theorem proving with millions of lemmas. ~ Cezary Kaliszyk, Josef Urban. #ITP #ATP #MachineLearning
• Build scripts with perfect dependencies. ~ Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt. #Haskell #FunctionalProgramming

01-Oct-20

• Building the mathematical library of the future. ~ Kevin Hartnett (@KSHartnett). #ITP #LeanProver #Math

Septiembre de 2020

30-Sep-20

• Iteration in ACL2. ~ Matt Kaufmann, J Strother Moore. #ITP #ACL2 #CommonLisp
• Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2. ~ David M. Russinoff. #ITP #ACL2
• Coherence for monoidal groupoids in HoTT. ~ Stefano Piceghello.f#page=199 #ITP #Coq #HoTT
• Is impredicativity implicitly implicit? Stefan Monnier, Nathaniel Bos.f#page=219 #ITP #Coq
• Higher inductive type eliminators without paths. ~ Nils Anders Danielsson.f#page=239 #ITP #Agda #HoTT
• ¿Qué es una red neuronal? | Aprendizaje profundo. Capítulo 1. #AI #AprendizajeAutomático
• Descenso de gradiente. Cómo aprenden las redes neuronales | Aprendizaje profundo. Capítulo 2. #AI #AprendizajeAutomático

29-Sep-20

• The empirical metamathematics of Euclid and beyond. ~ Stephen Wolfram. #Logic #Math #ITP #LeanProver #Metamath
• Making Isabelle content accessible in knowledge representation formats. ~ Michael Kohlhase, Florian Rabe, Makarius Wenzel.f#page=11 #ITP #IsabelleHOL #MKM
• Type theory unchained: Extending Agda with user-defined rewrite rules. ~ Jesper Cockx.f#page=35 #Agda #ITP #FunctionalProgramming
• The Tao of Types. ~ Thorsten Altenkirch. #TypeTheory
• Big step normalisation for type theory. ~ Thorsten Altenkirch, Colin Geniet.f#page=99 #ITP #Agda #TypeTheory
• For finitary induction-induction, induction is enough. ~ Ambrus Kaposi, András Kovács, Ambroise Lafont. f#page=137 #ITP #Agda
• Eta-equivalence in core dependent Haskell. ~ Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, Stephanie Weirich.f#page=167 #Haskell #FunctionalProgramming #ITP #Coq

28-Sep-20

• Integration of formal proof into unified assurance cases with Isabelle/SACM. ~ Simon Foster, Yakoub Nemouchi, Mario Gleirscher, Ran Wei, Tim Kelly. #ITP #Isabelle/SACM
• Proving excluded middle in Lean (FP lunch 25/9/20). ~ Thorsten Altenkirch. #ITP #LeanProver #Logic
• Primitive element theorem in Lean. #ITP #LeanProver #Math
• Universal enveloping algebra in Lean. #ITP #LeanProver #Math
• Jensen’s inequality for integrals in Lean. #ITP #LeanProver #Math
• Haskell via Sokoban. ~ Joachim Breitner (@nomeata). #Haskell #FunctionalProgramming #CodeWorld
• ¿Qué es Idris y por qué es un lenguaje de programación tan interesante? ~ Adrián Arroyo (@aarroyoca). #Idris #ProgramaciónFuncional

26-Sep-20

• Machine learning and the formalisation of mathematics: Research challenges. ~ Lawrence C Paulson. #ITP #ML
• Developing a concept-oriented search engine for Isabelle based on natural language: Technical challenges. ~ Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL #MKM #Math
• Automation of proof by induction in Isabelle/HOL using Domain-Specific Languages (LiFtEr: Logical Feature Extractor, SeLFiE: Semantic Logical Feature Extractor). ~ Yutaka Nagashima. #ITP #IsabelleHOL #ML
• Reinforcement learning for interactive theorem proving in HOL4. ~ Minchao Wu, Michael Norrish, Christian Walder, Amir Dezfouli. #ITP #HOL4 #ML
• Relieving user effort for the auto tactic in Coq with machine learning. ~ Lasse Blaauwbroek. #ITP #Coq #MachineLearning
• The IMO Grand Challenge. ~ Daniel Selsam. #AI #ITP #LeanProver #Math
• Classification of finite semigroups and categories using computational methods. ~ Najwa Ghannoum et als. #APT #MACE4 #Math
• Formal/symbolic/numerical computational methods. ~ Michael R. Douglas. #AI #ITP #ML
• Learning cubing heuristics for SAT from DRAT proofs. ~ Jesse Michael Han. #ATP #SAT #ML
• Learning theorem proving through self-play. ~ Stanisław Purgał. #ATP #MachineLearning
• The open logic text (Revision: 2020-09-24). #eBook #Logic

25-Sep-20

• CertRL: Formalizing convergence proofs for value and policy iteration in Coq. ~ Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry Trager, Nathan Fulton. #ITP #Coq
• Formalized generalization bounds for perceptron-like algorithms. ~ Robin J. Kelby. #MSc_Thesis #ITP #Coq #Haskell
• Reanimate: Build declarative animations with SVG and Haskell. #Haskell #FunctionalProgramming
• The chessboard puzzle and the mathematics of invariants. ~ Maths and Musings in Cantor’s Paradise. #Math #CompSci
• Un problema que llevaba 20 años abierto (I): Grupos de trenzas y grupos de Artin. ~ María Cumplido. #Matemáticas
• In the computer. ~ Chris Martin (@chris__martin). #Programming

24-Sep-20

• Course retrospective: SMT solving and solver-aided systems. ~ Lindsey Kuper (@lindsey). #SMT #ATP
• The Incredible Proof Machine. #Logic
• Euclidea: Geometric constructions game with straightedge and compass. #Math #Game

23-Sep-20

• Higher-order nonemptiness step by step. ~ Paweł Parys. #ITP #Coq
• A mechanically assisted examination of vacuity and question begging in Anselm’s ontological argument. ~ John Rushby. #ITP #PVS
• Verifying correctness of contract decompositions. ~ Gustav Hedengran. #ITP #HOL4
• A formally verified protocol for log replication with byzantine fault tolerance. ~ Joel Wanner, Laurent Chuat, Adrian Perrig. #ITP #IsabelleHOL
• Similar triangles and orientation in plane elementary geometry for Coq-based proofs. ~ Tuan Minh Pham. #ITP #Coq #Math
• Strategic deriving. ~ Veronika Romashkina (@vrom911), Dmitrii Kovanikov ((@ChShersh)). #Haskell #FunctionalProgramming

22-Sep-20

• Foundations: a draft of a chapter on mathematical logic and foundations for an upcoming handbook of computational proof assistants. ~ Jeremy Avigad. #Logic #Math #ITP #CompSci
• At the Math Olympiad, computers prepare to go for the gold. ~ Kevin Hartnett (@KSHartnett). #Math #AI #ITP
• Faster smarter induction in Isabelle/HOL with SeLFiE. ~ Yutaka Nagashima. #ITP #IsabelleHOL
• Haskell’s children. ~ Owen Lynch (@u_map_prop). #Haskell #FunctionalProgramming #Rust #Idris #JuliaLang
• Logic programming and machine ethics. ~ Abeer Dyoub, Stefania Costantini, Francesca A. Lisi. #LogicProgramming
• Deriving theorems in implicational linear logic, declaratively. ~ Paul Tarau, Valeria de Paiva. #Prolog #LogicProgramming #Logic

20-Sep-20

• Software Foundations in Lean. ~ Andrew Ashworth. #ITP #LeanProver
• Thoughts on the Pythagorean theorem. ~ Kevin Buzzard (@XenaProject). #Math
• List of unsolved problems in mathematics. #Math
• Finger trees explained anew, and slightly simplified (functional pearl) Haskell. ~ Koen Claessen. #Haskell #FunctionalProgramming

19-Sep-20

• A formally verified abstract account of Gödel’s incompleteness theorems. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• An abstract formalization of Gödel’s incompleteness theorems. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• From abstract to concrete Gödel’s incompleteness theorems (Part I). ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• From abstract to concrete Gödel’s incompleteness theorems (Part II). ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• Syntax-independent logic infrastructure. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• Robinson arithmetic. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• A formal model of extended finite state machines. ~ Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick. #ITP #IsabelleHOL
• Inference of extended finite state machines. ~ Michael Foster, Achim D. Brucker, Ramsay G. Taylor, John Derrick. #ITP #IsabelleHOL
• Lazy sort: Counting comparisons. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming

18-Sep-20

• Lean: The Calculator on Steroids. ~ James Arthur. #ITP #LeanProver #Math
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types. ~ Anders Mörtberg. #ITP #Agda
• Art and automated reasoning tools in geometry. ~ F. Botana, Tomás Recio. #Math #CompSci #ATP #GeoGebra
• The SAT game. ~ Olivier Roussel. #Logic #Game #SAT
• Which monads Haskell developers use: An exploratory study. ~ Ismael Figueroa, Paul Leger, Hiroaki Fukuda. #Haskell #FunctionalProgramming via @FunctorFact
• Fun with Haskell. ~ Pritesh Shrivastava (@pritesh_shri). #Haskell #FunctionalProgramming
• Aggressive refactoring. ~ Simon Shine. #Haskell #FunctionalProgramming
• Tensor chain contraction with refolds. ~ David Anekstein. #Haskell #FunctionalProgramming
• An application of knowledge engineering to mathematics curricula organization and formal verification. ~ Eugenio Roanes-Lozano, Angélica Martínez-Zarzuelo, María José Fernández-Díaz. #Math #CompSci #FormalVerification #RBES
• Problemas del mes (Septiembre 2020). #Matemáticas

17-Sep-20

• Coinductive natural semantics for compiler verification in Coq. ~ Angel Zúñiga, Gemma Bel-Enguix. #ITP #Coq
• Dynamic IFC theorems for free! ~ Maximilian Algehed, Jean-Philippe Bernardy, Catalin Hritcu. #ITP #Agda
• Haskell functors in detail: An in-depth tutorial/reference about functors. #Haskell #FunctionalProgramming

16-Sep-20

• Formalising Σ-protocols and commitment schemes using CryptHOL. ~ D. Butler, A. Lochbihler, D. Aspinall, A. Gascón. #ITP #IsabelleHOL
• Towards formal verification of program obfuscation. ~ Weiyun Lu, Bahman Sistany, Amy Felty, Philip Scott. #ITP #Coq
• The duality of subtyping. ~ Bruno C. d. S. Oliveira, Cuui Shaobo, Baber Rehman. #ITP #Coq
• The computer scientist who can’t stop telling stories. ~ Susan D’Agostino (@susan_dagostino). #CompSci

15-Sep-20

• Proving the consistency of Logic in Lean. ~ Luiz Carlos R. Viana. #ITP #LeanProver #Logic
• Authenticated data structures as functors in Isabelle/HOL. ~ Andreas Lochbihler, Ognjen Marić.f#page=52 #ITP #IsabelleHOL
• Inter-blockchain protocols with the Isabelle infrastructure framework. ~ Florian Kammüller, Uwe Nestmann.f#page=105 #ITP #IsabelleHOL
• Verifying, testing and running smart contracts in ConCert. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters.f#page=118 #ITP #Coq
• Albert, an intermediate smart-contract language for the Tezos blockchain. ~ Bruno Bernardo, Raphaël Cauderlier, Arvid Jakobsson, Basile Pesin, Julien Tesson.f#page=128 #ITP #Coq

14-Sep-20

• A general definition of dependent type theories. ~ Andrej Bauer, Philipp G. Haselwarter, Peter LeFanu Lumsdaine. #TypeTheory #Logic #Math #ITP #Coq
• What we talk about when we talk about monads. ~ Tomas Petriceka. #Haskell #FunctionalProgramming #CategoryTheory via @impurepics

13-Sep-20

• Some proofs about sequences and series in Coq. #ITP #Coq #Math0
• Liquid Haskell. ~ Andres Löh. #Haskell #FunctionalProgramming

12-Sep-20

• Intuitionism in Lean. ~ Rick Koenders. #BsC_Thesis #ITP #LeanProver #Logic
• Generative language modeling for automated theorem proving. ~ Stanislas Polu, Ilya Sutskever. #ATP #MachineLearning #DeepLearning
• Verifiable C (Software foundations, Volume 5). ~ Andrew W. Appel, Qinxiang Cao, #eBook #ITP #Coq
• Theorems for free. ~ Lars Hupel. #Haskell #FunctionalProgramming
• Haskell: Understanding GHC’s error messages. ~ Obro Und. #Haskell #FunctionalProgramming

11-Sep-20

• Contravariant functors are weird. ~ Sanjiv Sahayam (@ssanj). #Haskell #FunctionalProgramming
• Four reasons that PureScript is your best choice to build a server in 2020. ~ Mike Solomon. #PureScript #FunctionalProgramming
• Let’s write a Haskell Language Server plugin. ~ Pepe Iborra. #Haskell #FunctionalProgramming
• Monoids (and semigroups). ~ Sam A. Horvath-Hunt. #Haskell #TypeScript #FunctionalProgramming

10-Sep-20

• Certified semantics for disequality. ~ Dmitry Rozplokhas, Dmitry Boulytchev. #ITP #Coq
• miniKanren-coq: A certified semantics for relational programming workout. ~ Dmitry Boulytchev. #ITP #Coq
• Machine learning guidance for connection tableaux. ~ Michael Färber, Cezary Kaliszyk, Josef Urban. #Logic #ATP #MachineLearning
• Ergonomic Haskell 1: Records. #Haskell #FunctionalProgramming

09-Sep-20

• Holbert: A graphical interactive proof assistant designed for education. ~ Liam O’Connor (@kamatsu8). #ITP #Haskell #Logic

08-Sep-20

• Mechanising set theory in Coq (The generalised continuum hypothesis and the axiom of choice). ~ Felix Rech. #MsC_Thesis #ITP #Coq #Logic #Math
• Program logics for certified compilers. ~ Andrew W. Appel et als. #eBook #ITP #Coq
• Language-integrated verification. ~ Ranjit Jhala. #Haskell #FunctionalProgramming
• Check your (students’) proofs-with holes. ~ Dennis Renz, Sibylle Schwarz, Johannes Waldmann. #Haskell #FunctionalProgramming

06-Sep-20

• Practical idiomatic considerations for checkable meta-logic in experimental functional programming. ~ Baltasar Trancón y Widemann, Markus Lepper. #Haskell #FunctionalProgramming
• Actually, Maybe is great. ~ Dave Della Costa. #Haskell #FunctionalProgramming
• Implementing a GHC plugin for Liquid Haskell. ~ Alfredo Di Napoli. #Haskell #FunctionalProgramming #LiquidHaskell
• Un-obscuring a few GHC type error messages. ~ Ziyang Liu. #Haskell #FunctionalProgramming
• Fixed points of indexed functors. ~ Oleg Grenrus. #Haskell #FunctionalProgramming
• La calculadora de Emacs. #Emacs

05-Sep-20

• Church’s thesis and related axioms in Coq’s type theory. ~ Yannick Forster. #ITP #Coq #Logic #Math
• Addition chains. ~ Pierre Castéran. #ITP #Coq #Math
• lean-mode (emacs mode for Lean Theorem Prover). ~ Soonho Kong, Leonardo de Moura. #ITP #LeanProver #Emacs
• Relational reasoning for effects and handlers. ~ Craig McLaughlin. #PhDThesis #Haskell #FunctionalProgramming #ITP #Agda
• Herramientas de razonamiento automático en GeoGebra: qué son y para qué sirven. ~ Steven Van Vaerenbergh, Tomás Recio, Pilar Vélez. #RA #GeoGebra #Matemáticas
• Dependent types to code are what static types to data (Modeling state machines: Part 2). ~ Evgeny Poberezkin (@epoberezkin). #Haskell #FunctionalProgramming
• Solving the “Beautiful bridges” problem, algebraically. ~ Ziyang Liu. #Math #Haskell #FunctionalProgramming
• Practical dependent type checking using twin types. ~ Víctor López Juan, Nils Anders Danielsson. #ITP #Agda #FunctionalProgramming
• A framework for generating diverse Haskell-IO exercise tasks. ~ Oliver Westphal. #Haskell #FunctionalProgramming

03-Sep-20

• Formalization of cryptographic algorithms in the Lean Theorem Prover. ~ Guilherme Gomes Felix da Silva, Edward Hermann Haeusler, Bruno Lopes.f#page=127 #ITP #LeanProver #Math
• Some classical results in inductive inference of recursive functions in Isabelle/HOL. ~ Frank J. Balbach. #ITP #IsabelleHOL
• Putting the ‘K’ into Bird’s derivation of Knuth-Morris-Pratt string matching in Isabelle/HOL. ~ Peter Gammie. #ITP #IsabelleHOL

02-Sep-20

• Church’s thesis and related axiomsin Coq’s type theory. ~ Yannick Forster. #ITP #Coq #Logic #TypeTheory
• Can computers do mathematical research? ~ David H Bailey. #Math #CompSci
• The inevitable questions about automated theorem proving. ~ Michael Harris. #ATP #ITP #AI #Math
• Can machine learning algorithms replace exams? ~ Orit Hazzan, Koby Mike. #AI #DataScience

01-Sep-20

• Infinite fun with infinite worlds. ~ Florian Meyer. #Logic #Math
• Practical algebraic calculus checker in Isabelle/HOL. ~ Mathias Fleury, Daniela Kaufmann. #ITP #IsabelleHOL #Logic #Math
• A list of Haskell articles on good design, good testing. ~ William Yao et als. #Haskell #FunctionalProgramming
• Gödel’s incompleteness theorems from a paraconsistent perspective. ~ Walter Carnielli, David Fuenmayor. #ITP #IsabelleHOL #Logic #Math
• VerifyThis 2019: A program verification competition (Extended report). ~ Claire Dross, Carlo A. Furia, Marieke Huisman, Rosemary Monahan, Peter Müller. #FormalVerification
• A gentle introduction to dependent types. ~ A. Samartino. #FunctionalProgramming

Agosto de 2020

31-Ago-20

• Type-driven neural programming by example. ~ Kiara Grouwstra. #PhD_Thesis #Haskell #FunctionalProgramming #NeuralNetwork
• Typed neuro-symbolic program synthesis for the typed lambda calculus. ~ Kiara Grouwstra. #Haskell #FunctionalProgramming #NeuralNetwork

29-Ago-20

• Ackermann’s function in iterative form: A subtle termination proof with Isabelle/HOL. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Formalising cryptography using CryptHOL. ~ David Thomas Butler. #PhD_Thesis #ITP #IsabelleHOL
• Describing console I/O behavior for testing student submissions in Haskell. ~ Oliver Westphal, Janis Voigtländer. #Haskell #FunctionalProgramming
• Haskell from 0 to IO (Maybe Hero). #Haskell #FunctionalProgramming
• Knowledge representation and reasoning with Answer Set Programming. ~ Natalie Kuster (@natalie_kuster). #ASP #LogicProgramming

28-Ago-20

• How close are computers to automating mathematical reasoning? ~ Stephen Ornes (@StephenOrnes). #ATP #ITP #Math #CompSci
• Computer scientists attempt to corner the Collatz conjecture. ~ Kevin Hartnett (@KSHartnett). #ATP #SAT_Solver #Math #CompSci
• Finding the hardest formulas for resolution. ~ Tomáš Peitl, Stefan Szeider. #ATP #SAT_Solver #Logic
• What is Haskell, and who should use it? ~ Jason McClellan (@jk_mcclellan). #Haskell #FunctionalProgramming

27-Ago-20

• Towards a verified model of the Algorand consensus protocol in Coq. ~ Musab A. Alturki et als. #ITP #Coq

26-Ago-20

• Relational disjoint-set forests in Isabelle/HOL. ~ Walter Guttmann. #ITP #IsabelleHOL
• Verifiable C. ~ Andrew W. Appel, Qinxiang Cao. #eBook #ITP #Coq
• Do more with your types: GADTs and LiquidHaskell. ~ Alejandro Serrano, Haskeller (@trupill). #Haskell #FunctionalProgramming #LiquidHaskell
• OCaml scientific computing (Functional programming meets Data Science). ~ Liang Wang, Jianxin Zhao. #eBook #OCaml #FunctionalProgramming #DataScience

25-Ago-20

• Automating proofs of lattice inequalities in Coq with reinforcement learning and duality. ~ Anshula Gandhi, Favio E. Miranda-Perea, Lourdes del Carmen Gonz. #ITP #Coq #MachineLearning
• Getting started with proving math theorems through reinforcement learning (An experiment at MIT’s Brains, Minds, and Machines Lab). ~ Anshula Gandhi. #ITP #Coq #MachineLearning
• Guaranteeing proof termination (Dealing with infinite proof search in reinforcement-learning automated proofs). ~ Anshula Gandhi. #ITP #Coq #MachineLearning

24-Ago-20

• LiquidHaskell is a GHC plugin. ~ Ranjit Jhala (@RanjitJhala). #Haskell #FunctionalProgramming
• Functional programming is awesome!! ~ Amandeep Singh (@theamndeepsingh). #FunctionalProgramming #Haskell

23-Ago-20

• An introduction to formal logic. ~ Peter Smith. #eBook #Logic
• An introduction to Gödel’s theorems. ~ Peter Smith. #eBook #Logic
• Some more list algorithms. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming

22-Ago-20

• Introduction to Homotopy Type Theory. ~ Egbert Rijke. #HoTT #ITP #Agda #Coq
• Adventures in mathematical reasoning. ~ Toby Walsh. #ATP #Math
• Understanding memory fragmentation. ~ David Eichmann. #Haskell #FunctionalProgramming
• Probabilistic programming with continuations. ~ Jules Hedges (@_julesh_). #Haskell #FunctionalProgramming
• Five stages of accepting constructive mathematics. ~ Andrej Bauer. #Logic #Math
• Logic symbols (A comprehensive collection of the most notable symbols in formal/mathematical logic). ~ Math Vault. #Logic #Math

21-Ago-20

• Formal Mathematics and the Lean theorem prover. ~ Jeremy Avigad. #Logic #Math #ITP #LeanProver
• [[https://youtu.be/uPCxm1_R_4I][Formal Mathematics and the Lean theorem prover [Video]]]. ~ Jeremy Avigad. #Logic #Math #ITP #LeanProver
• Effect handlers in Haskell, evidently. ~ Ningning Xie, Daan Leijen. #Haskell #FunctionalProgramming
• Scripted signal functions. ~ David A. Stuart. #Haskell #FunctionalProgramming
• Types as axioms, or: playing god with static types. ~ Alexis King (@lexi_lambda). #Haskell #FunctionalProgramming
• Inductive logic programming at 30: a new introduction. ~ Andrew Cropper, Sebastijan Dumančić. #ILP #MachineLearning #LogicProgramming

20-Ago-20

• Computer search settles 90-year-old Math problem. ~ Kevin Hartnett. #Math #CompSci #ATP #SAT_Solvers
• Whirlwind tour of Cabal for beginners. #Haskell #FunctionalProgramming
• How stylish-haskell works. ~ Felix Mulder. #Haskell #FunctionalProgramming
• A graded Monad for deadlock-free concurrency (Functional Pearl). ~ Andrej Ivašković, Alan Mycroft. #Haskell #FunctionalProgramming
• Finger trees explained anew, and slightly simplified (Functional Pearl). ~ Koen Claessen. #Haskell #FunctionalProgramming
• Enhancing functor structures step-by-step (Part 1). ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
• Enhancing functor structures step-by-step (Part 2). ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
• Set theory symbols. ~ Math Vault. #Math

19-Ago-20

• Ordinal partitions in Isabelle/HOL. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
• Post-quantum verification of Fujisaki-Okamoto. ~ Dominique Unruh. #ITP #IsabelleHOL
• Logipedia: towards a Wikipedia of formal proofs. ~ Gilles Dowek. #ITP #Math
• Topology (A categorical approach). ~ Tai-Danae Bradley, Tyler Bryson, and John Terilla. #Ebook #Math #CategoryTheory

18-Ago-20

• Hybrid logic in the Isabelle proof assistant: Benefits, challenges and the road ahead. ~ Asta Halkjær From.f#page=27 #ITP #IsabelleHOL #Logic
• A formalisation of the SPARC TSO memory model for multi-core machine code. ~ Zhe Hou, David Sanan, Alwen Tiu, Yang Liu, Jin Song Dong. #ITP #IsabelleHOL
• Generalised Veltman semantics in Agda. ~ J.M. Rovira, L. Mikec, J.J. Joosten.f#page=90 #ITP #Agda #Logic
• Penrose: from mathematical notation to beautiful diagrams. ~ K. Ye, W. Ni, M. Krieger, D. Ma’ayan, J. Wise, J. Aldrich. #DSL #Haskell #FunctionalProgramming #Math
• Automatic verification of annotated sequential imperative programs. ~ Alinda Harmanny. #Haskell #FunctionalProgramming #Logic
• Un poco más sobre magit. #Emacs #Git

17-Ago-20

• A proof of the Sprague-Grundy theorem and other results related to impartial games in Lean. ~ Fox Thomson. #ITP #LeanProver
• HOList: An environment for machine learning of higher-order theorem proving. ~ Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox. #ITP #HOL_Light #MachineLearning
• Haskell mini-patterns handbook. ~ Dmitrii Kovanikov (@ChShersh), Veronika Romashkina (@vrom911). #Haskell #FunctionalProgramming

16-Ago-20

• Proof-carrying plans: a resource logic for AI planning. ~ Alasdair Hill, Ekaterina Komendantskaya, Ronald P. A. Petrick. #ITP #Agda #AI
• Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. ~ Ralph Bottesch, Max W. Haslbeck, René Thiemann. #ITP #IsabelleHOL
• The Mathlib formalisation project needs your help (A serious effort to formalise modern mathematics). ~ Oliver Nash. #ITP #LeanProver #Math

15-Ago-20

• A verified tableau prover for modal logic K- ~ Minchao Wu. #ITP #LeanProver #Logic
• Cross wolf, goat and cabbage across the river with effects. ~ Murat Kasimov #Haskell #FunctionalProgramming
• Generic Haskell. ~ Jonathan Dowland (@jmtd). #Haskell #FunctionalProgramming
• Towards provably correct probabilistic flight systems. ~ Elkin Cruz-Camacho, Saswata Paul, Fotis Kopsaftopoulos, Carlos A. Varela. #ITP #Agda
• Amicable numbers in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math

14-Ago-20

• Using Lean with undergraduate mathematicians. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• mathlib: Lean’s mathematical library. ~ Johannes Hölzl. #ITP #LeanProver #Math
• Embedding specialized proof languages into Lean (A case study). ~ Simon Hudon. #ITP #LeanProver #Logic
• A formal proof of Hensel’s lemma over the p-adic integers. ~ Robert Y. Lewis. #ITP #LeanProver #Math
• How to design co-programs. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• Quantitative typing with non-idempotent intersection types. ~ Bob Atkey (@bentnib). #ITP #Agda

13-Ago-20

• Datatypes as quotients of polynomial functors. ~ Jeremy Avigad. #ITP #LeanProver
• Model categories in Lean. ~ Reid Barton. #ITP #LeanProver #CategoryTheory
• A formalization of a Henkin-style completeness proof for propositional modal logic in Lean. ~ Bruno Bentzen. #ITP #LeanProver #Logic
• So what are hammers good for? ~ Jasmin Blanchette. #ITP #IsabelleHOL
• Data vs Control: a tale of two functors. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• Building a web library using super hard Haskell. ~ Marcin Rzeźnicki. #Haskell #FunctionalProgramming
• Zero-overhead abstractions in Haskell using staging. ~ Andres Löh. #Haskell #FunctionalProgramming

12-Ago-20

• Safety and conservativity of definitions in HOL and Isabelle/HOL. ~ Ondřej Kunčar, Andrei Popescu. #Logic #ITP #HOL #IsabelleHOL
• Coq Coq correct! (Verification of type checking and erasure for Coq, in Coq). ~ M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, T. Winterhalter. #ITP #Coq
• FreeSpec: Specifying, verifying and executing impure computations in Coq. ~ Thomas Letan, Yann Régis-Gianas. #ITP #Coq
• CoCon: A conference management system with formally verified document confidentiality. ~ Andrei Popescu, Peter Lammich, Ping Hou. #ITP #IsabelleHOL
• Haskell to core: Understanding Haskell features through their desugaring. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
• Agile generation of Cloud API bindings with Haskell. ~ Michal Gajda. #Haskell #FunctionalProgramming
• GraphQL ❤️ Haskell. ~ Alejandro Serrano. #Haskell #FunctionalProgramming

11-Ago-20

• Formalising undergraduate mathematics. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• [[http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/ug_maths.pdf][Formalising undergraduate mathematics [Slides]]]. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Read you a blaze. ~ Guru Devanla (@grdvnl). #Haskell #FunctionalProgramming
• Down to the wire. ~ Eric Torreborre. #Haskell #FunctionalProgramming
• Getting acquainted with Lens. ~ Pawel Szulc. #Haskell #FunctionalProgramming
• Stan: Haskell static analyser. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
• El lenguaje Prolog: un ejemplo del paradigma de programación lógica. ~ Marcos Merino (@MarcosMerino_B) #Prolog #ProgramaciónLógica

10-Ago-20

• Testing Haskell code with Stack, Ghcid and Hspec. ~ Iori Matsuhara (@Matsumonkie). #Haskell #FunctionalProgramming
• How a Haskell programmer wrote a tris in Purescript. ~ Henri Tuhola (@HenriTuhola). #Haskell #Purescript #FunctionalProgramming
• Lorentz: Achieving correctness with Haskell Newtypes. ~ Kostya Ivanov. #Haskell #FunctionalProgramming
• Functional dependencies. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming
• Clojure basics: How code is evaluated. #Clojure #FunctionalProgramming
• Elastic sheet-defined functions. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
• The many faces of isOrderedTree. ~ Joachim Breitner. #Haskell #FunctionalProgramming
• Bit vectors without compromises. ~ Andrew Lelechenko. #Haskell #FunctionalProgramming

09-Ago-20

• Verified textbook algorithms (A biased survey). ~ T. Nipkow, M. Eberl, M.P.L. Haslbeck. #ITP #FormalVerification #Algorithms
• Tools for teaching Theoretical Computer Science. ~ Sam Lowenstein. #ITP #Coq
• Haskell - Extracting IO. ~ Ken Aguilar. #Haskell #FunctionalProgramming
• Lenses for tree traversas. ~ Michael Peyton Jones (@mpeytonjones). #Haskell #FunctionalProgramming
• Definitional lawfulness: proof by inspection testing. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming
• Finding proofs in Tarskian geometry. ~ M. Beeson, L. Wos. #ATP #Otter #Math via @SandMouth
• Defunctionalizing arithmetic to an abstract machine. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming #Math

08-Ago-20

• The Tactician (extended version): A seamless, interactive tactic learner and prover for Coq. ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning
• Theorem proving in Lean (Release 3.18.4, Aug 06, 2020). ~ Jeremy Avigad, Leonardo de Moura, Soonho Kong. #eBook #ITP #LeanProver
• Formalizing 100 theorems in Lean. #ITP #LeanProver #Math
• Designing critical digital systems (Formal verification of a token player for synchronously executed Petri Nets). ~ Vincent Iampietro. #ITP #Coq
• Formalizing foundational notions in Naproche-SAD. ~ P. Koepke, J. Penquitt, M. Schütz, E. Sturzenhecker. #ITP #NaprocheSAD #Math
• «Four in a Row» in Haskell (Part I: Background and General Considerations). ~ Patrick Bucher. #Haskell #FunctionalProgramming
• «Four in a Row» in Haskell (Part II: Implementation of the Board Logic). ~ Patrick Bucher. #Haskell #FunctionalProgramming
• Some fundamental theorems in Mathematics. ~ Oliver Knill. #Math

05-Ago-20

• Eliminating bugs with dependent Haskell(Experience report). ~ Noam Zilberstein. #Haskell #FunctionalProgramming
• Staged sums of products. ~ Matthew Pickering, Andres Löh, Nicolas Wu. #Haskell #FunctionalProgramming
• GHC exercises (A little course to learn about some of the more obscure GHC extensions). ~ Tom Harding (@am_i_tom). #Haskell #FunctionalProgramming
• Generic traversals with applicative difference lists. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming

04-Ago-20

• Effect handlers in Haskell, evidently. ~ N. Xie, D. Leijen. #Haskell #FunctionalProgramming
• Stitch: the sound type-indexed type checker (functional pearl). ~ R.A. Eisenberg. #Haskell #FunctionalProgramming
• Composing effects into tasks and workflows. ~ Y. Parès, J.P. Bernardy, R.A. Eisenberg. #Haskell #FunctionalProgramming
• Type your matrices for great good (Functional pearl): A Haskell library of typed matrices and applications. ~ Armando Santos (@_bolt12). #Haskell #FunctionalProgramming #Math
• A mathematical formulation of the tax code? (Reverse engineering the tax code and analysis by automated theorem proving). ~ Denis Merigoux. #ATP #SMT
• Problem solving strategies. ~ Terence Tao (2010). #Math
• Emacs for statisticians (Part 1): Analyzing data on remote servers using Spacemacs and ESS. ~ Sergio Olmos (@solmos41). #Emacs #Rstat
• Lectures on mathematical computing with Python. ~ Jay Gopalakrishnan. #eBook #Python #Math

03-Ago-20

• #ForMatUS: Libro “Matemáticas en Lean”. #DAO #LeanProver #Matemáticas
• Checkpoint: Implementing linear relations for linear time invariant systems. ~ Philip Zucker (@SandMouth). #JuliaLang #CategoryTheory
• Describing microservices using modern Haskell. ~ Alejandro Serrano (@trupill). #FuncionalProgramming #Haskell

02-Ago-20

• Solving text adventure games via symbolic execution. ~ Gergő Érdi. #Haskell #FunctionalProgramming #SMT

Julio de 2020

01-Jul-20

• The complex number game, levels 1 to 3. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Logic and computation intertwined. ~ Prabhakar Ragde (@plragde). #eBook #Logic #ITP #Agda #Coq
• Teach yourself Racket. ~ Prabhakar Ragde (@plragde). #eBook #Racket #FunctionalProgramming
• Functional data structures. ~ Prabhakar Ragde (@plragde). #eBook #OCaml #FunctionalProgramming #Algorithms

02-Jul-20

• Certifying the weighted path order. ~ R. Thiemann, J. Schöpf, C. Sternagel, A. Yamada. #ITP #IsabelleHOL
• Notes on “Programming language foundations in Agda”. ~ Prabhakar Ragde (@plragde). #eBook #ITP #Agda
• Dependent types and software verification. ~ Prabhakar Ragde (@plragde). #ITP #Agda
• Proust: A nano proof assistant. ~ Prabhakar Ragde (2016). #Logic #Racket #ITP #Proust
• Functional Pearls: Composable data visualizations. ~ T. Petricek. #FunctionalProgramming #Fsharp
• Total functional programming. ~ D.A. Turner (2004). #FunctionalProgramming

03-Jul-20

• Higher-order Logic as Lingua franca (Integrating argumentative discourse and deep logical analysis). ~ David Fuenmayor, Christoph Benzmüller. #ITP #IsabelleHOL
• Equality, specifications, and implementations. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math #CompSci
• Modeling state machines with dependent types in Haskell: Part 1. ~ Evgeny Poberezkin (@epoberezkin). #Haskell #FunctionalProgramming
• Abstract algebra cheatsheet: a visual summary of key structures in abstract algebra. ~ Matthias Vallentin. #Math

04-Jul-20

• Reasoning about algebraic structures with implicit carriers in Isabelle/HOL. ~ W. Guttmann. #ITP #IsabelleHOL #Math
• Binary intersection formalized. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
• The hydra and the rooster. ~ Pirre Castéran. #ITP #Coq #Math
• Teaching automated theorem proving by example: PyRes 1.2: (System description). ~ S. Schulz, A. Pease. #ATP #Logic #Python
• Unification in Julia. ~ Philip Zucker (@SandMouth). #Logic #JuliaLang
• Some thoughts on building software. ~ Alejandro Serrano (@trupill). #FuncionalProgramming #Haskell
• Sphere eversion. ~ Ricky Reusser. #Math

05-Jul-20

• Formalizing a Seligman-style tableau system for hybrid logic. ~ Asta Halkjær From, Patrick Blackburn, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
• Prawf: An interactive proof system for program extraction. ~ Ulrich Berger, Olga Petrovska, Hideki Tsuiki. #ITP #Haskell #FunctionalProgramming #Logic
• Formalizing the face lattice of polyhedra. ~ Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. #ITP #Coq #Math

06-Jul-20

• The mechanization of Mathematics. ~ Jeremy Avigad (2018). #ITP #Math
• Category theory in the E automated theorem prover. ~ Philip Zucker (@SandMouth). #ATP #CategoryTheory
• Division by zero in type theory: a FAQ. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math

07-Jul-20

• Formal topology in Univalent Foundations. ~ Ayberk Tosun. #MsC_Thesis #ITP #Agda #Math
• Certifying time complexity of Agda programs using complexity signatures. ~ Christian Bach Møllnitz, Johannes Elgaard, Simon Rannes. #Agda #FunctionalProgramming
• Scientific proof-oriented programming (S-pop). ~ Philip Thrift (@philipthrift). #CompSci
• Retrie: Haskell refactoring made easy. #Haskell #FunctionalProgramming

09-Jul-20

• [[https://leanprover-community.github.io/lftcm2020/][Lean for the curious mathematician: A virtual workshop on computer-checked mathematics [13–17 July 2020]]]. #ITP #LeanProver #Math
• Theorems in transcendental number theory. ~ Jujian Zhang. #ITP #LeanProver #Math
• La conjetura de Gilbreath. ~ Juan Arias de Reyna. #Matemáticas

10-Jul-20

• Introduction to Univalent Foundations of Mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #Math
• A survey on theorem provers in formal methods. 4 M. Saqib Nawaz, Moin Malik, Yi Li, Meng Sun and M. Ikram Ullah Lali. #ITP #ATP #FormalMethods
• A survey of languages for formalizing mathematics. ~ Cezary Kaliszyk, Florian Rabe. #ITP #Math

11-Jul-20

• A micro prover for teaching automated reasoning. ~ J. Villadsen. #ITP #IsabelleHOL #Logic
• Textbook mathematics in the Naproche-SAD system. ~ P. Koepke. #ITP #Math
• Formal analysis of unmanned aerial vehicles using higher-order-logic theorem proving. ~ Sa’ed Abed, Adnan Rashid, Osman Hasan. #ITP #HOL_Light
• Animated logic: Correct functional conversion to conjunctive normal form. ~ António Ravara, Mário Pereira, Pedro Barroso. #Logic #Why3
• Testing Mizar user interactivity in a University-level introductory course on foundations of Mathematics. ~ Adam Naumowicz. #ITP #Mizar #Math
• Strong extension-free proof systems. ~ Marijn J H Heule, Benjamin Kiesl, Armin Biere. #SAT
• Online convex optimization with Haskell. ~ Valentin Reis. #Haskell #FunctionalProgramming #Math
• Competitive programming in Haskell: 2D cross product, part 1. ~ Brent Yorgey. #Haskell #FunctionalProgramming

12-Jul-20

• Type safety in two easy lemmas. ~ Jeremy Siek (@jeremysiek). #ITP #Agda
• Performance of Haskell Array libraries through Canny edge detection. ~ Alexey Kuleshevich. #Haskell #FuncionalProgramming

13-Jul-20

• Learning selection strategies in Buchberger’s algorithm. ~ Dylan Peifer, Michael Stillman, Daniel Halpern-Leistner. #MachineLearning #Math
• Por qué Matemáticas ha pasado de ser una carrera minoritaria a una de las más codiciadas y de moda. ~ Carlos Prego. #Matemáticas
• Deriving the State monad from first principles. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming

14-Jul-20

• Adventures in verifying arithmetic. ~ John Harrison. #ITP #HOL_Light #Math
• The natural number game : an introduction to Lean tactics. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• The ten (or so) basic tactics. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver
• Infinitude of primes: a Lean theorem prover demo. ~ Scott Morrison. #ITP #LeanProver #Math
• Certifying emptiness of timed Büchi automata. ~ Simon Wimmer, Frédéric Herbreteau, Jaco van de Pol. #ITP #IsabelleHOL
• Development of a tropical algebraic geometry package in the Haskell programming language. ~ Fernando Patricio Zhapa Camacho. #PhD_Thesis #Haskell #FunctionalProgramming #Math

15-Jul-20

• Optimization of Wu’s algorithm for the elimination of polynomial variables by High-Performance Computing (HPC). ~ José Luis Seraquive Cuenca. #Haskell #FunctionalProgramming #Math
• Record constructors. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
• Qualified do: rebind your do-notation the right way. ~ Matthías Páll Gissurarson, Facundo Domínguez, Arnaud Spiwack. #Haskell #FunctionalProgramming
• Metaprogramming in Lean. ~ Robert Y. Lewis. #ITP #LeanProver
• A one-line proof of the infinitude of primes. ~ Jason Orendorff. #ITP #LeanProver #Math
• A Lean tactic for normalising ring expressions with exponents. ~ Anne Baanen. #ITP #LeanProver #Math
• Formalization of forcing in Isabelle/ZF. ~ Pedro Sánchez Terraf. #ITP #Isabelle #Math
• The resolution of Keller’s conjecture. ~ Marijn Heule. #ATP #SAT_Solver #Math
• Mathematics in Lean introduction. ~ Patrick Massot. #ITP #LeanProver #Math #LftCM2020
• Logic in Lean. ~ Jeremy Avigad. #ITP #LeanProver #Math #LftCM2020

16-Jul-20

• Numbers in Lean. ~ Rob Lewis. #ITP #LeanProver #Math #LftCM2020
• Sets in Lean. ~ Jeremy Avigad. #ITP #LeanProver #Math #LftCM2020
• Structures and classes in Lean. ~ Floris van Doorn. #ITP #LeanProver #Math #LftCM2020
• Building an algebraic hierarchy in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math #LftCM2020
• Lean at Mathcamp 2020. ~ Apurva Nakade, Jalex Stark. #ITP #LeanProver #Math

17-Jul-20

• Building the topological hierarchy in Lean. ~ Alex Best. #ITP #LeanProver #Math #LftCM2020
• PubSub implementation in Haskell with formal verification in Coq. ~ Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska. #Haskell #FunctionalProgramming #ITP #Coq
• Haskell style guide. ~ Kowainik. #Haskell #FunctionalProgramming
• Forbidden Haskell types. ~ Ashley Yakeley. #Haskell #FunctionalProgramming
• The evolution of a Scheme programmer. ~ Erkin Batu Altunbaş. #Programming #Scheme

18-Jul-20

• Managing Haskell extensions. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
• Optimizing ray tracing in Haskell. ~ Sarfaraz Nawaz. #Haskell #FunctionalProgramming
• Order structures in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math #LftCM2020
• Groups, rings, and fields in Lean. ~ Johan Commelin. #ITP #LeanProver #Math #LftCM2020
• Lean for the Curious Mathematician 2020. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math #LftCM2020

19-Jul-20

• Linear algebra in Lean. ~ Anne Baanen.c#ITP #ITP #LeanProver #Math #LftCM2020
• Category theory in Lean. ~ Scott Morrison. #ITP #LeanProver #Math #LftCM2020
• Topology and filters in Lean. ~ Patrick Massot. #ITP #LeanProver #Math #LftCM2020
• Calculus and integration in Lean. ~ Yury Kudryashov. #ITP #LeanProver #Math #LftCM2020
• Simplifying casts and coercions. ~ Robert Y. Lewis, Paul-Nicolas Madelaine. #ITP #LeanProver
• Competitive programming in Haskell: cycle decomposition with mutable arrays. ~ Brent Yorgey. #Haskell #FunctionalProgramming

20-Jul-20

• Differential geometry in Lean. ~ Sebastien Gouëzel. #ITP #LeanProver #Math #LftCM2020
• Verification of ML systems via reparameterization. ~ Jean-Baptiste Tristan et als. #ITP #LeanProver #MachineLearning
• Modal FRP For All (Functional reactive programming without space leaks in Haskell). ~ Patrick Bahr. #Haskell #FunctionalProgramming #ITP #Coq
• Contributions to a science of contemporary mathematics. ~ Frank Quinn. #Math

21-Jul-20

• Metamath Zero: Designing a theorem prover prover. ~ Mario Carneiro. #ITP #MethamathZero0
• A promising path towards autoformalization and general Artificial Intelligence. ~ Christian Szegedy. #MKM #AI #ITP #MachineLearning0
• Graphics in Haskell: linear algebra. ~ David Alexander Stuart. #Haskell #FunctionalProgramming #Math
• How to read Haskell Documentation. Step by step guide. ~ Theofanis Despoudis. #Haskell #FunctionalProgramming

22-Jul-20

• Formalizing graph trail properties in Isabelle/HOL. ~ Laura Kovács, Hanna Lachnitt, Stefan Szeider. #ITP #IsabelleHOL #Math0
• Leveraging the information contained in theory presentations. ~ Jacques Carette, William M. Farmer, Yasmine Sharoda. #ITP #Agda #IsabelleHOL #LeanProver
• A framework for formal dynamic dependability analysis using HOL theorem proving. ~ Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar. #ITP #HOL4
• Maintaining a library of formal mathematics. ~ Floris van Doorn, Gabriel Ebner, Robert Y. Lewis. #ITP #LeanProver #Math

23-Jul-20

• Formalizing Henkin-Style completeness of an axiomatic system for propositional logic. ~ Asta Halkjær From. #ITP #IsabelleHOL #Logic
• Two types of universe for two types of mathematician. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• The Tactician (A seamless, interactive tactic learner and prover for Coq). ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning
• Computational logic for biomedicine and neurosciences. ~ A. Bahrami, E. de Maria, J. Despeyroux, A. Felty, P. Lió. #ITP #Coq
• Tree neural networks in HOL4. ~ Thibault Gauthier. #ITP #HOL4 #NeuralNetwork
• The stillness of Haskell code. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming

24-Jul-20

24-Jul-20

• A formally verified compiler for programs that deal with cached address translation. ~ J. Andersson. #MsC_Thesis #ITP #IsabelleHOL
• An MIU decision procedure in Lean. ~ Gihan Marasingha. #ITP #LeanProver
• [[http://kodu.ut.ee/%7Evarmo/tday-andu/chapman-slides.pdf][A biased history of equality in type theory]. (Some equations are more equal than others)]]. ~ James Chapman. #TypeTheory #ITP #Coq
• Who verifies the verifiers? A computer-checked implementation of the DPLL algorithm in Dafny. ~ Cezar-Constantin Andrici, Ştefan Ciobâcă. #Dafny #Logic
• Towards verified Artificial Intelligence. ~ Sanjit A. Seshia, Dorsa Sadigh, S. Shankar Sastry. #AI #FormalVerification

25-Jul-20

25-Jul-20

• Playing with the tower of Hanoi formally. ~ Laurent Théry. #ITP #Coq
• Towards secure IoT programming in Haskell. ~ N. Valliappan, R. Krook, A. Russo, K. Claessen. #Haskell #FunctionalProgramming
• Setting up Haskell development environment: The basics. #Haskell #FunctionalProgramming
• Strong functional pearl: Harper’s regular-expression matcher in Cedille. ~ Aaron Stump et als. #Haskell #Cedille #FunctionalProgramming
• Approaches to the implementation of generalized complex numbers in the Julia language. ~ M.N. Gevorkyan, A.V. Korolkova, D.S. Kulyabov. #JuliaLang #Math

26-Jul-20

• Formalizing Nakamoto-style proof of Stake. ~ Søren Eller Thomsen, Bas Spitters. #ITP #Coq

28-Jul-20

• Relational characterisations of paths. ~ Walter Guttmann, Peter Höfner. #ITP #IsabelleHOL
• Formally verifying proofs for algebraic identities of matrices. ~ Leonard Schmitz, Viktor Levandovskyy. #ITP
• Formally verified constraint solvers. ~ Catherine Dubois, Sourour Elloumi, Arnaud Gotlieb. #ITP #Coq #CSP
• Machine learning in Haskell. ~ @tonyday567 #Haskell #FunctionalProgramming #MachineLearning
• The golden rule of software quality. ~ G. Gonzalez (@GabrielG439). #Programming #Haskell
• Día Mundial de la Lógica 2021. #Lógica

30-Jul-20

• Metamath Zero: Designing a theorem prover prover. ~ #ITP
• Maintaining a library of formal Mathematics. ~ Gabriel Ebner. #ITP #LeanProver #Math

31-Jul-20

• Automated verification of reactive and concurrent programs by calculation. ~ Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock. #ITP #Isabelle
• Certifying a rule-based model transformation engine for proof preservation. ~ Z. Cheng, M. Tisi, J. Hotonnier. #ITP #Coq

Junio de 2020

01-Jun-20

• Breve historia de Haskell. ~ Emanuel Goette (@emanuelpeg). #Haskell #ProgramaciónFuncional

03-Jun-20

• The Nash-Williams partition theorem in Isabelle/HOL. ~ Lawrence C. Paulson. #ITP #IsabelleHOL
• Setting up a Haskell development environment with Nix. ~ Romain Viallard. #Haskell #Nix
• Big step normalisation for type theory. ~ Thorsten Altenkirch, Colin Geniet. #ITP #Agda
• Carnegie Mellon tool automatically turns math into pictures. #Math
• Penrose: from mathematical notation to beautiful diagrams. ~ Katherine Ye el als. #Math

04-Jun-20

• Welcome to The Proof Theory Blog! ~ Anupam Das. #Logic #Math
• Penrose: Create beautiful diagrams just by typing mathematical notation in plain text. #Haskell #DSL #Math #Visualization
• Lean tutorial for mere mortals. ~ Alcides Fonseca. #ITP #LeanProver
• A formally verified checker of the safe distance traffic rules for autonomous vehicles. ~ Albert Rizaldi, Fabian Immler. #ITP #IsabelleHOL

05-Jun-20

• Isomorphic data type transformations. ~ Alessandro Coglio, Stephen Westfold. #ITP #ACL2
• Cellular cohomology in homotopy type theory. ~ Ulrik Buchholtz, Kuen-Bang Hou. #ITP #Agda #Math
• A history of Clojure. ~ Rich Hickey. #Clojure #FunctionalProgramming
• Adventures in refactoring. ~ Sam Tay. #Haskell #FunctionalProgramming
• Reanimate: a tutorial on making programmatic animations. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming

06-Jun-20

• Using Template Haskell to generate boilerplate. ~ Jonathan Dowland. #Haskell #FunctionalProgramming
• Simulated annealing. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming
• Trusting toList. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
• Formal verification: History and methods. ~ Danya Rogozin. #FormalVerification
• Red Blob Games: interactive visual explanations of math and algorithms, using motivating examples from computer games. ~ Amit Patel. #Algorithms
• Toy machine learning with Haskell. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming #MachineLearning
• The sphere eversion project. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Algorithm design with Haskell. ~ Richard Bird, Jeremy Gibbons.1#v=onepage&q&f=false #eBook #Haskell #FunctionalProgramming #Algorithms

07-Jun-20

• Formalization of the computational theory of a Turing complete functional language model. ~ TMF Ramos, AA Almeida, M Ayala-Rincón. #ITP #PVS
• The proof-theoretic foundations of logic programming. ~ Dale Miller. #LogicProgramming

08-Jun-20

• What is Mathematics? ~ Get Smarter. #Math
• Formalizing text editors in Coq. ~ Boro Sitnikovski. #ITP #Coq
• Making the most of Cabal. ~ Luke Lau. #Haskell #FunctionalProgramming
• The pain points of Haskell: A practical summary. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming

09-Jun-20

• Functional programming in data science projects. ~ Nathanael Weill. #FuncionalProgramming #DataScience

10-Jun-20

• Using client-side Haskell web frameworks in CodeWorld. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld
• 4 excellent free books to learn Agda and type theory. ~ Erik Karlsson. #ITP #Agda #FunctionalProgramming #TypeTheory
• Disco: Functional teaching language for use in a discrete mathematics course. ~ Brent Yorgey. #Haskell #FunctionalProgramming #DSL #Math
• Hoogle searching overview. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming

11-Jun-20

• The ‘useless’ perspective that transformed mathematics. ~ Kevin Hartnett (@KSHartnett). #Math
• “The truth: What is the truth?”, at Gödel’s Lost Letter and P=NP. ~ R.J. Lipton. #Logic #Math
• Scripting in Haskell: Parsing command line arguments. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
• Template Haskell and stream-processing programs. ~ Jonathan Dowland (@jmtd). #Haskell #FunctionalProgramming
• How to design co-programs. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• Conway’s circle theorem: a proof, this time with words. ~ Colin Beveridge, Elizabeth A. Williams. #Math
• Monadic equational reasoning in Coq. ~ Reynald Affeldt. #ITP #Coq
• Category theory for computing science. ~ Michael Barr, Charles Wells (1998). #eBook #CategoryTheory #Math #CompSci
• Seven sketches in compositionality: An invitation to applied category theory. ~ Brendan Fong, David I. Spivak (2018). #eBook #CategoryTheory #Math #CompSci

12-Jun-20

• What functional programming is, what it isn’t, and why it matters. ~ Noel Welsh. #FunctionalProgramming
• Simple Haskell install instructions - ZuriHac 2020. #Haskell #FunctionalProgramming
• La logique: un instrument théorique pour des problèmes pratiques. ~ Franco Raimondi. #Logic #Math #CompSci

13-Jun-20

• Deploying your application with NixOS. ~ Romain Viallard. #Nix #Haskell
• An extended comparative study of language support for generic programming. ~ Ronald Garcia, Jaakko J Ärvi, Andrew Lumsdaine, Jeremy Siek, Jeremiah Willcock. #Cpp #SML #OCaml #Haskell #Eiffel #Java #Csharp #Cecil.
• Towards a verified first-stage bootloader in Coq. ~ Zygimantas Straznickas. #MsC_Thesis #ITP #Coq
• Completeness theorems for first-order logic analysed in constructive type theory. ~ Yannick Forster, Dominik Kirst, Dominik Weh. #ITP #Coq #Logic
• Efficient verified implementation of introsort and pdqsort. ~ Peter Lammich. #ITP #IsabelleHOL
• (Programming Languages) in Agda = Programming (Languages in Agda). ~ Philip Wadler. #ITP #Agda

14-Jun-20

• Verifying strong eventual consistency in δ-CRDTs. Taylor Blau. #ITP #IsabelleHOL
• The history of Standard ML. ~ David MacQueen, Robert Harper, John Reppy. #SML #FunctionalProgramming
• Programación funcional: Próximamente en un lenguaje de programación cerca de usted. ~ Andrés Marzal. #ProgramaciónFuncional
• Awesome Haskell videos (A collection of awesome Haskell videos). ~ @_andys8 #Haskell #FunctionalProgramming

15-Jun-20

• Type inference. ~ Splinter Suidman. #Haskell #FunctionalProgramming
• Practical proof search for Coq by type inhabitation. ~ Lukasz Czajka. #ITP #Coq
• Validating mathematical structures. ~ Kazuhiko Sakaguchi. #ITP #Coq #math
• Competing inheritance paths in dependent type theory: a case study in functional analysis. ~ Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling and Kazuhiko Sakaguchi. #ITP #Coq #Math
• Quotients of bounded natural functors. ~ Basil Fürer, Andreas Lochbihler, Joshua Schneider and Dmitriy Traytel. #ITP #IsabelleHOL
• Application of formal systems to model biological systems. ~ @prathyvsh #Math #Biology

16-Jun-20

• Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. ~ Clément Pit-Claudel, Peng Wang, Benjamin Delaware, Jason Gross and Adam Chlipala. #ITP #Coq
• Adventures in verifying arithmetic. ~ John Harrison. #ITP #HOL_Light #Math
• A formally verified, optimized monitor for metric first-order dynamic logic. ~ David Basin, Thibault Dardinier, Lukas Heimes, Srđan Krstić, Martin Raszyk, Joshua Schneider, Dmitriy Traytel. #ITP #IsabelleHOL
• The resolution of Keller’s conjecture. ~ Joshua Brakensiek, Marijn Heule, John Mackey, David Narvaez. ~ #ATP #SAT_Solver #Math
• Monoidal catamorphisms. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #CategoryTheory
• Free Math Textbooks. #Math
• The power of IO in Haskell. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
• Training our agent with Haskell! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming

17-Jun-20

• A Lean tactic for normalising ring expressions with exponents. ~ Anne Baanen. #ITP #LeanProver #Math
• Verified approximation algorithms. ~ Robin Eßmann, Tobias Nipkow, Simon Robillard. #ITP #IsabelleHOL
• Análisis de texto usando funciones de orden superior. ~ Emanuel Goette (@emanuelpeg). #Haskell #ProgramaciónFuncional
• Using Template Haskell to generate static data. ~ Andreas Klebinger. #Haskell #FunctionalProgramming

18-Jun-20

• Computer-assisted proofs for Lyapunov stability via Sums of Squares certificates and Constructive Analysis. ~ Grigory Devadze, Victor Magron, Stefan Streif. #ITP #MinLog #Math
• Basic optics: lenses, prisms, and traversals in Haskell. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming

19-Jun-20

• Simple linear regression in one pass. ~ Daniel Brice (@fried_brice). #Haskell #FuncionalProgramming
• Solving algorithm challenges in Haskell: Anagrams. ~ Theofanis Despoudis (@nerdokto). #Haskell #FunctionalProgramming
• Lean 4. ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver
• Connected Papers: A visual tool to help researchers and practitioners find and explore academic papers. ~ @ConnectedPapers

20-Jun-20

• Linear types are merged in GHC. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• Proofs and computation with trees. ~ Boro Sitnikovski (@BSitnikovski). #Math #CompSci

21-Jun-20

• Mathematics in type theory. ~ Kevin Buzzard (@XenaProject). #Logic #Math #ITP #LeanProver
• Verified Isabelle/HOL tactic for the theory of bounded linear integer arithmeticl based on quantifier instantiation and SMT. ~ Rafael Sadykov , Mikhail Mandrykin. #ITP #IsabelleHOL #SMT
• An efficient normalisation procedure for linear temporal logic: Isabelle/HOL formalisation. ~ Salomon Sickert. #ITP #IsabelleHOL #Logic
• Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2. ~ David M. Russinoff. #ITP #ACL2

22-Jun-20

• Cauchy-Schwarz in ACL2(r) abstract vector spaces. ~ Carl Kwan, Yan Peng, Mark R. Greenstreet. #ITP #ACL2 #Math
• Quadratic extensions in ACL2. ~ Ruben Gamboa, John Cowles, Woodrow Gamboa. #ITP #ACL2 #Math
• Techniques for implementation of symbolically interpretable Haskell EDSLs. ~ Grigoriy Volkov. #Haskell #FunctionalProgramming

23-Jun-20

• Leibniz equality is isomorphic to Martin-Löf identity, parametrically. ~ Andreas Abel, Jesper Cockx, Dominique Devriese, Amin Timany. #ITP #Agda #FunctionalProgramming
• Strongly typed system F in GHC. ~ Stephanie Weirich. #Haskell #FunctionalProgramming #Logic
• An introduction to parsing text in Haskell with Parsec. ~ Nick Chung. #Haskell #FunctionalProgramming
• The HLint match engine. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming
• Rendering frozen lake with Gloss! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming

24-Jun-20

• Haskell for a new decade. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
• Calculating correct compilers II (Return of the register machines). ~ Patrick Bahr, Graham Hutton. #Haskell #FuncionalProgramming
• Lucas’s theorem: Formalising generating function proofs. ~ Chelsea Edmonds. #ITP #IsabelleHOL #Math
• Ackermann’s function in iterative form: A subtle termination proof with Isabelle/HOL. ~ Lawrence Paulson. #ITP #IsabelleHOL
• Axiomatic architecture of scientific theories. ~ Andrei V. Rodin. #PhD_Thesis #Logic #Math

25-Jun-20

• A concise sequent calculus for teaching first-order logic. ~ Asta Halkjær From, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
• SErAPIS : A concept-oriented search engine for the Isabelle libraries based on natural language. ~ Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL
• Authenticated data structures as functors in Isabelle/HOL. ~ Andreas Lochbihler, Ognjen Marić. #ITP #IsabelleHOL
• A generic framework for verified compilers using Isabelle/HOL’s locales. ~ Martin Desharnais, Stefan Brunthaler. #ITP #IsabelleHOL
• Competitive programming in Haskell: vectors and 2D geometry. ~ Brent Yorgey. #Haskell #FunctionalProgramming

26-Jun-20

• A mechanized proof of a textbook type unification algorithm. ~ Maycon Amaro, Rodrigo Ribeiro, André Rauber Du Bois. #ITP #Coq
• Reasoning about partial correctness assertions in Isabelle/HOL. ~ A.R. Martini. #ITP #IsabelleHOL
• Extensive infinite games and escalation, an exercice in Agda. ~ Pierre Lescanne. #ITP #Agda
• Animated logic: Correct functional conversion to conjunctive normal form. ~ Pedro Barroso, Mário Pereira, António Ravara. #Why3 #Logic

27-Jun-20

• Teaching interactive proofs to mathematicians. ~ M. Ayala-Rincón, T.A. de Lima. #ITP #PVS #Math
• Interactively proving mathematical theorems. ~ M. Ayala-Rincón et als. #Logic #Math #ITP #PVS
• Undergraduate mathematics in mathlib. #ITP #LeanProver #Math
• Formalization of ring theory in PVS (Isomorphism theorems, principal, prime and maximal ideals ,chinese remainder theorem). ~ T.A. de Lima, A L. Galdino, A. Borges Avelar, M. Ayala-Rincón. #ITP #PVS #Math
• Why we need structured proofs in mathematics. ~ M. Ayala-Rincón, G.F. Silva. #Logic #Math #ITP #PVS
• Lambda Calculus - step by step. ~ Helmut Brandl. #Logic #Math #CompSci #LambdaCalculus
• Programming with Lambda Calculus. ~ Helmut Brandl. #Logic #Math #CompSci #LambdaCalculus
• The quest for Artificial Intelligence (A history of ideas and achievements). ~ Nils J. Nilsson. #eBook #AI

28-Jun-20

• Teaching dependent type theory to 4 year olds via mathematics. ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver
• Deep generation of Coq lemma names using elaborated terms. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq

29-Jun-20

• El traje nuevo de la inteligencia artificial. ~ Ramon López de Mántaras. #IA
• Try these 4 languages from 4 corners of programming. ~ Saurabh Sharma (@itsjzt). #C #Smalltak #Clojure #Haskell
• Using Haskell in the Mission Control Domain. ~ Michael Oswald (@OswaldChocolate). #Haskell #FunctionalProgramming

30-Jun-20

• Splittable pseudo-random number generators in Haskell: random v1.1 and v1.2. ~ Leonhard Markert. #Haskell #FunctionalProgramming #Math
• Formalizing the soundness of the encoding methods of SAT-based model checking. ~ Daisuke Ishii, Saito Fujii. #ITP #Coq
• Teaching Lean what a group is (ignoring the fact that it actually already knows). ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Competitive programming in Haskell: data representation and optimization, with cake. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Algorithm design with Haskell. ~ Jeremy Gibbons (@jer_gib). #Haskell #FunctionalProgramming

Mayo de 2020

1-May-20

• Gaussian integers in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Power sum polynomials and the Girard–Newton theorem in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• The Ramanujan Machine: Automatically generated conjectures on fundamental constants. ~ Gal Raayoni et als. #MachineLearning #Math
• UWisconsin course on Haskell and Rust. #Haskell #Rust
• Learn to moonwalk with waterflow problem. ~ Murat Kasimov. #Haskell #FunctionalProgramming
• Property testing in depth: genvalidity’s fixed-size type generators. ~ Tom Sydney Kerckhove. #Haskell #QuickCheck

2-May-20

• New AI enables teachers to rapidly develop intelligent tutoring systems. #AI #Teaching
• Verified certification of reachability checking for timed automata. ~ Simon Wimmer, Joshua von Mutius. #ITP #IsabelleHOL
• Formalized proofs of the infinity and normal form predicates in the first-order theory of rewriting. ~ Alexander Lochmann, Aart Middeldorp. #ITP #IsabelleHOL
• Formal proof of the group law for Edwards elliptic curves. ~ Thomas Hales, Rodrigo Raya. #ITP #IsabelleHOL #Math
• Formal adventures in convex and conical spaces. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Math

3-May-20

• More random access lists. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
• History of Logo. ~ C. Solomon et als. #Logo #Programming
• Interactive teaching of programming language theory with a proof assistant. ~ Horpácsi Dániel et als. #ITP #Coq
• A problem-based curriculum for algorithmic programming. ~ Nikházy László. #Programming
• Bye-bye Python. Hello Julia! ~ Rhea Moutafis (@RheaMoutafis). #Python #JuliaLang #Programming

4-May-20

• Design by Contract with Lean theorem prover. ~ Nam Nguyen. #ITP #LeanProver #Programming

5-May-20

• Data flow - what functional programming and Unix philosophy can teach us about data streaming. ~ Bartosz Mikulski (@mikulskibartosz). #FunctionalProgramming
• Intervals and their relations. ~ Marco Perone (@marcoshuttle). #Haskell #FunctionalProgramming #Math
• Frozen lake in Haskell. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI
• Advanced programming languages. ~ Matt Might (@mattmight). #Haskell #Scala #SML #OCaml #Scheme #FunctionalProgramming
• The age of algorithms. ~ Serge Abiteboul, Gilles Dowek. #eBook #Algorithms

6-May-20

• Proving theorems with computers. ~ Kevin Buzzard. #ITP #Math
• Formalization of forcing in Isabelle/ZF. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic
• Banach-Steinhaus theorem in Isabelle/HOL. ~ Dominique Unruh, Jose Manuel Rodriguez Caballero. #ITP #IsabelleHOL #Math

8-May-20

• Eat Haskell String Types for Breakfast. ~ Ziyang Liu. #Haskell #FunctionalProgramming
• Environment variables parsing for free (applicatives). ~ Clément Delafargue. #Haskell #FunctionalProgramming
• Monoids as one-object categories, or not? ~ @Iceland_jack #Haskell #FunctionalProgramming #CategoryTheory
• π with leftovers: a mechanisation in Agda. ~ Uma Zalakain, Ornela Dardha. #ITP #Agda
• The Chalmers Online Functional Programming Seminar Series. #FunctionalProgramming

9-May-20

• An efficient normalisation procedure for linear temporal logic: Isabelle/HOL formalisation. ~ Salomon Sickert. #ITP #IsabelleHOL
• Matrices for ODEs in Isabelle/HOL. ~ Jonathan Julian Huerta y Munive. #ITP #IsabelleHOL #Math
• A linear algebra approach to linear metatheory. ~ James Wood, Robert Atkey. #ITP #Agda
• Certified semantics for relational programming. ~ Dmitry Rozplokhas, Andrey Vyatkin, Dmitry Boulytchev. #ITP #Coq
• Why is Lisp not as popular as Python? ~ Jan Meww (@JanMeww). #Python #CommonLisp #Scheme #Clojure

10-May-20

• Learning programs by learning from failures. ~ Andrew Cropper, Rolf Morel. #ILP #MachineLearning #LogicProgramming

11-May-20

• Clean vs. defaulty representations in Prolog. ~ Markus Triska (@MarkusTriska). #Prolog #LogicProgramming
• Diagram chasing in interactive theorem proving. ~ Markus Himmel. #BsC_Thesis #ITP #LeanProver #Math
• Learning selection strategies in Buchberger’s algorithm. ~ Dylan Peifer, Michael Stillman, Daniel Halpern-Leistner. #MachineLearning #Math
• On the effect of learned clauses on stochastic local search. ~ Jan-Hendrik Lorenz, Florian Wörz. #ATP #SAT_solvers
• L’intelligence artificielle et l’apprentissage profond. ~ Benjamin Bradu. #AI #DeepLearning
• Extensions. ~ Veronika Romashkina (@vrom911). #Haskell #FunctionalProgramming
• Indexed monads: examples and discussion. ~ Adam Wespiser (@wespiser). #Haskell #FunctionalProgramming

12-May-20

• The origins and motivations of univalent foundations (A personal mission to develop computer proof verification to avoid mathematical mistakes). ~ Vladimir Voevodsky (2014). #Logic #Math #ITP via @AngelikiKoutso1
• Evolution of Emacs Lisp. ~ Stefan Monnier et als. #Emacs #Lisp
• 15 reasons why I use Emacs, with GIFs. ~ Dominik Tarnowski. #Emacs
• Blackjack: Following the patterns. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI

14-May-20

• Recursion theorem in ZF. ~ Georgy Dunaev. #ITP #IsabelleZF #Logic #Math
• Haskell: Function application vs fmap vs sequential application vs bind. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
• The science behind functional programming. ~ Rafa Paradela. #CategoryTheory #FuncionalProgramming #Kotlin
• Irrationality criteria for series by Erdős and Straus in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Wenda Li. #ITP #IsabelleHOL #Math

15-May-20

• A quick look at impredicativity. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
• Proof-relevant category theory in Agda. ~ Jason Z.S. Hu, Jacques Carette. #ITP #Agda #CategoryTheory
• Janet: a functional and imperative programming language. #FunctionalProgramming #JanetLang
• MathZero, the classification problem, and set-theoretic type theory. ~ David McAllester. #MachineLearning #TypeTheory
• A formalization of Knuth–Bendix orders in Isabelle/HOL. ~ Christian Sternagel, René Thiemann. #ITP #IsabelleHOL

16-May-20

• Formalising Mathematics in a theorem prover. ~ K. Buzzard. #ITP #Math
• Types vs. datatypes vs. typeclasses in Haskell. ~ Jesse Evers (@_jlevers). #Haskell #FunctionalProgramming
• Automatic test generationfor Haskell programming assignments. ~ Vladimír Štill. #Haskell #FunctionalProgramming

17-May-20

• Vídeos de las clases de algorítmica con Haskell. #Haskell #ProgramaciónFuncional #Algorítmica #I1M2019
• Vídeos de las clases de razonamiento automático con Isabelle/HOL. #Lógica #DAO #IsabelleHOL #LMF2019
• Dynamic IFC theorems for free! ~ Maximilian Algehed, Jean-Philippe Bernardy, Cătălin Hrit. #ITP #Agda #FunctionalProgramming
• Machine-checked semantic session typing. ~ Jonas Kastberg Hinrichsen et als. #ITP #Coq
• MathZero, the classification problem, and set-theoretic type theory. ~ David McAllester. #MachineLearning #TypeTheory
• Interesting ATP proofs. #ATP #Logic #Math

18-May-20

• Automating Mathematics? ~ Siddhartha Gadgil. #ITP #Math
• ProvingGround: Automated Theorem proving by learning. ~ Siddhartha Gadgil. #ATP #Math #HoTT

19-May-20

• Purely functional data structures and monoids. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
• Frozen lake with Q-learning! ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #MachineLearning
• 2020 Berkeley Lean Seminar. #ITP #LeanProver
• Backtracking generators for random testing. ~ Benjamin Pierce. #ITP #Coq #FunctionalProgramming

20-May-20

• The essence of Bluespec (A core language for rule-based hardware design). Thomas Bourgeat et als. #ITP #Coq
• PubSub implementation in Haskell with formal verification in Coq. ~ Boro Sitnikovski, Biljana Stojcevska, Lidija Goracinova-Ilieva, Irena Stojmenovska. #Haskell #FuncionalProgramming #ITP #Coq
• Why functors and applicatives compose but monads don’t. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
• Why functors and applicatives compose but monads don’t. [Slides]. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming
• Competitive programming in Haskell: sorting tree shapes. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Galois theory for non-mathematicians. ~ Mikael Davidsson. #Math
• Stateful protocol composition and typing in Isabelle/HOL. ~ Andreas V. Hess, Sebastian Mödersheim, Achim D. Brucker. #ITP #IsabelleHOL

21-May-20

• Visualizing Cantor’s theorem on dense linear orders using Coq. ~ Evan Marzion. #ITP #Coq #Math

22-May-20

• The complex numbers are a ring. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• How to build with Stack. #Haskell #FunctionalProgramming
• How to script with Stack. #Haskell #FunctionalProgramming
• How to play with Stack. #Haskell #FunctionalProgramming
• Profiling and performance. #Haskell #FunctionalProgramming
• Monad transformers. #Haskell #FunctionalProgramming
• Recommended Haskell libraries. #Haskell #FunctionalProgramming
• String types. #Haskell #FunctionalProgramming
• Synonyms in base. #Haskell #FunctionalProgramming
• Lenses. #Haskell #FunctionalProgramming
• Safe exception handling. #Haskell #FunctionalProgramming
• Data types. #Haskell #FunctionalProgramming
• Data structures. #Haskell #FunctionalProgramming
• Common typeclasses. #Haskell #FunctionalProgramming
• Applied Haskell 101 course. #Haskell #FunctionalProgramming
• Crash course to applicative syntax. #Haskell #FunctionalProgramming
• All about strictness. #Haskell #FunctionalProgramming
• European Lisp Symposium 2020 videos. #Lisp #Programming
• SIXEL Library for Haskell: displaying images on ghci. ~ Junji Hashimoto. #Haskell #FunctionalProgramming
• Error messages in Haskell, and how to improve them. ~ Anthony Super. #Haskell #FunctionalProgramming

23-May-20

• Simple Haskell is best Haskell. ~ Sam Halliday. #Haskell #FunctionalProgramming
• Competitive programming in Haskell: building unordered trees. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Sets, logic and maths for computing. ~ David Makinson.1#v=onepage&q&f=false #eBook #Logic #Math #CompSci

24-May-20

• A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper. ~ Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger. #FuncionalProgramming #Haskell
• Mathematics in Lean. ~ Jeremy Avigad, Kevin Buzzard, Robert Y. Lewis, Patrick Massot. #ITP #LeanProver #Math
• Dynamically flunking the coding interview (A gentle introduction to functional dynamic programming). ~ Maxfield Chen. #Haskell #FunctionalProgramming
• The complex number game. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver
• Accumulating independent errors. ~ Tim Humphries (@thumphriees). #Haskell #FunctionalProgramming
• HandWiki: Online Encyclopedia of Science and Computing.
• How to generate random lambda terms? ~ Maciej Bendkowski. #Haskell #FunctionalProgramming

25-May-20

• Prototyping controlled mathematical languages in Jupyter notebooks. ~ Jan Frederik Schaefer, Kai Amann, Michael Kohlhase. #MKM
• Toward the formal verification of HILECOP: Formalization and implementation of synchronously executed Petri nets. ~ Vincent Iampietro, David Andreu, David Delahaye. #ITP #Coq
• A proof and formalization of the initiality conjecture of dependent type theory. ~ Menno de Boer. #ITP #Coq
• Symbolic reasoning about quantum circuits in Coq. ~ Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng. #ITP #Coq

26-May-20

• Simply typed lambda calculus. ~ Splinter Suidman. #Haskell #FuncionalProgramming #LambdaCalculus
• A verified algorithm for computing the Smith normal form of a matrix. ~ Jose Divasón. #ITP #IsabelleHOL #Math

27-May-20

• A survey of languages for formalizing mathematics. ~ Cezary Kaliszyk, Florian Rabe. #Logic #Math #ITP #MKM
• Monoidal puzzle solving. ~ Jonas Carpay (@jonascarpay) #Haskell #FunctionalProgramming

28-May-20

• Capítulo 1 de “Paradojas del nihilismo: La Academia”: Desilusión. #Universidad
• New LaTeX.css library enables websites to look like LaTeX docs. #LaTeX #Math

29-May-20

• Formalising perfectoid spaces. ~ Kevin Buzzard, Johan Commelin, Patrick Massot. #ITP #LeanProver #Math

30-May-20

• Natural numbers with addition form a monoid. ~ James Chapman. #ITP #Agda #Math
• Code-level model checking in the software development workflow. ~ Nathan Chong et als. #FormalVerification #ModelChecking
• How to integrate formal proofs into software development. ~ Daniel Schwartz-Narbonne. #FormalVerification
• Curry-Howard tutorial in literate Haskell. ~ Keith Pinson. #Haskell #FunctionalProgramming #Logic

31-May-20

• On marketing Haskell. ~ Stephen Diehl (@smdiehl) #Haskell #FunctionalProgramming
• A calculator with Reflex and CodeWorld. ~ Chris Smith (@cdsmithus). #Haskell #CodeWorld
• Competitive programming in Haskell: permutations. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Economic argument for functional programming. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming
• [[https://www.snoyman.com/reveal/economic-argument-functional-programming][Economic argument for functional programming [Slides]]]. ~ Michael Snoyman (@snoyberg). #Haskell #FunctionalProgramming
• A proof assistant based formalisation of core Erlang. ~ Péter Bereczky, Dániel Horpácsi, Simon Thompson. #ITP #Coq #Erlang
• Verification of closest pair of points algorithms. ~ Martin Rau, Tobias Nipkow. #ITP #IsabelleHOL #Algorithms

Abril de 2020

01-Abr-20

• There’s a mathematician in your compiler. ~ James Phillips. #Logic #Math #CompSci #Scala #FunctionalProgramming via @FunctorFact
• Animations in Kaleidogen. ~ Joachim Breitner (@nomeata). #Haskell #FunctionalProgramming
• Curried functions. ~ Graham Hutton (@haskellhutt). #Haskell #FunctionalProgramming
• Migrating from QuickCheck to Hedgehog: mixed results. ~ Fraser Tweedale (@hackuador). #Haskell #FunctionalProgramming

02-Abr-20

• A distributed and trusted web of formal proofs. ~ Dale Miller. #ITP #Logic #Math #CompSci
• Explosive proofs of mathematical truths. ~ Scott Viteri, Simon DeDeo. #ITP #Coq

03-Abr-20

• The Hitchhiker’s Guide to Logical Verification. ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl. #eBook #ITP #LeanProver
• Reasoning with conditional probabilities and joint distributions in Coq. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa. #ITP #Coq #Math
• Generalized monoidal effects and handlers. ~ Ruben P. Pieters, Tom Schrijvers, Exequiel Rivas. #Haskell #FunctionalProgramming
• Refactoring a neural network implementation in Haskell. ~ The H2 Wiki. #Haskell #FunctionalProgramming #NeuralNetwork
• ACM Open access to LFP (Conference on LISP and Functional Programming). #Lisp #FunctionalProgramming
• The power of tiny DSLs. ~ Jack Kelly. #Haskell #CodeWorld

04-Abr-20

• Verified functional programming in Agda. ~ Aaron Stump. #eBook #ITP #Agda
• El problema de Basilea. ~ Urtzi Buijs (@UrtziBuijs). #Matemáticas
• The Bates LaTeX Manual. #LaTeX

06-Abr-20

• Composition of functions cheatsheet. #Haskell #FunctionalProgramming
• Doing a math assignment with the Lean theorem prover. ~ Andrew Helwer (@ahelwer). #ITP #LeanProver #Math

07-Abr-20

• Replacing Jupyter with Orgmode. ~ Rohit Goswami (@rg0swami). #Emacs #OrgMode #Python

08-Abr-20

• Practical proof search for Coq by type inhabitation. ~ Lukasz Czajka. #ITP #Coq
• Haskell: Why monad composes operations sequentially. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
• Pointless style. ~ Chris Dornan (@CDornan). #Haskell #FunctionalProgramming
• Write unbreakable Python. ~ Jesse Warden (@jesterxl). #Python #FunctionalProgramming
• Functor (expanded). ~ Chris Dornan (@CDornan). #Haskell #FunctionalProgramming
• Introducing the #ProjectEuler100 challenge: the “dark souls” of coding achievements. ~ Quincy Larson (@ossia). #Programming #Math

09-Abr-20

• Maintaining a library of formal mathematics. ~ Floris van Doorn, Gabriel Ebner, Robert Y. Lewis. #ITP #LeanProver #Math

10-Abr-20

• Coursework: The power and limits of Logic. ~ Greg Restall (@consequently). #Logic
• Key benefits of working in Haskell. ~ Sreenidhi Nair (@ersran9). #Haskell #FunctionalProgramming
• A fast verified liveness analysis in SSA form. ~ Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie. #ITP #Coq
• Certifying certainty and uncertainty in approximate membership query structures. ~ Kiran Gopinathan, Ilya Sergey. #ITP #Coq

11-Abr-20

• The interplay between logic and computation. ~ Zena M. Ariola. #Logic #CompSci
• Understanding the power of LISP. ~ @josh_b_rad. #Lisp
• A comprehensive framework for saturation theorem proving. ~ Sophie Tourret. #ITP #IsabelleHOL #Logic
• Esencia del álgebra lineal. #Matemáticas

12-Abr-20

• Fundamentals of Artificial Intelligence. ~ K.R. Chowdhary. #AI #Logic
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL. ~ Sadegh Dalvandi, Brijesh Dongol, Simon Doherty. #ITP #IsabelleHOL
• Verifying the DPLL algorithm in Dafny. ~ Cezar-Constantin Andrici, Ştefan Ciobâcă. #Dafny #Verification
• Herramientas de razonamiento automático en GeoGebra: qué son y para qué sirven. ~ M. Pilar Vélez, Tomás Recio, Steven Van Vaerenbergh. #Razonamiento_automático #GeoGebra
• Functional Pearls: Heterogeneous binary random-access lists. ~ Wouter Swierstra. #Agda #FunctionalProgramming
• On beyond Prolog. ~ Anne Ogborn (@AnnieTheObscure). #Prolog #LogicProgramming
• Zipping trees. Part 1. ~ Joseph Morag. #Haskell #FunctionalProgramming
• Zipping trees. Part 2. ~ Joseph Morag. #Haskell #FunctionalProgramming

13-Abr-20

• Formalization of an algorithm for greedily computing associative aggregations on sliding windows. ~ Lukas Heimes, Dmitriy Traytel, Joshua Schneider. #ITP #IsabelleHOL
• Things software engineers trip up on when learning Haskell. ~ William Yao (@williamyaoh). #Haskell #FuncionalProgramming
• 10 minute Lean tutorial: proving logical propositions. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Logic
• Doglike programming book (Chicken jerky flavoured introduction to functional programming). ~ Juuso Vuorinen. #eBook #Haskell #FunctionalProgramming

14-Abr-20

• At the interface of algebra and statistics. ~ Tai-Danae Bradley. #PhD_Thesis #Math
• Haskell Wizards (Character illustrations of Haskell users). #Haskell #FunctionalProgramming
• Computable analysis and notions of continuity in Coq. ~ Florian Steinberg, Laurent Thery, Holger Thies. #ITP #Coq #Math
• Programming totally with head and tail. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming

16-Abr-20

• Prolog technology reinforcement learning prover. ~ Zsolt Zombori, Josef Urban, Chad E. Brown. #ATP #MachineLearning #Prolog
• Programming algorithms. ~ Vsevolod Domkin #eBook #CommonLisp #Programming #Algorithms
• Online seminar lists. #Math #CompSci
• Towards faster iteration in industrial Haskell. ~ Patrick Thomson (@importantshock). #Haskell #FunctionalProgramming

17-Abr-20

• Trakhtenbrot’s theorem in Coq, a constructive approach to finite model theory. ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Math
• The three kinds of Haskell exceptions and how to use them. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• Why Haskell matters. ~ Thomas Mahler. #Haskell #FunctionalProgramming

18-Abr-20

• Distilling the requirements of Gödel’s Incompleteness theorems with a proof assistant. ~ Andrei Popescu, Dmitriy Traytel. #ITP #IsabelleHOL #Logic #Math
• Towards a formal proof of the Cook-Levin theorem. ~ Lennard Gäher. #ITP #Coq #Logic #Math
• Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL. ~ René Thiemann et als. #ITP #IsabelleHOL

19-Abr-20

• What Is Haskell, who uses it, and where can you learn to code it. ~ Alexander Sechin. #Haskell #FunctionalProgramming
• The mechanization of Mathematics. ~ Jeremy Avigad. #ITP #Math
• The mechanization of Mathematics. ~ Jeremy Avigad. #ITP #Math
• Great moments in Haskell history. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
• Algebraically closed fields in Isabelle/HOL. ~ Paulo Emı́lio de Vilhena, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
• Introduction to relude an alternative Haskell prelude. ~ Dmitrii Kovanikov (@ChShersh). #Haskell #FunctionalProgramming

21-Abr-20

• Lucas’s theorem in Isabelle/HOL. ~ Chelsea Edmonds. #ITP #IsabelleHOL #Math
• Blazing fast Fibonacci numbers using Monoids. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming #Math
• Deep generation of Coq lemma names using elaborated terms. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq #MachineLearning

23-Abr-20

• Formal verification of flow equivalence in desynchronized designs. ~ Jennifer Paykin, Brian Huffman, Daniel M. Zimmerman, Peter A. Beerel. #ITP #Coq
• The Imandra automated reasoning system (system description). ~ Grant Olneya Passmore et als. #ITP
• Deriving isomorphically. ~ Hans Hoeglund. #Haskell #FunctionalProgramming

25-Abr-20

• When will computers prove theorems? ~ Kevin Buzzard. #ITP #Math

27-Abr-20

• Recursive functions. ~ Walter Dean. #Logic #Math
• Is HoTT the way to do mathematics? ~ Kevin Buzzard. #Math #HoTT #ITP

28-Abr-20

• El método Moore o cómo aprender matemáticas al estilo tejano. ~ Pedro Alegría. #Matemáticas
• Active Prelude to Calculus. ~ Matthew Boelkins. #Math
• Active Calculus 2.1. ~ Matthew Boelkins. #Math
• Active Calculus Multivariable: 2018 Edition. ~ Steve Schlicker, David Austin, Matt Boelkins. #Math
• Detecting fake news for the new coronavirus by reasoning on the Covid-19 ontology. ~ Adrian Groza. #ATP #Racer
• Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems. ~ Florian Kammüller. #ITP #IsabelleHOL
• Diagnosis in tennis serving technique. ~ Eugenio Roanes-Lozano et als. #KBS #CAS #GroebnerBases #Logic #Math #CompSci

29-Abr-20

• Scala book (Learn Scala fastwith small, easy lessons). ~ Alvin Alexander, et al. #eBook #Scala #FunctionalProgramming
• A simplified version of Bitcoin, implemented in Agda. ~ Guilherme Horta Alvares da Silva. #ITP #Agda #FunctionalProgramming
• Consider Haskell. ~ Gil Mizrahi (@_gilmi). #Haskell #FunctionalProgramming

30-Abr-20

• The Lambert W function on the reals. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Introduction to Artificial Intelligence. ~ Wolfgang Ertel. #eBook #Logic #AI
• Open Textbook Library: Open textbooks are textbooks that have been funded, published, and licensed to be freely used, adapted, and distributed. #eBooks
• Mathematical logic (On numbers, sets, structures, and symmetry). ~ Romana Kossak. #eBook #Logic #Math
• Philosophical and mathematical logic. ~ Harrie de Swart. #eBook #Logic #Math
• Foundations of programming languages. ~ Kent D. Lee. #eBook #Programming #CompSci
• The invisible map. ~ Kevin Buzzard (@XenaProject). #Logic #Math #ITP #Lean
• Proofs from THE BOOK. ~ Martin Aigner, Günter M. Ziegler #FreeEbook #Math

Marzo de 2020

01-Mar-20

• Programming with Miranda. ~ C. Clack, C. Myers, and E. Poon (1995). #eBook #Miranda #FunctionalProgramming
• Church’s thesis and functional programming. ~ David Turner (2006). #Logic #FunctionalProgramming #Miranda
• Some history of functional programming languages. ~ David Turner (2012). #FunctionalProgramming
• Postcondition-preserving fusion of postorder tree transformations. ~ Eleanor Davies, Sara Kalvala. #ITP #Coq
• A modern look at GRIN, an optimizing functional language back end. ~ Csaba Hruska, Péter Dávid Podlovics, Andor Pénzes. #Haskell #FunctionalProgramming
• Course: Approximation theory and proof assistants: certified computations. ~ Nicolas Brisebarre, Damien Pous./#coqsessions #ITP #Coq #Math
• First steps with Coq (for primary and secondary school teachers, APMEP, Grenoble, 2011). ~ Damien Pous. #ITP #Coq

02-Mar-20

• Optimizing a maze with graph theory, genetic algorithms, and Haskell. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming #Math
• Seventy-five problems for testing automatic theorem provers. ~ Francis Jeffry Pelletier (1986). #Logic
• How to get a Haskell job. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming

03-Mar-20

• Lisp code for the textbook “Paradigms of Artificial Intelligence Programming”. ~ Peter Norvig. #CommonLisp #AI
• Competitive programming in Haskell: modular arithmetic, part 2. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math

04-Mar-20

• Practical machine-checked formalization of change impact analysis. ~ Karl Palmskog, Ahmet Celik, Milos Gligoric. #ITP #Coq
• Declarative pearl: Deriving monadic quicksort. ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming
• Automated derivation of random generators for algebraic data types. ~ Agustín Mista. #Haskell #FunctionalProgramming
• Should your specification language be typed?. ~ Leslie Lamport, Lawrence C. Paulson (1999). #ITP #FunctionalProgramming
• The Prolog debugger and declarative programming. Examples. ~ Włodzimierz Drabent. #Prolog #LogicProgramming

05-Mar-20

• Scissors congruence (An interactive demonstration of the Wallace–Bolyai–Gerwien theorem). ~ Dima Smirnov, Zivvy Epstein. #Math
• Create blockchain in Haskell (Rolling your own blockchain in Haskell). ~ Michael Burge (2017). #Haskell #Blockchain
• Intuitionistic mathematics and logic. ~ Joan R. Moschovakis, Garyfallia Vafeiadou. #Logic #Math
• Code is engineering, types are science. ~ Juan Raphael Diaz Simões. #Programming #Logic
• Speak math, not code. (Writing algorithms in mathematics rather than code is not only more elegant but also more efficient, says 2013 Turing Award winner Leslie Lamport). #Math #Programming #CompSci

06-Mar-20

• Building a friendly and safe EDSL with IxState and TypeLits. #Haskell #FunctionalProgramming
• distributed-dataset: A distributed data processing framework in Haskell. ~ Utku Demir. #Haskell #FunctionalProgramming
• GHC Haskell Pats and LPats. ~ Shayne Fletcher. #Haskell #FunctionalProgramming
• Audience role in mathematical proof development. ~ Zoe Ashton. #Logic #Math #ITP

07-Mar-20

• Writing more modular code with lazy evaluation. ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming
• How does lazy evaluation work in Haskell? ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming via @etorreborre
• Declarative stream runtime verification (hLola). ~ Martı́n Ceresa, Felipe Gorostiaga, César Sánchez. #Haskell #FunctionalProgramming

08-Mar-20

• Idris 2: Quantitative Type Theory in action. ~ Edwin Brady. #Idris #FunctionalProgramming

09-Mar-20

• Naive synthesis of sorting networks using Z3Py. ~ Philip Zucker (@SandMouth). #SMT #Z3
• P =? NP. ~ Scott Aaronson (2002). #Logic #CompSci
• El Coronavirus y la leyenda del tablero de ajedrez. ~ Carlos Pena y Juan José Gómez Cadenas. #Matemáticas
• Les algorithmes du programme 2019 de mathématiques de Seconde. ~ Benjamin Clerc. #Math #Programming #Python
• Implémentations du problème du Duc de Toscane dans différents langages. ~ Guillaume Connan. #Math #Caml #Haskell #Scala #Python #Scilab
• Algorithmes de graphes. ~ Guillaume Connan (2019). #Math #SageMath #Pythom
• Au delà des réels: méthodes numériques en informatique. ~ Guillaume Connan (2016). #Math #Python
• Easily making CheatSheets with Org-mode. ~ Musa Al-hassy. #Emacs #OrgMode
• PythonCheatSheet: Quick reference to a tremendously accessible high-level language - executable pseudocode! ~ Musa Al-hassy. #Python #OrgMode

10-Mar-20

• Formal verification of cyber-physical systems using theorem proving. ~ Adnan Rashid, Umair Siddique, Sofine Tahar. #ITP #HOL4 #HOL_Light #IsabelleHOL #Coq #PVS
• Julia Snail: An Emacs development environment for Julia. #Emacs #JuliaLang
• Holmes: a library for computing constraint-solving problems. ~ Tom Harding. #Haskell #FunctionalProgramming

11-Mar-20

• Landmark Computer Science proof cascades through Physics and Math. ~ Kevin Hartnett (@KSHartnett). #CompSci #Physics #Math
• Hilbert’s tenth problem in Coq. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math
• Haskell with UTF-8. ~ Kirill Elagin. #Haskell #FunctionalProgramming
• Proofs, computability, undecidability, complexity, and the lambda calculus (An introduction). ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompsCi

12-Mar-20

• Mechanization of a type system for atomicity analysis and its type safety. ~ Beatriz Ferreira et als. #ITP #Coq

13-Mar-20

• #Exercitium: Soluciones de “Producto de Fibonaccis consecutivos”. #Haskell #ProgramaciónFuncional #Matemáticas #I1M2019
• #Exercitium: Enunciado de “Distancia esperada entre dos puntos de un cuadrado unitario”. #Haskell #ProgramaciónFuncional #Matemáticas #I1M2019

14-Mar-20

• Computational complexity and Brouwer’s continuum. ~ Robert L. Constable. #Logic #Math #ITP #Nuprl
• On proof complexity of resolution over polynomial calculus. ~ Erfan Khaniki. #Logic #Math #CompSci
• El problema aritmético de Sylvester. ~ Juan Arias de Reyna. #Matemáticas
• Ventajas del texto plano. #Emacs #OrgMode
• More natural deduction exercises. ~ Peter Smith. #Logic

15-Mar-20

• The hardest Math problem. ~ John Baez (@johncarlosbaez). #Math
• LISP comes of age. ~ Steven K. Roberts (1980). #Lisp #Programming #AI
• Todas las revistas Cacumen. #Matemáticas
• Matemáticas recreativas: ponga a prueba su destreza resolviendo enigmas históricos. ~ Fernando Blasco (@fblascoxyz). #Matemáticas

18-Mar-20

• FindFacts: a search application to find formal theory content of Isabelle and the AFP. ~ Fabian Huch./#about #ITP #IsabelleHOL #AFP
• The ideal mathematician. ~ Phillip J. David & Reuben Hersh (1981). #Math
• QED at large: A survey of engineering of formally verified software. ~ Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock. #ITP #FormalVerification
• The <- pure pattern. ~ Neil Mitchell (@ndm_haskell). #Haskell #FunctionalProgramming

20-Mar-20

• Verifying typeclasses with refinement types. ~ Yiyun Liu, James Parker, Michael Hicks, Niki Vazou. #Haskell #LiquidHaskell
• Can computers ever replace the classroom? ~ Alex Beard. #IA #Teaching

21-Mar-20

• seL4 in Australia: From research to real-world trustworthy systems. ~ Gernot Heiser, Gerwin Klein, June Andronick. #ITP #IsabelleHOL
• El Mundo de las Matemáticas de Mathigon. ~ @Alvy. #Matemáticas
• World of Mathematics. #Math

22-Mar-20

• Need a logic course, fast? ~ Richard Zach (@RrrichardZach). #Logic

23-Mar-20

• Nix for Coq development. ~ Yann Herklotz (@ymherklotz). #ITP #Coq #Nix
• Gröbner bases and their applications. ~ Mateusz Paprocki. #Math #Python
• Tactic learning and proving for the Coq proof assistant. ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning
• Towards formally verified smart contracts with Haskell. ~ Allison Irvin, Nick Waywood. #Haskell #FunctionalProgramming
• “Hello World!” in Isabell/HOL (including a formal framework for reasoning about IO). ~ Cornelius Diekmann and Lars Hupel. #ITP #IsabelleHOL #Monads

24-Mar-20

• Blaze: Lightweight HTML generation. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
• Data structure challenge: finding the rightmost empty slot. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Infinite patterns. ~ Cristóbal Vila. #Maths

26-Mar-20

• A formalization of SQL with nulls. ~ Wilmer Ricciotti, James Cheney. #ITP #Coq
• Taichi: A brand new programming language, “Frozen” in 99 lines of code. #Programming
• The problem with adding functions to compact regions. ~ Ömer Sinan Ağacan. #Haskell #FunctionalProgramming
• An under-approximate relational logic in Isabelle/HOL. ~ Toby Murray. #ITP #IsabelleHOL

27-Mar-20

• Furstenberg’s topology and his proof of the infinitude of primes in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Applying the Isabelle Insider framework to airplane security. ~ Florian Kammüller, Manfred Kerber. #ITP #IsabelleHOL
• Building a web app with functional programming - Haskell - part I. ~ Iori Matsuhara (@Matsumonkie). #Haskell #FunctionalProgramming
• Zipping Trees, Part 1. ~ Joseph Morag. #Haskell #FunctionalProgramming

28-Mar-20

• A trustful monad for axiomatic reasoning with probability and nondeterminism. ~ Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. #ITP #Coq
• Logic-based technologies for intelligent systems: State of the art and perspectives. ~ Roberta Calegari, Giovanni Ciatto, Enrico Denti, Andrea Omicini. #Logic #AI
• Dual and axiomatic systems for constructive S4, a formally verified equivalence. ~ Lourdes del Carmen González HuescaFavio, E. Miranda-Perea, P. Selene Linares-Arévalo. #ITP #Coq

31-Mar-20

• A starter template for SWI-Prolog projects. ~ Alex Kelley. #Prolog #LogicProgramming
• Some coding guidelines for Prolog. ~ Michael A. Covington (2002). #Prolog #LogicProgramming
• A repository for writing a Thesis with Org Mode. #Emacs #OrgMode
• Programming algorithms: Synchronization. ~ Vsevolod Dyomkin. #CommonLisp
• Lucid: Another HTML option. ~ James Bowen (@james_OWA). #Haskell #FuncionalProgramming
• Thinking mathematically notes. ~ A. Máté. #Logic #Math

Febrero de 2020

01-Feb-20

• A certifying extraction with time bounds from Coq to call-by-value λ-calculus. ~ Yannick Forster, Fabian Kunze. #ITP #Coq
• The weak call-by-value λ-calculus is reasonable for both time and space. ~ Yannick Forster, Fabian Kunze, Marc Roth. #ITP #Coq
• Verified programming of Turing machines in Coq. ~ Yannick Forster, Fabian Kunze, Maximilian Wuttke. #ITP #Coq
• Computational type theory and interactive theorem proving with Coq (Version of August 2, 2019). ~ Gert Smolka. #eBook #ITP #Coq #Logic
• Towards a readable formalisation of category theory. ~ Greg O’Keefe. #ITP #IsabelleHOL #CategoryTheory
• A hierarchy of algebras for boolean subsets. ~ Walter Guttmann, Bernhard Möller. #ITP #IsabelleHOL #Math
• Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL. ~ Albert Rizaldi. #PhD_Thesis #ITP #IsabelleHOL
• Ulam spirals. ~ Ken T Takusagawa. #Haskell #FunctionalProgramming
• Karp’s 21 NP-complete problems. #CompSci
• NP-completeness, part I. ~ Kevin Buchin. #CompSci
• NP-completeness, part II. ~ Kevin Buchin. #CompSci

02-Feb-20

• Completeness theorems for first-order logic analysed in constructive type theory. ~ Yannick Forster, Dominik Kirst, Dominik Wehr. #ITP #Coq #Logic
• Hilbert’s tenth problem in Coq. ~ Dominique Larchey-Wendling, Yannick Forster. #ITP #Coq #Math
• Beyond notations: Hygienic macro expansion for theorem proving languages. ~ Sebastian Ullrich, Leonardo de Moura. #ITP #LeanProver
• MOIN: A nested sequent theorem prover for intuitionistic modal logics (system description). ~ Marianna Girlando, Lutz Straßburger. #ATP #Prolog #Logic

03-Feb-20

• A formal development cycle for security engineering in Isabelle. ~ Florian Kammüller. #ITP #IsabelleHOL
• Automated proof of Bell-LaPadula security properties. ~ Maximiliano Cristiá, Gianfranco Rossi. #ATP #SetLog
• List of open and free logic textbooks. ~ Richard Zach (@RrrichardZach). #Logic
• Intro to Kaleidoscopes: Optics for aggregating data through Applicatives. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
• Nix: Functional package management! ~ James Bowen (@james_OWA). #Nix

04-Feb-20

• A comprehensive framework for saturation theorem proving (Technical report). ~ Uwe Waldmann, Sophie Tourret, Simon Robillard, Jasmin Blanchette. #ITP #IsabelleHOL #Logic
• jsCoq: A port of Coq to Javascript (Run Coq in your browser). ~ Emilio Jesús Gallego Arias (@ejgallego). #ITP #Coq
• Why monad composes operations sequentially. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
• Los primos de la conjetura de Collatz. ~ Francisco R. Villatoro (@emulenews). #Matemáticas
• Free and open-source textbooks. ~ Dana C. Ernst. #eBooks #Math
• How I created my website with Org mode. ~ John Borwick (@borwick). #Emacs #OrgMode

05-Feb-20

• VERONICA: Expressive and precise concurrent information flow security (Extended version with technical appendices). ~ Daniel Schoepe, Toby Murray, Andrei Sabelfeld. #ITP #IsabelleHOL
• A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Math
• Trakhtenbrot’s theorem in Coq (A constructive approach to finite model theory). ~ Dominik Kirst, Dominique Larchey-Wendling. #ITP #Coq #Logic
• ZZ (drunk octopus) is a modern formally provable dialect of C, inspired by Rust. ~ Arvid E. Picciani. #ZZ #Programming #SMT #FormalVerification
• Java & Haskell: Similarities and differences. ~ Dervis Mansuroglu (@dervis_m). #Java #Haskell
• Proofs, computability, complexity, and the lambda calculus (An introduction). ~ Jean Gallier, Jocelyn Quaintance. #eBook #Logic #CompSci #LambdaCalculus
• An algorithms course with minimal prerequisites. ~ Adam Sheffer. #Algorithms

06-Feb-20

• Computer-supported analysis of arguments in climate engineering. ~ David Fuenmayor, Christoph Benzmüller. #ITP #IsabelleHOL.
• Implementing and certifying a Web server in Coq. ~ Thomas Letan. #ITP #Coq
• Finkel: Haskell in S-expression. #Haskell #Lisp #Finkel_lang
• Safe memory management in inline-java using linear types. ~ Facundo Dominguez. #Haskell #FunctionalProgramming
• Functional or combinator parsing. ~ Graham Hutton (@haskellhutt). #Haskell #FunctionalProgramming
• Learning algorithmic techniques: dynamic programming. ~ Eric P. Hanson. #Algorithms #Programming #JuliaLang

07-Feb-20

• Toward a mechanized compendium of gradual typing. ~ Jeremy G. Siek. #ITP #Agda
• Introduction to univalent foundations of mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #Math
• Formalizing functional analysis structures in dependent type theory. ~ Reynald Affeldt et als. #ITP #Coq #Math
• A formal verification framework for security issues of blockchain smart contracts. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Blockchain
• Lorentz: Implementing smart contract eDSL in Haskell. ~ Kostya Ivanov. #Haskell #FunctionalProgramming

08-Feb-20

• Thinking in types. ~ Pat Brisbin. #Haskell #FunctionalProgramming
• Functional programming: The simple version. ~ Muhammad Tabaza. #Haskell #FunctionalProgramming
• Advanced Functional Programming concepts made easy. ~ Tal Joffe. #FunctionalProgramming #JavaScript
• Competitive Programming in Haskell: primes and factoring. ~ Brent Yorgey. #Haskell #FunctionalProgramming

09-Feb-20

• Type classes and filters for mathematical analysis in Isabelle/HOL. ~ Johannes Hölzl, Fabian Immler, Brian Huffman. #ITP #IsabelleHOL #Math
• Lean is better for proper maths than all the other theorem provers. ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Where is the fashionable mathematics? ~ Kevin Buzzard (@XenaProject). #Math #ITP #LeanProver #Coq #IsabelleHOL
• An experimental study of formula embeddings for automated theorem proving in first-order logic. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning
• Automated reasoning I. ~ Uwe Waldmann. #eBook #ATP #Logic
• Automated reasoning II. ~ Sophie Tourret, Uwe Waldmann. #eBook #ATP #Logic
• Verificación de estructura de redes neuronales profundas en tiempo de compilación (Proyecto TensorSafe). ~ Leonardo Piñeyro. #Haskell #DeepLearning
• MateFun: Functional Programming and Math with adolescents. ~ Alejandra Carboni et als. #Haskell #FunctionalProgramming #Math
• Mejoras al intérprete MateFun. ~ Nicolás Vázquez. #Haskell #FunctionalProgramming #Math
• Template Haskell tutorial. ~ Mark Karpov (@mrkkrp). #Haskell #FunctionalProgramming
• Imperative Haskell. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming
• Typeable and Data in Haskell. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming

10-Feb-20

• Arithmetic progressions and relative primes. ~ José Manuel Rodríguez Caballero. #ITP #IsabelleHOL #Math
• Tutoriel: types de données, fonctions et preuves en Isabelle. ~ Frédéric Boulanger. #ITP #IsabelleHOL
• Cours: Sémantique des langages. ~ Frédéric Boulanger. #ITP #IsabelleHOL
• How small can we make a useful type theory? ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming
• Coquedille: A Coq to Cedille transpiler written in Coq. ~ Pedro Abreu (@etapedro). #ITP #Coq #Cedille #FunctionalProgramming
• How laziness works. #Haskell #FunctionalProgramming
• An introduction to recursion schemes. ~ Patrick Thomson. #Haskell #FunctionalProgramming
• Counterexamples of type classes. ~ Phil Freeman. #Haskell #Purescript #FunctionalProgramming
• Compiling Haskell to JavaScript, not in the way you’d expect. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming #JavaScript

11-Feb-20

• Converting Cabal to Nix! ~ James Bowen (@james_OWA). #Haskell #Cabal #Nix
• Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ Niki Vazou (@nikivazou). #Haskell
• State will do. ~ Willem Seynaeve, Koen Pauwels and Tom Schrijvers. #Haskell #FunctionalProgramming
• PaSe: An extensible and inspectable DSL for micro-animations. ~ Ruben P. Pieters and Tom Schrijvers. #Haskell #FunctionalProgramming
• Physics, History and Haskell. (Interview with Rinat Stryungis). ~ Denis Oleynikov. #Haskell #FunctionalProgramming

12-Feb-20

• A DSL for fluorescence microscopy. Birthe van den Berg, Peter Dedecker, Tom Schrijvers. #Haskell #FunctionalProgramming
• A proof assistant based formalisation of core Erlang. ~ Péter Bereczky, Dániel Horpácsi and Simon Thompson. #ITP #Coq #Erlang
• An equational modeling of asynchronous concurrent programming. ~ David Janin. #Haskell #FunctionalProgramming
• BinderAnn: Automated reification of source annotations for monadic EDSLs. ~ Agustín Mista and Alejandro Russo. #Haskell #FunctionalProgramming
• Formalization of cost and utility in Microeconomics. ~ Asad Ahmed, Osman Hasan, Falah Awwad, and Nabil Bastaki. #ITP HOL_Light
• Haskell in production: Riskbook (an interview with Jezen Thomas). ~ Gints Dreimanis. #Haskell #FunctionalProgramming
• Generalized Algebraic Data Types and Data Kinds. ~ Andre Popovitch (@PopovitchAndre). #Haskell #FunctionalProgramming
• Utilización de registros en Emacs. #Emacs

13-Feb-20

• Generating next step hints for task oriented programs using symbolic execution. ~ Nico Naus and Tim Steenvoorden. #Haskell #FunctionalProgramming
• Mac Lane’s comparison theorem for the Kleisli construction formalized in Coq. ~ Burak Ekici, and Cezary Kaliszyk. #ITP #Coq
• Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming
• Practical Common Lisp. ~ Peter Seibel. #eBook #CommonLisp

15-Feb-20

• Maintainable software architecture in Haskell (with Polysemy). ~ Paweł Szulc (@EncodePanda). #Haskell #FunctionalProgramming
• The Logic course adventure (An active learning textbook for formal logic). ~ Ian Schnee. #eBook #Logic
• Awesome Coq Awesome (A curated list of awesome Coq libraries, plugins, tools, and resources). #ITP #Coq
• Equality of functions in Agda. ~ Mark Armstrong. #ITP #Agda #FunctionalProgramming via @armk_eh

16-Feb-20

• Equality in mechanized mathematics. ~ Ramkumar Ramachandra. #ITP #Coq #Math
• Porting to Rio. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
• Competitive programming in Haskell: modular arithmetic, part 1. ~ Brent Yorgey. #Haskell #FunctionalProgramming #Math
• There and Back Again (TABA). ~ Olivier Danvy, and Mayer Goldberg. #Programming #Algoritms
• Typing TABA (There and Back Again). ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
• Profunctor optics, a categorical update. ~ Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Román. #Haskell #FunctionalProgramming
• How to start using Python type annotations with Mypy. ~ Carlos Villavicencio. #Python #Mypy
• Teaching natural deduction as a subversive activity. ~ James Caldwell. #Logic

17-Feb-20

• Certifications of programs with computational effects. ~ Burak Ekici. #PhD_Thesis #ITP #Coq
• Certification of nonclausal connection tableaux proofs. ~ Michael Färber, and Cezary Kaliszyk. #ITP #HOL_Light
• Flexible coinduction in Agda. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda
• What I wish I knew when learning Haskell (Version 2.5). ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
• Categorical combinators for Graphviz in Python. ~ Philip Zucker (@SandMouth). #Python
• How to make mondrian art in Haskell (Unleash your inner functional artist). ~ Marc Fichtel (@mc_razzy). #Haskell #FunctionalProgramming

18-Feb-20

• 3 tribes of programming. ~ Joseph Gentle (@josephgentle). #Programming
• Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi. ~ Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. #ITP #Coq
• Signatures and induction principles for higher inductive-inductive types. ~ Ambrus Kaposi, and András Kovács. #ITP #Agda #Haskell #FunctionalProgramming
• From Curry to Haskell. ~ Felice Cardone. #Haskell #FunctionalProgramming #Logic
• A Why3 proof of GMP algorithms. ~ Raphaël Rieu-Helft. #Why3 #FormalVerification
• mCoq: Mutation analysis for Coq verification projects. ~ Kush Jain et als. #ITP #Coq

19-Feb-20

• Most popular programming languages 1965-2019. #Programming
• Programming algorithms: Compression. ~ Vsevolod Dyomkin. #Algorithms #CommonLisp
• On linear types and exceptions. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• A Lisp programmer living in Python-land: The Hy programming language. ~ Mark Watson. #eBook #Programing #Lisp #Python #Hy

20-Feb-20

• [[https://svhol.pbmichel.com/][Isabelle/HOL and Proof General reference [Isabelle/HOL support wiki]]]. #ITP #IsabelleHOL
• Agda vs. Coq vs. Idris. #ITP #Agda #Coq #Idris

21-Feb-20

• Type witnesses in Haskell. ~ Sandeep Chandrika. #Haskell #FunctionalProgramming
• “Papers we love” is a repository of academic computer science papers and a community who loves reading them. @papers_we_love #CompSci
• Papers from the computer science community to read and discuss. #CompSci
• Scheme: An interpreter for extended lambda calculus (1975). ~ Gerald J. Sussman, and Guy L. Steele. #Programming #Scheme #CompSci
• What is a knowledge representation?. ~ Randall Davis, Howard Shrobe, and Peter Szolovits (1993). #KR #AI
• An axiomatic basis for computer programming. ~ C.A.R. Hoare (1969). #CompSci
• Why functional programming matters. ~ John Hughes (1989). #FunctionalProgramming #CompSci
• A tutorial on the universality and expressiveness of fold. ~ Graham Hutton (1999). #FunctionalProgramming #Haskell
• QuickCheck: Α lightweight tool for random testing of Haskell programs. ~ Koen Claessen and John Hughes (2000). #Haskell #FunctionalProgramming
• Computational lambda-calculus and monads. ~ Eugenio Moggi (1988). #CompSci
• Infinite sets that admit fast exhaustive search. ~ Martı́n Escardó (2007). #Haskell #FunctionalProgramming
• Monoids: Theme and variations (Functional Pearl). ~ Brent A. Yorgey (2012). #Haskell #FunctionalProgramming
• QuickCheck testing for fun and profit. ~ John Hughes (2007). #Haskell #FunctionalProgramming
• The mechanical evaluation of expressions. ~ P.J. Landin (1964). #CompSci
• On computable numbers, with an application to the Entscheidungsproblem. ~ A.M. Turing (1937). #CompSci #Math
• Propositions as types. ~ Philip Wadler (2014). #Logic #CompSci
• Recursive functions of symbolic expressions and their computation by machine, Part I. ~ John McCarthy (1960). #CompSci #Lisp
• Fundamental concepts in programming languages. ~ Christopher Strachey (2000). #CompSci

22-Feb-20

• Graph theory in Coq: Minors, treewidth, and isomorphisms. ~ Christian Doczkal and Damien Pous. #ITP #Coq #Math
• Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. ~ Christian Doczkal, and Damien Pous. #ITP #Coq #Math
• Pensamientos de Antonio Machado. ~ Guiomar Godoy. #Filosofía
• A selected bibliography on formalised mathematics. ~ Laurent Théry. #ITP #Math
• A machine-checked constructive metatheory of computation tree logic. ~ Christian Doczkal (2016). #PhD_Thesis #ITP #Coq #Logic
• Course: Machine-checked Mathematics. ~ Assia Mahboubi. #ITP #Coq #Math

23-Feb-20

• On memory addressing. ~ Reto Achermann. #PhD_Thesis #ITP #IsabelleHOL
• Experiences from exporting major proof assistant libraries. ~ Michael Kohlhase, and Florian Rabe. #ITP #Coq #HOL_Light #IsabelleHOL #Mizar #PVS #MMT
• Flexible coinduction in Agda. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda
• Various new theorems in constructive univalent mathematics written in Agda. ~ Martín Escardó. #ITP #Agda #Math
• The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. ~ Martı́n Escardó. #ITP #Agda #Math
• Translation from FOL to LTL+Past and LTL, via separation of LTL+Past. ~ Daniel Oliveira. #Logic #Haskell #FunctionalProgramming
• Linear temporal logic: separation and translation. ~ Daniel Oliveira. #MSc_Thesis #Logic #Haskell #FunctionalProgramming
• Revisiting separation: Algorithms and complexity. ~ Daniel Oliveira, and João Rasga. #Logic #Haskell #FunctionalProgramming
• Sobre listas y atoms. #Emacs #Elisp

24-Feb-20

• Isabelle/Spartan: A dependent type theory framework for Isabelle. ~ Joshua Chen. #ITP #IsabellleHOL #HoTT
• Implementing the Goodstein function in λ-calculus. ~ Bertram Felgenhauer. #ITP #IsabelleHOL
• Testing higher-order properties with QuickCheck. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming #QuickCheck
• Another breadth-first traversal. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
• Lectures on scientific computing with Python. ~ Robert Johansson (2017). #Python
• Machine Learning in Python: Main developments and technology trends in data science, machine learning, and artificial intelligence. ~ Sebastian Raschka, Joshua Patterson, Corey Nolet. #MachineLearning #AI #Python
• Category theory as a tool for thought. ~ Daniel Beskin. #CategoryTheory #FunctionalProgramming #Haskell
• The scientific paper is outdated (For the sake of research, their careers, and their mental health, scientists should spend more time developing software). ~ Ryan Abernathey. #

25-Feb-20

• A mechanised semantics for HOL with ad-hoc overloading. ~ Johannes Åman Pohjola, Arve Gengelbach. #ITP #HOL4

26-Feb-20

• A generic framework for verified compilers in Isabelle/HOL. ~ Martin Desharnais. #ITP #IsabelleHOL
• An analysis of programming paradigms in high-level synthesis tools. ~ Pieter Staal. #Haskell #FunctionalProgramming
• Marlowe: implementing and analysing financial contracts on blockchain. ~ Pablo Lamela Seijas et als. #Haskell #ITP #IsabelleHOL #Blockchain #Cardano
• A machine-checked C implementation of Dijkstra’s shortest path algorithm. ~ Anshuman Mohan, Shengyi Wang, and Aquinas Hobor. #ITP #Coq
• Formal verification of hardware components in critical systems. ~ Wilayat Khan et als. #ITP #Coq
• MMT: The Meta Meta Tool (system description). ~ Florian Rabe. #ITP #MMT
• Type-based formal verification. ~ Alejandro Serrano (@trupill). #Haskell #Verification
• Probabilistic programming with monad‑bayes, Part 3: A bayesian neural network. ~ Siddharth Bhat, Simeon Carstens, Matthias Meschede. #Haskell #FunctionalProgramming

27-Feb-20

• Short proof of Menger’s theorem in Coq (Proof Pearl). ~ Christian Doczka. #ITP #Coq #Math

28-Feb-20

• Proof-reconstruction in type theory for propositional logic. ~ Jonathan Prieto-Cubides, Andrés Sicard-Ramírez. #ITP #Agda #Metis #Logic
• Athena: a tool that translates Metis ATP proofs to the Agda programming language to check their correctness. ~ Jonathan Prieto-Cubides. #Haskell #ITP #Agda #Metis #Logic
• agda-prop: A library for classical propositional logic in Agda. ~ Jonathan Prieto-Cubides. #ITP #Agda #Logic
• agda-metis: Metis prover reasoning for propositional logic in Agda. ~ Jonathan Prieto-Cubides. #ITP #Agda #Metis
• The natural deduction pack. ~ Alastair Carr. #Logic
• Highly automated formal proofs over memory usage of assembly code. ~ Freek Verbeek et als. #ITP #IsabelleHOL
• Math is your insurance policy. ~ Bartosz Milewski (@BartoszMilewski). #Programming
• Automating the generation of high school geometry proofs using Prolog in an educational context. ~ Ludovic Font et als. #Prolog #LogicProgramming #Math
• A mobile application for self-guided study of formal reasoning. ~ David M. Cerna, Rafael P.D. Kiesel, Alexandra Dzhiganskaya. #Logic #Teaching #Android
• Tools in term rewriting for education. ~ Sarah Winkler, Aart Middeldorp. #Logic #Teaching

29-Feb-20

• Teaching a formalized logical calculus. ~ Asta Halkjær From et als. #Logic #Teaching #ITP #IsabelleHOL
• Structure and interpretation of computer programs — JavaScript adaptation. #eBook #JavaScript #SICP
• Mathematical structures. ~ Contributors of math.chapman.edu. #Math
• Reductions and jokes. ~ R.J. Lipton & K.W. Regan. #CompSci #Math
• Mathematical humor. ~ Andrej and Elena Cherkaev. #Math

Enero de 2020

01-Ene-20

• Introduction to HOL4 theorem prover. ~ K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4
• Design and verification of parity checking circuit using HOL4 theorem proving. ~ E. Deni̇z, K. Aksoy, S. Tahar, Y. Zeren. #ITP #HOL4
• Proof searching in HOL4 with genetic algorithm. ~ M.Z. Nawaz et als #ITP #HOL4

02-Ene-20

• Defunctionalization: Everybody does it, nobody talks about it. ~ James Koppel. #FunctionalProgramming #Haskell
• Constructive reverse mathematics. ~ Hannes Diener. #Logic #Math
• Formalizing modal logic in HOL. ~ Yiming Xu. #PhD_Thesis #ITP #HOL #Logic

03-Ene-20

• On correctness of an n queens program. ~ Włodzimierz Drabent. #LogicProgramming #Prolog #Verification
• The simple Haskell initiative. #Haskell #FunctionalProgramming
• A computer made from DNA can compute the square root of 900. #CompSci
• Learn Haskell now! ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming

04-Ene-20

• Lean versus Coq: The cultural chasm. ~ Ramkumar Ramachandra. #ITP #LeanProver #Coq

05-Ene-20

• Type-level rewrite rules. ~ Samuel Gélineau. #Haskell #FunctionalProgramming
• Mandelbrot & Lovejoy’s rain fractals. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming
• Kind inference for datatypes. ~ N. Xie, R.A. Eisenberg, B.C.d.S. Oliveira. #Haskell #FunctionalProgramming

06-Ene-20

• Organizing our package! ~ James Bowen (@james_OWA). #Haskell #Cabal #FunctionalProgramming

07-Ene-20

• Formalizing a Seligman-style tableau system for hybrid logic in Isabelle/HOL. ~ Asta Halkjær. #ITP #IsabelleHOL #Logic
• Different problems, common threads: Computing the difficulty of mathematical problems. ~ Karen Lange. #Math #CompSci
• Estimating the proportion of smooth numbers. ~ John D. Cook (@JohnDCook). #Math #Programming #Python
• Lean 3 for hackers. ~ J Kenneth King. #LeanProver #FunctionalProgramming

08-Ene-20

• Haskell language extension taxonomy. ~ Doug Beardsley. #Haskell #FunctionalProgramming

09-Ene-20

• A formal proof of the irrationality of ζ(3). ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math
• Proof pearl: Braun trees. ~ T. Nipkow, T. Sewell. #ITP #Isabelle

10-Ene-20

• Gauss sums and the Pólya–Vinogradov inequality. ~ R. Raya, M. Eberl. #ITP #IsabellleHOL #Math
• Bicategories in Isabelle/HO: ~ Eugene W. Stark. #ITP #IsabelleHOL
• The irrationality of ζ(3) in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabellleHOL #Math
• Skip lists in Isabelle/HOL. ~ M.W. Haslbeck, M. Eberl. #ITP #IsabelleHOL
• Motivated proofs: what they are, why they matter and how to write them. ~ Rebecca Lea Morris. #Math
• Programming with categories. ~ Peter Smith. #Programming #CategoryTheory
• Generating small binaries in Haskell. ~ Alex Dixon (@dixonary_). #Haskell #FunctionalProgramming
• Collections of papers and books about Haskell, type theory and category theory. ~ Saurabh Kukade. #Haskell #TypeTheory #CategoryTheory

11-Ene-20

• LF+ in Coq for “fast and loose” reasoning. ~ F. Alessi. #ITP #Coq
• Selective applicative functors & probabilities. ~ Armando Santos (@_bolt12). #MSc_Thesis #Haskell #FunctionalProgramming #Math
• Linear algebra of programming - Algebraic matrices in Haskell. ~ Armando Santos (@_bolt12). #FunctionalProgramming #Math
• Gain confidence with Haskell! ~ Brandon Chinn. #Haskell #FunctionalProgramming

12-Ene-20

• Programming algorithms: approximation. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms
• The road to proficient Haskell. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
• Teach yourself Logic 2020: A study guide. ~ Peter Smith. #Logic
• Rusty Razor is a tool for constructing finite models for first-order theories. ~ Salman Saghafi. #Logic
• A framework for exploring finite models. ~ Salman Saghafi. #PhD_Thesis #Logic #Haskell

13-Ene-20

• Computer Science as the continuation of Logic by other means. ~ Georg Gottlob. #Logic #CompSci #WorldLogicDay
• Mathematical Logic in Computer Science. ~ Assaf Kfoury. #Logic #CompSci #WorldLogicDay
• On the unusual effectiveness of Logic in Computer Science. ~ J.Y. Halpern et als. #Logic #CompSci #WorldLogicDay
• Computer Science and Logic (a match made in heaven). ~ Luca Aceto. #Logic #CompSci #WorldLogicDay
• The story of Logic. ~ Robert L. Constable. #Logic #CompSci #WorldLogicDay
• History of interactive theorem .proving. ~ J. Harrison, J. Urban, F. Wiedijk. #ITP #Logic #CompSci #WorldLogicDay
• Automated reasoning: From bold dreams to Computer Science methodology. ~ Robert L. Constable. #ATP #CompSci #WorldLogicDay
• Can the computer really help us to prove theorems? ~ Herman Geuvers. #ITP #Logic #CompSci #WorldLogicDay

14-Ene-20

• TAUT: A website that contains randomly-generated, self-correcting logic excercises. ~ Ariel Roffé. #Logic
• TAUT: el software desarrollado por un filósofo del CONICET para enseñar Lógica. #Lógica #WorldLogicDay
• Randomly generated and self-correcting logic exercises site. ~ Justin Weinberg. #Logic #WorldLogicDay
• Adjunctions in the wild: foldl. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
• Computer-supported exploration of a categorical axiomatization of modeloids. ~ L. Tiemens, D.S. Scott, C. Benzmüller, M. Benda. #ITP #IsabelleHOL #Math
• Computer-supported analysis of positive properties, ultrafilters and modal collapse in variants of Gödel’s ontological argument. ~ C. Benzmüller, D. Fuenmayor. #ITP #IsabelleHOL #Logic
• A verified packrat parser interpreter for parsing expression grammars. ~ C. Blaudeau, N. Shankar. #ITP #PVS
• Using Cabal on its own. ~ James Bowen (@james_OWA). #Haskell #Cabal
• Common stanzas. ~ Veronika Romashkina (@vronnie911). #Haskell #Cabal

15-Ene-20

• Closest pair of points algorithms. ~ M. Rau, T. Nipkow. #ITP #IsabelleHOL
• Automatic generation and verification of test-stable floating-point code. ~ L. Titolo, M. Moscato, C.A. Muñoz. #ITP #PVS
• The space of mathematical software systems. ~ J. Carette, W.M. Farmer, Y. Sharoda. #ATP #ITP #Math #CompSci
• A mechanized formalization of the WebAssembly specification in Coq. ~ X. Huang. #ITP #Coq
• Is Haskell a category? ~ B. Fong, B. Milewski, D. Spivak. #Haskell #FunctionalProgramming #CategoryTheory

16-Ene-20

• Your students could have invented … the Pythagorean theorem. ~ Chris Smith (@cdsmithus). #Math #Teaching
• Programming with categories (Draft). ~ B. Fong, B. Milewski, D.I. Spivak. #FunctionalProgramming #Haskell #CategoryTheory
• Verified approximation algorithms in Isabelle/HOL. ~ R. Eßmann, T. Nipkow, S. Robillard. #ITP #IsabelleHOL
• La magia del orden (de los datos). ~ Alejandro Serrano (@trupill). #Algoritmos
• A tale of two functors (or: how I learned to stop worrying and love Data and Control). ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
• Talks from the formal methods in Mathematics / Lean together 2020 workshop. #ITP #LeanProver #IsabelleHOL #Coq

17-Ene-20

• Generating mathematical structure hierarchies using Coq-ELPI. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math
• High level commands to declare a hierarchy based on packed classes. ~ C. Cohen, K. Sakaguchi, E. Tassi. #ITP #Coq #Math
• On a mathematician’s attempts to formalize his own research in proof assistants. ~ Sébastien Gouëzel. #ITP #IsabelleHOL #LeanProver #Math
• Automating asymptotics in a theorem prover. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Using Lean for new research. ~ Neil Strickland. #ITP #LeanProver #Math
• Iterated chromatic localisation. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math
• Lean code formalising many of the proofs from the paper “Iterated chromatic localisation”. ~ Neil Strickland, Nicola Bellumat. #ITP #LeanProver #Math
• Proof in Lean that there are infinitely many primes. ~ Neil Strickland. #ITP #LeanProver #Math
• Reasoning with non-linear formulas in Isabelle/HOL. ~ Wenda Li. #ITP #IsabelleHOL #Math
• ODEs and the Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math
• Julia programming’s dramatic rise in HPC and elsewhere. ~ John Russell. #JuliaLang
• Complex geometry in Isabelle/HOL. ~ F. Marić, D. Simić. #ITP #IsabelleHOL #Math

18-Ene-20

• Poincaré disc model in Isabelle/HOL. ~ D. Simić, F. Marić, P. Boutry. #ITP #IsabelleHOL #Math
• Static types are dangerously interesting. ~ Alex Nixon (@alexnixon_uk). #Haskell #FunctionalProgramming
• Digging into Lenses. ~ Josh Kuhn (@deontologician). #Haskell #FunctionalProgramming
• Formalizing a sophisticated definition. ~ Patrick Massot, Kevin Buzzard, Johan Commelin. #ITP #LeanProver #Math

19-Ene-20

• A Coq formalization of Lebesgue integration of nonnegative functions. ~ Sylvie Boldo et als. #ITP #Coq #Math
• First-order theorem (dis)proving for reachability problems in verification and experimental mathematics. ~ Alexei Lisitsa. #ATP #Prover9 #Mace4 #Math
• SMTCoq: Coq automation and its application to formal mathematics. ~ Chantal Keller. #ITP #Coq #SMT #Math
• Metamath Zero (or: how to verify a verifier). ~ Mario Carneiro. #ITP #MetamathZero
• Lisping at JPL. ~ Ron Garret. #Programming #CommonLisp
• Números primos que son imágenes. ~ @Alvy #Matemáticas
• swMATH: an information service for mathematical software. #Math #CompSci
• The Encyclopedia of Mathematics wiki is an open access resource designed specifically for the mathematics community. #Math
• Theorem prover. ~ Encyclopedia of Mathematics. #ATP #ITP #Math
• NIST digital library of mathematical functions. #Math
• The On-Line Encyclopedia of Integer Sequences (OEIS). #Math
• A modern perspective on type theory: From its origins until today. ~ Fairouz Kamareddine, Twan Laan, and Rob Nederpelt. #eBook #TypeTheory

20-Ene-20

• The future of Mathematics? ~ Kevin Buzzard. #Math #ITP
• Formal specification of a security framework for smart contracts. ~ M. Mandrykin et als. #ITP #IsabelleHOL
• Tabled typeclass resolution. ~ D. Selsam, S. Ullrich, L. de Moura. #ITP #LeanProver
• Mersenne primes and the Lucas–Lehmer test in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Nicer package organization with Stack! ~ James Bowen (@james_OWA). #Haskell #Stack
• A small matter of programming. ~ Jeremy Gibbons. #AI #Programming

21-Ene-20

• Adding online exercises with automated grading to any logic course with Carnap. ~ Richard Zach (@RrrichardZach). #Logic #Teaching
• Three equivalent ordinal notation systems in cubical Agda. ~ Fredrick Nordvall Forsberg. #ITP #Agda #Math
• Undecidability of higher-order unification formalised in Coq. ~ Simon Spies. #ITP #Coq
• A functional proof pearl: Inverting the Ackermann heirarchy. ~ Linh Tran. #ITP #Coq
• Euclid’s theorem on the infinitude of primes: a historical survey of its proofs (300 B.C.–2017) and another new proof. ~ Romeo Meštrović. #Math #History
• Crash course on higher-order logic, type theory, etc. ~ Theodore Sider. #Logic via @RrrichardZach

22-Ene-20

• Verified programming of Turing machines in Coq. ~ Fabian Kunze. #ITP #Coq
• Proof pearl: Braun trees. ~ Tobias Nipkow. #ITP #IsabelleHOL
• Algebraic data types aren’t numbers on steroids. Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
• Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. ~ Simon Foster, Jonathan Julián Huerta y Munive, and Georg Struth. #ITP #IsabelleHOL
• Formalizing π-calculus in Guarded Cubical Agda. ~ Niccolò Veltri, Andrea Vezzosi. #ITP #Agda

23-Ene-20

• For beginners. ~ Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
• Drawing Prolog search trees: A manual for teachers and students of logic programming. ~ Johan Bos. #Prolog #LogicProgramming

24-Ene-20

• Coinductive formalization of SECD machine in Agda. ~ Adam Krupička. #MsC_Thesis #ITP #Agda
• Folding lists. ~ Chris Martin (@chris__martin), Julie Moronuki (@argumatronic). #Haskell #FunctionalProgramming
• Beautiful mutable values. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming
• Haskell problems for a new decade. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming
• The Functor family: Profunctor. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming

25-Ene-20

• Formally verified code obfuscation in the Coq Proof Assistant. ~ Weiyun Lu. #PhD_Thesis #ITP #Coq
• A formalised polynomial-time reduction from 3SAT to Clique. ~ Lennard Gäher. #ITP #Coq
• Haskell in production: CentralApp. ~ Ashesh Ambasta (@AsheshAmbasta), Gints Dreimanis. #Haskell #FunctionalProgramming
• La conjetura de Merterns y su relación con un número tan raro como extremada y colosalmente grande. ~ @Alvy. #Matemáticas
• The benefits of sequent calculus. ~ Étienne Miquey. #Logic #CompSci
• Curry-Howard: unveiling the computational content of proofs. ~ Étienne Miquey. #Logic #CompSci
• Realizabilidad clásica y efectos colaterales: Extendiendo la correspondencia de Curry-Howard. ~ Étienne Miquey. #Logic #CompSci
• Introduction to Coq. ~ Assia Mahboubi. #ITP #Coq
• First steps with Coq. ~ Assia Mahboubi. #ITP #Coq
• Programming with dependent types in Coq: inductive families and dependent patter-matching. ~ Matthieu Sozeau. #ITP #Coq
• Homotopy Type Theory. ~ Nicolas Tabareau. #ITP #Coq #HoTT
• Set Theory vs. Type Theory. Alexandre Miquel. #Logic #CompSci

26-Ene-20

• Profunctor optics, a categorical update. ~ Bryce Clarke et als. #Haskell #FunctionalProgramming
• Multiple address spaces in a distributed capability system. ~ Nora Hossle. #MsC_Thesis #Haskell #FunctionalProgramming
• Coherence via wellfoundedness. ~ Nicolai Kraus, Jakob von Raumer. #ITP #LeanProver #Math
• Formalizing the Curry-Howard correspondence. ~ Juan Ferrer Meleiro, Hugo Luiz Mariano. #ITP #Idris #Logic
• A sketch of categorical relation algebra combinators in Z3Py. ~ Philip Zucker (@SandMouth). #Z3 #SMT
• Primeros pasos con Nix: un Linux más funcional. ~ Adrián Arroyo Calle. #Nix #Linux #FunctionalProgramming
• Case study: migrating from lens to optics. ~ Oleg Grenrus (@phadej). #Haskell #FunctionalProgramming

27-Ene-20

• TEpla: A certified type enforcement access-control policy language. ~ Amir Eaman. #PhD_Thesis #ITP #Coq
• Elaborating dependent (co)pattern matching: No pattern left behind. ~ Jesper Cockx, Andreas Abel. #ITP #Agda
• The Cantor-Schröder-Bernstein theorem for ∞-groupoids. ~ Martin Escardo. #ITP #Agda #Math
• FASiM: A framework for automatic formal analysis of simulink models of linear analog circuits. ~ Adnan Rashid, Ayesha Gauhar and Osman Hasan. #ITP #HOL_Light
• Transformations on applicative concurrent computations. ~ Román González. #Haskell #FunctionalProgramming
• The beauty of abstraction in mathematics. ~ Thomas Lingefjärd, Russell Hatami. #Math

28-Ene-20

• Formalization of forcing in Isabelle/ZF. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic
• HolPy: Interactive theorem proving in Python. ~ Bohua Zhan. #ITP #HolPy #Logic #Python
• Org-mode features you may not know. ~ Bastien Guerry (@bzg2). #Emacs #OrgMode

28-Ene-20

• Formalization of forcing in Isabelle/ZF. ~ Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic
• HolPy: Interactive theorem proving in Python. ~ Bohua Zhan. #ITP #HolPy #Logic #Python
• Org-mode features you may not know. ~ Bastien Guerry (@bzg2). #Emacs #OrgMode

30-Ene-20

• Smart induction for Isabelle/HOL (System description). ~ Yutaka Nagashima. #ITP #IsabelleHOL
• Show that a monic (injective) and epic (surjective) function has an inverse in Coq. ~ Arthur Azevedo De Amorim. #ITP #Coq #Math
• Mechanized proofs for PL: Past, present, and future. ~ Talia Ringer. #ITP
• Profunctor optics: The categorical view. ~ Emily Pillmore and Mario Román. #Haskell #FunctionalProgramming #CategoryTheory
• vmap in Haskell. ~ Edward Z. Yang (@ezyang). #Haskell #FunctionalProgramming
• Developing GHC for a Living: Interview with Vladislav Zavialov. ~ Denis Oleynikov. #Haskell #FunctionalProgramming
• Terminating tricky traversals. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming
• Locating performance bottlenecks in large Haskell codebases. ~ Juan Raphael Diaz Simões. #Haskell #FunctionalProgramming

31-Ene-20

• A certificate-based approach to formally verified approximations. ~ Florent Bréhard, Assia Mahboubi, Damien Pous. #ITP #Coq #Math
• Combining predicate transformer semantics for effects: a case study in parsing regular languages. ~ Tim Baanen, Wouter Swierstra. #Agda #FunctionalProgramming
• Searching the space of representations: reasoning through transformations for mathematical problem solving. ~ Daniel Raggi. #PhD_Thesis #ITP #IsabelleHOL
• Introduction and formalization of Boolean algebra. ~ Boro Sitnikovski (@BSitnikovski). #ITP #Metamath #Math
• Property testing in depth: The size parameter. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
• A Pythonista’s Review of Haskell. ~ Ying Wang. #Haskell #Python