Resumen de lecturas compartidas durante septiembre de 2020

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.

• 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
• 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
• 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. #Haskell #FunctionalProgramming #CodeWorld
• ¿Qué es Idris y por qué es un lenguaje de programación tan interesante? ~ Adrián Arroyo. #Idris #ProgramaciónFuncional
• 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
• 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. #Programming
• Course retrospective: SMT solving and solver-aided systems. ~ Lindsey Kuper. #SMT #ATP
• The Incredible Proof Machine. #Logic
• Euclidea: Geometric constructions game with straightedge and compass. #Math #Game
• 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, Dmitrii Kovanikov . #Haskell #FunctionalProgramming
• 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. #Math #AI #ITP
• Faster smarter induction in Isabelle/HOL with SeLFiE. ~ Yutaka Nagashima. #ITP #IsabelleHOL
• Haskell’s children. ~ Owen Lynch. #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
• Software Foundations in Lean. ~ Andrew Ashworth. #ITP #LeanProver
• Thoughts on the Pythagorean theorem. ~ Kevin Buzzard. #Math
• List of unsolved problems in mathematics. #Math
• Finger trees explained anew, and slightly simplified (functional pearl) Haskell. ~ Koen Claessen. #Haskell #FunctionalProgramming
• 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. #Haskell #FunctionalProgramming
• 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. #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
• 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
• 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. #CompSci
• 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
• 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
• Some proofs about sequences and series in Coq. #ITP #Coq #Math0
• Liquid Haskell. ~ Andres Löh. #Haskell #FunctionalProgramming
• 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
• Contravariant functors are weird. ~ Sanjiv Sahayam. #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
• 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
• Holbert: A graphical interactive proof assistant designed for education. ~ Liam O’Connor. #ITP #Haskell #Logic
• 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
• 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
• 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. #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
• 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
• 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
• 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