Esta entrada es una recopilación de lecturas compartidas, durante mayo de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
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.
- ¿Pueden las máquinas ser creativas? ~ Ramón López de Mántaras. #IA
- Fun with category theory and dynamical systems. ~ Chris Smith. #CategoryTheory
- Representable functors: Practical examples. ~ Siddharth Bhat. #Haskell #FunctionalProgramming
- Quantum and classical registers. ~ Dominique Unruh. #ITP #IsabelleHOL
- Proof repair. ~ Talia Ringer. #PhD_Thesis #ITP #Coq
- CoCEC: An automatic combinational circuit equivalence checker based on the interactive theorem prover. ~ Wilayat Khan, Farrukh Aslam Khan, Abdelouahid Derhab, Adi Alhudhaif. #ITP #Coq
- Some formal tools for computer arithmetic: Flocq and Gappa. ~ S. Boldo, G. Melquiond. #ITP #Coq
- A beginner guide to Iris, Coq and separation logic. ~ Elizabeth Dietrich. #ITP #Coq
- Mechanized type safety for gradual information flow. ~ Tianyu Chen, Jeremy G. Siek. #ITP #Agda
- Actions you can handle: Dependent types for AI plans. ~ Alasdair Hill, Ekaterina Komendantskaya, Matthew L. Daggitt, Ronald P. A. Petrick. #ITP #Agda #AI
- Formal synthesis of filter components for use in security-enhancing architectural transformations. ~ David S. Hardin, Konrand L. Slind. #ITP #ACL2
- A combinator library for taxes. ~ Fraser Tweedale. #Haskell #FunctionalProgramming
- Haskell: Applicative. ~ Vlad P. Luchian. #Haskell #FunctionalProgramming
- Testing smart contracts with QuickCheck. ~ John Hughes. #Haskell #FunctionalProgramming #QuickCheck
- Proof-oriented programming in F*. #ITP #FunctionalProgramming
- Separation logic foundations (Software Foundations, Volume 6). ~ Arthur Charguéraud. #ITP #Coq
- The Natural Number Game. ~ Brent Yorgey. #ITP #LeanProver #Math
- Combinatorics on words basics. ~ Štěpán Holub, Martin Raška, Štěpán Starosta. #ITP #IsabelleHOL
- Graph lemma. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
- Lyndon words. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
- Functors and monads for people who have read too many “tutorials”. ~ Jeremy Bowers. #Haskell #FunctionalProgramming
- Tying the Knot in Haskell. ~ Michael Snoyman. #Haskell #FunctionalProgramming
- Verifying time complexity of binary search using Dafny. ~ Shiri Morshtein et als. #Dafny #Algorithms
- Two new ways to formally prove Dandelin-Gallucci’s theorem. ~ D. Braun, N. Magaud, P. Schreck. #ITP #Coq #Math
- A logic theory pattern for linearized control systems. ~ A. Domenici, C. Bernardeschi. #ITP #PVS
- Fix(ity) me. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- Translating LaTeX to Coq: A recurrent neural network approach to formalizing natural language proofs. ~ Benjamin A. Carman. #PhD_Thesis #ITP #Coq #NeuralNetwork
- A novel proof of shuffle: Exponentially secure cut-and-choose. ~ Thomas Haines, Johannes Müller. #ITP #Coq
- Verbatim: A verified lexer generator. ~ D. Egolf, S. Lasser, K. Fisher. #ITP #Coq
- miniF2F: Formal to Formal Mathematics Benchmark consisting of exercise statements from olympiads (AMC, AIME, IMO). #ITP #LeanProver #Math
- A complete bibliography of publications in the Journal of Functional Programming. ~ Nelson H.F. Beebe. #FunctionalProgramming
- Annotations in GHC. ~ Shayne Fletcher. #Haskell #FunctionalProgramming
- Mathematicians answer old question about odd graphs. ~ Kevin Hartnett. #Maths
- Silver Oak: Formal specification and verification of hardware, especially for security and privacy. #ITP #Coq
- An AI has disproved five mathematical conjectures with no human help. #AI #Math
- Constructions in combinatorics via neural networks. ~ Adam Zsolt Wagner. #AI #Math #MachineLearning #NeuralNetwork
- Module organization guidelines for Haskell projects. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming
- A collection of OEIS sequences in Haskell. ~ Debdut Karmakar. #Haskell #FunctionalProgramming #Math
- Formally verified simulations of state-rich processes using interaction trees in Isabelle/HOL. ~ Simon Foster, Chung-Kil Hur, Jim Woodcock. #ITP #IsabelleHOL
- Formalization of ring theory in PVS (Isomorphism theorems, principal, prime and maximal ideals, chinese remainder theorem). ~ Thaynara Arielly de Lima et als. #ITP #PVS #Math
- Computable analysis and notions of continuity in Coq. ~ H. Thies, L. Thery, F. Steinberg. #ITP #Coq #Math
- Fixed point construction on complete lattices. ~ Johannes Hölzl et als. #ITP #LeanProver #Math
- Constructions in combinatorics via neural networks. ~ Adam Zsolt Wagner. #MachineLearning #Math
- On preserving the computational content of mathematical proofs: toy examples for a formalising strategy. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
- Hensel’s Lemma for the p-adic integers (in Isabelle/HOL). ~ Aaron Crighton. #ITP #IsabelleHOL #Math
- The Haskell Phrasebook. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming
- Haskell MOOC University of Helsinki. ~ Joel Kaasinen, John Lång. #Haskell #FunctionalProgramming
- Counterexamples in type systems. ~ Stephen Dolan. #TypeTheory
- Qué son los algoritmos y cómo aprenden de nosotros. | BBC Mundo. #Algoritmos
- Enigma GPT-2: ¿Puedes distinguir un artículo real de otro falso generado mediante inteligencia artificial simplemente leyendo el resumen?. ~ @Alvy. #IA
- Regreso al futuro de las matemáticas: Si Hipatia levantara la cabeza. ~ Patricia Contreras Tejada. #Matemáticas
- The Genuine Sieve of Eratosthenes. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
- Type-guided development and garden paths. ~ Fraser Tweedale. #Haskell #FunctionalProgramming
- Why you should learn functional programming: Type classes vs. interfaces. ~ @forketyfork #Java #Haskell #FunctionalProgramming
- How mathematicians use homology to make sense of topology. ~ Kelsey Houston-Edwards. #Math
- Automated conjecturing in QuickSpec. ~ Moa Johansson, Nicholas Smallbone. #Haskell #FuncionalProgramming
- Functional algorithms, verified! ~ Tobias Nipkow et als. #eBook #ITP #IsabelleHOL #Algorithms
- Construction of an algebraic number that is not solvable by radicals. ~ Thomas Browning. #ITP #LeanProver #Math
- Slides and exercises of the Lean 4 course “Theorem prover lab: applications in programming languages”. ~ Jakob von Raumer, Sebastian Ullrich. #ITP #Lean4
- Lean 4 Metamath verifier. ~ Mario Carneiro. #ITP #Lean4 #Metamath
- The type theory of Lean. ~ Mario Carneiro. #ITP #LeanProver #TypeTheory
- Books: Inquiry-Based Learning Guides. #eBooks #Math
- The beauty of functional languages in Deep Learning — Clojure and Haskell. ~ Jun Wu. #Clojure #Haskell #FunctionalProgramming #DeepLearning
- The IMO Grand Challenge. ~ Daniel Selsam. #ITP #LeanProver
- The trick to avoid deeply-nested error-handling code. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming
- Regression test selection. ~ Susannah Mansky. #ITP #IsabelleHOL #Math
- Itauto: an extensible intuitionistic SAT solver. ~ Frédéric Besson. #ITP #Coq #Logic #SAT_Solver
- Programming in Z3 by learning to think like a compiler. ~ Marianne Bellotti. #SMT #Z3
- Formalizing the face lattice of polyhedra. ~ Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub. #ITP #Coq #Math
- Lean Together 2021: Panel on teaching with proof assistants. #ITP #LeanProver
- Quick and dirty backpropagation in Haskell. ~ Francesco Mazzoli. #Haskell #FunctionalProgramming #NeuralNetwork
- Feferman’s virtual book: Logic, Mathematics, and Conceptual Structuralism. ~ Peter Smith. #Logic #Math
- A formalised theorem in the partition calculus. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
- Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL. ~ Martin Raška, Štěpán Starosta. #ITP #IsabelleHOL
- Reliable reconstruction of fine-grained proofs in a proof assistant. ~ HJ Schurr, M Fleury, M Desharnais. #ITP #IsabelleHOL
- LEO: A programming language for formally verified, zero-knowledge applications. ~ C. Chin et als. #ITP #ACL2
- Formal verification of termination criteria for first-order recursive functions. ~ C.A. Muñoz et als. #ITP #PVS
- Verifying the semantics of disambiguation rules (Using parse tree repairing for showing safety and completeness of associativity and priority rules). ~ L. Miljak. #ITP #Coq