Esta entrada es una recopilación de lecturas compartidas, del 22 al 29 de febrero, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
1 DAO: Demostración asistida por ordenador
1.1 DAO con Agda
- Flexible coinduction in Agda. ~ Luca Ciccone. #MSc_Thesis #ITP #Agda
- The Cantor-Schröder-Bernstein Theorem for ∞-groupoids. ~ Martı́n Escardó. #ITP #Agda #Math
- agda-metis: Metis prover reasoning for propositional logic in Agda. ~ Jonathan Prieto-Cubides. #ITP #Agda #Metis
- agda-prop: A library for classical propositional logic in Agda. ~ Jonathan Prieto-Cubides. #ITP #Agda #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
- Various new theorems in constructive univalent mathematics written in Agda. ~ Martín Escardó. #ITP #Agda #Math
- Proof-reconstruction in type theory for propositional logic. ~ Jonathan Prieto-Cubides, Andrés Sicard-Ramírez. #ITP #Agda #Metis #Logic
1.2 DAO con Coq
- Course: Machine-checked Mathematics. ~ Assia Mahboubi. #ITP #Coq #Math
- Short proof of Menger’s theorem in Coq (Proof Pearl). ~ Christian Doczka. #ITP #Coq #Math
- 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
- Experiences from exporting major proof assistant libraries. ~ Michael Kohlhase, and Florian Rabe. #ITP #Coq #HOL_Light #IsabelleHOL #Mizar #PVS #MMT
- 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
- A machine-checked constructive metatheory of computation tree logic. ~ Christian Doczkal (2016). #PhD_Thesis #ITP #Coq #Logic
1.3 DAO con HOL4
- A mechanised semantics for HOL with ad-hoc overloading. ~ Johannes Åman Pohjola, Arve Gengelbach. #ITP #HOL4
1.4 DAO con Isabelle/HOL
- Teaching a formalized logical calculus. ~ Asta Halkjær From et als. #Logic #Teaching #ITP #IsabelleHOL
- Isabelle/Spartan: A dependent type theory framework for Isabelle. ~ Joshua Chen. #ITP #IsabellleHOL #HoTT
- Implementing the Goodstein function in λ-calculus. ~ Bertram Felgenhauer. #ITP #IsabelleHOL
- A generic framework for verified compilers in Isabelle/HOL. ~ Martin Desharnais. #ITP #IsabelleHOL
- On memory addressing. ~ Reto Achermann. #PhD_Thesis #ITP #IsabelleHOL
- Highly automated formal proofs over memory usage of assembly code. ~ Freek Verbeek et als. #ITP #IsabelleHOL
1.5 DAO en general
- A selected bibliography on formalised mathematics. ~ Laurent Théry. #ITP #Math
- MMT: The Meta Meta Tool (system description). ~ Florian Rabe. #ITP #MMT
2 Programación declarativa
2.1 Programación funcional con Haskell
- Testing higher-order properties with QuickCheck. ~ Li-yao Xia (@lysxia). #Haskell #FunctionalProgramming #QuickCheck
- Another breadth-first traversal. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
- An analysis of programming paradigms in high-level synthesis tools. ~ Pieter Staal. #Haskell #FunctionalProgramming
- Revisiting separation: Algorithms and complexity. ~ Daniel Oliveira, and João Rasga. #Logic #Haskell #FunctionalProgramming
- Linear temporal logic: separation and translation. ~ Daniel Oliveira. #MSc_Thesis #Logic #Haskell #FunctionalProgramming
- Translation from FOL to LTL+Past and LTL, via separation of LTL+Past. ~ Daniel Oliveira. #Logic #Haskell #FunctionalProgramming
- Marlowe: implementing and analysing financial contracts on blockchain. ~ Pablo Lamela Seijas et als. #Haskell #ITP #IsabelleHOL #Blockchain #Cardano
- Probabilistic programming with monad‑bayes, Part 3: A bayesian neural network. ~ Siddharth Bhat, Simeon Carstens, Matthias Meschede. #Haskell #FunctionalProgramming
- Type-based formal verification. ~ Alejandro Serrano (@trupill). #Haskell #Verification
- Category theory as a tool for thought. ~ Daniel Beskin. #CategoryTheory #FunctionalProgramming #Haskell
2.2 Programación lógica con Prolog
- Automating the generation of high school geometry proofs using Prolog in an educational context. ~ Ludovic Font et als. #Prolog #LogicProgramming #Math
3 Lógica
- 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
- The natural deduction pack. ~ Alastair Carr. #Logic
4 Otros
- Mathematical structures. ~ Contributors of math.chapman.edu. #Math
- Math is your insurance policy. ~ Bartosz Milewski (@BartoszMilewski). #Programming
- Reductions and jokes. ~ R.J. Lipton & K.W. Regan. #CompSci #Math
- Structure and interpretation of computer programs — JavaScript adaptation. #eBook #JavaScript #SICP
- Mathematical humor. ~ Andrej and Elena Cherkaev. #Math
- 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
- Lectures on scientific computing with Python. ~ Robert Johansson (2017). #Python