Resumen de lecturas compartidas del 22 al 29 de febrero de 2020
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