Resumen de lecturas compartidas durante marzo de 2021

Esta entrada es una recopilación de lecturas compartidas, durante marzo 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.

• Abstract modeling of systems communication in constructive cryptography using CryptHOL. ~ D. Basin, A. Lochbihler, U. Maurer, S.R. Sefidgar. #ITP #IsabelleHOL
• Verified software units. ~ Lennart Beringer. #ITP #Coq
• linear-logic: a version of intuitionistic linear logic on top of linear Haskell. ~ Edward Kmett. #Haskell #FunctionalProgramming #Logic
• Do judge a test by its cover: Combining combinatorial and property-based testing. ~ Harrison Goldstein, John Hughes, Leonidas Lampropoulos, Benjamin C. Pierce. #Haskell #FunctionalProgramming
• Varieties of mathematical understanding. ~ Jeremy Avigad. #ITP #Math
• A formal proof of the Lax equivalence theorem for finite difference schemes. ~ Mohit Tekriwal, Karthik Duraisamy, Jean-Baptiste Jeannin. #ITP #Coq #Math
• Verifying min-plus Computations with Coq (extended version with appendix). ~ Lucien Rakotomalala, Pierre Roux, Marc Boyer. #ITP #Coq
• For a few dollars more: Verified fine-grained algorithm analysis down to LLVM. ~ Maximilian P.L. Haslbeck, Peter Lammich. #ITP #IsabelleHOL
• Certifying proofs in the first-order theory of rewriting. ~ Fabian Mitterwallner, Alexander Lochmann, Aart Middeldorp, Bertram Felgenhauer. #ITP #IsabelleHOL
• Limits of real numbers in the binary signed digit representation. ~ Franziskus Wiesnet, Nils Köpp. #Haskell #FunctionalProgramming #Math
• El Análisis complejo y una exploración de los conjuntos de Mandelbrot y Julia con código abierto. ~ @Alvy. #Matemáticas #Programación
• Análisis complejo (Una introducción visual e interactiva). ~ Juan Carlos Ponce Campuzano. #eBook #Matemáticas
• Lógica de programação funcional: Pense em Hope (Exercícios de programação funcional com Hope). ~ José Augusto N. G. Manzano, José A. Alonso Jiménez, María J. Hidalgo Doblado. #eBook #Hope #FunctionalProgramming
• Strong typing. ~ M-J. Dominus (1999). #Programming
• Why functional programming matters. ~ John Hughes. #FunctionalProgramming
• The dawning of a new era in applied mathematics. ~ Weinan E. #Math via @emulenews
• La inteligencia artificial nunca será como la humana. ~ Ramón López de Mántaras. #IA
• EmacsTutorial01: Semantic keybindings to memorize hundreds of keys instantly. #Emacs
• SSProve: A foundational framework for modular cryptographic proofs in Coq. ~ C. Abate, P.G. Haselwarter, E. Rivas, A. Van Muylder, T. Winterhalter, C. Hritcu, K. Maillard, B. Spitters. #ITP #Coq
• A well-known representation of monoids and its application to the function “vector reverse”. ~ Wouter Swierstra. #Agda #FunctionalProgramming
• Functional Pearl: Witness me – Constructive arguments must be guided with concrete witness. ~ Hiromi Ishii. #Haskell #FunctionalProgramming
• Combining folds using semigroups. ~ Luc Tielen. #Haskell #FunctionalProgramming
• Many faces of internal functions. ~ Veronika Romashkina. #Haskell #FunctionalProgramming
• Alectryon: a collection of tools for writing technical documents that mix Coq code and prose. ~ Clément Pit-Claudel. #ITP #Coq via @jjcarett2
• Building a personal website with org-mode. ~ Rafael Fernández. #Emacs #OrgMode
• Weblorg: A static HTML generator for Emacs and Org-Mode. #Emacs #OrgMode
• An introduction to typeclass metaprogramming. ~ Alexis King. #Haskell #FunctionalProgramming
• How to build hybrid Haskell and Java programs. ~ Facundo Domínguez, Andreas Hermann. #Haskell #Java
• Course: Programming languages. ~ Zach Tatlock, Leonardo De Moura. #CompSci #ITP #LeanProver
• Coq fundamentals. ~ Zach Tatlock. #ITP #Coq
• Leaning into Spivak’s calculus. ~ Tom Houle. #ITP #LeanProver #Math
• IsarStep: A benchmark for high-level mathematical reasoning. ~ W. Li, L. Yu, Y. Wu, L.C. Paulson. #ITP #IsabelleHOL #Math #MachineLearning
• Formal verification of Zagier’s one-sentence proof. ~ Guillaume Dubach, Fabian Muehlboeck. #ITP #Coq #Math
• Programmer learning list. ~ Michael Snoyman. #Programming
• Install GHC, Cabal and Haskell Language Server IDE on Windows 10. ~ Will Gould. #Haskell #FunctionalProgramming
• Diagrams for Penrose tiles. ~ Chris Reade. #Haskell #FunctionalProgramming #Math
• Quantum projective measurements and the CHSH inequality in Isabelle/HOL. ~ Mnacho Echenim, Mehdi Mhalla. #ITP #IsabelleHOL
• Reasoning about the garden of forking paths. ~ Yao Li, Li-yao Xia, Stephanie Weirich. #ITP #Coq
• Plotting in a formally verified way. ~ Guillaume Melquiond. #ITP #Coq
• Classical (co)recursion: Programming. ~ Paul Downen, Zena M. Ariola. #Agda #Scheme #Python #Java
• Partial evaluation of logic programs in vector spaces. ~ Chiaki Sakama, Hien D. Nguyen, Taisuke Sato, Katsumi Inoue. #LogicProgramming #Math
• Verified quantitative analysis of imperative algorithms. ~ Maximilian P.L. Haslbeck. #PhDThesis #ITP #IsabelleHOL
• Constructive cryptography in HOL: the communication modeling aspect. ~ Andreas Lochbihler, S. Reza Sefidgar. #ITP #IsabelleHOL
• Introduction to lambda calculus. ~ John Lång. #LambdaCalculus #FunctionalProgramming
• Pioneers linking Math and Computer Science win the Abel Prize. ~ Kevin Hartnett. #Math #CompSci
• László Lovász: Working mathematical miracles. ~ Marianne Freiberger. #Math #CompSci
• Avi Wigderson: “It’s good to have hard problems”. ~ Rachel Thomas. #Math #CompSci
• Cryptography and pseudorandomness. ~ Avi Wigderson. #Math #CompSci
• Mathematics and computation (A theory revolutionizing technology and science). ~ Avi Wigderson. #eBook #Math #CompSci via @mbelcrypt_vasco
• The Agda universal algebra library, Part 2: Structure. ~ William DeMeo. #ITP #Agda #Math
• Formal methods for the informal engineer (Tutorial 2: The Coq theorem prover). ~ Cody Roux. #ITP #Coq
• The bottom of the Haskell Pyramid. ~ Gil Mizrahi. #Haskell #FunctionalProgramming
• The history and concept of mathematical proof. ~ Steven G. Krantz. #Logic #Math via @mathematicsprof
• Historia visual de los lenguajes de programación. ~ Jordi Cabot. #Programación vía @fernand0
• Synthetic undecidability and incompleteness of first-order axiom systems in Coq. ~ Dominik Kirst, Marc Hermes. #ITP #Coq #Logic #Math
• Functional Pearls: Heterogeneous binary random-access lists. ~ Wouter Swierstra. #Agda #FunctionalProgramming
• Haskell knowledge map. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
• Evaluación perezosa en Python. Parte 5: Formalización de la secuencia perezosa. ~ Chema Cortés. #Python #Programación
• Formalising mathematics: workshop 8 (group cohomology). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation (in Isabelle/HOL). ~ Ralph Bottesch, Jose Divason, Rene Thiemann. #ITP #IsabelleHOL #Math
• Hyperfunctions. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
• List of formulae involving π. #Math via @mathematicsprof
• (((Wait a moment .) .) .) – Composing functions with multiple arguments. ~ Philip K. Dick. #Haskell #FunctionalProgramming
• Flycheck and HLS. ~ Magnus Therning. #Emacs #LSPmode #Haskell #HLS via @jneira
• The Hermite–Lindemann–Weierstraß transcendence theorem (in Isabelle/HOL). ~ Manuel Eberl. #ITP #IsabelleHOL #Math
• Order theory for computer scientists. ~ Matt Might. #Math #CompSci #Haskell #FunctionalProgramming via @CompSciFact
• What is mathematics? ~ Alec Wilkinson. #Math
• An infinite descent into pure mathematics. ~ Clive Newstead. #eBook #Math
• How to write proofs: a quick guide. ~ Eugenia Cheng. #Logic #Math
• Emacs y lsp-mode. #Emacs #LSPmode
• The Agda universal algebra library – Part 1: Foundation (Equality, extensionality, truncation, and dependent types for relations and algebras). ~ William DeMeo. #ITP #Agda #Math
• A replication crisis in mathematics? ~ Anthony Bordg. #Math #ITP
• Contrastando dos códices matemáticos iluminados. ~ Ángel Requena Fraile. #Matemáticas
• Programming and proving in Agda. ~ Jesper Cockx. #ITP #Agda #FunctionalProgramming #Haskell
• Formal verification of authenticated, append-only skip lists in Agda: Extended version. ~ Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. #ITP #Agda
• Symbolic and automatic differentiation of languages. ~ Conal Elliott. #ITP #Agda
• Quantum projective measurements and the CHSH inequality (in Isabelle/HOL). ~ Mnacho Echenim. #ITP #IsabelleHOL
• Bernoulli polynomials (in Lean prover). ~ Ashvni Narayanan. #ITP #LeanProver #Math
• Pruning unused Haskell dependencies. ~ Dan Fithian. #Haskell #FunctionalProgramming
• Logical foundations: Personal perspective. ~ Yuri Gurevich. #Logic #Math #CompSci
• Recreational Mathematics. ~ Paul Yiu. #eBook #Math
• Five principles for programming languages for learners. ~ Mark Guzdial. #CompSci #Teaching #Programming
• Fifteen awesome cross-platform math apps. ~ Jason Polak. #Math #CompSci #Programming
• Formalizing graph trail properties in Isabelle/HOL. ~ Laura Kovacs, Hanna Lachnitt, Stefan Szeider. #ITP #IsabelleHOL #Math
• Training a first-order theorem prover from synthetic data. ~ Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot, Laurent Orseau, Lei Zhang, Doina Precup, Shibl Mourad. #ATP #MachineLearning
• Measuring mathematical problem solving with the MATH dataset. ~ Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, Jacob Steinhardt. #MachineLearning #ITP #Math
• Theorems for free from separation logic specifications. ~ Lars Birkedal et als. #ITP #Coq
• Mereology (in Isabelle/HOL). ~ Ben Blumson. #ITP #IsabelleHOL #Logic
• Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOL. ~ Asta Halkjær From, Jørgen Villadsen. #Logic #FunctionalProgramming #ITP #Agda #IsabelleHOL
• Formalization and verification of reconfigurable discrete-event system using model driven engineering and Isabelle/HOL. ~ S. Soualah, Y. Hafidi, M. Khalgui, A. Chaoui, L. Kahloul. #ITP #IsabelleHOL
• Generalized universe hierarchies and first-class universe levels. ~ András Kovács. #ITP #Agda
• Roosterize: Suggesting lemma names for Coq verification projects using deep learning. ~ Pengyu Nie, Karl Palmskog, Junyi Jessy Li, Milos Gligoric. #ITP #Coq #DeepLearning
• Neural theorem proving in Lean using Proof Artifact Co-training and language models. ~ Jason Rute. #ITP #LeanProver #MachineLearning
• Neural theorem proving in Lean using Proof Artifact Co-training and language models. [Slides] ~ Jason Rute. #ITP #LeanProver #MachineLearning
• Proving theorems about regular languages and DFAs in Lean. ~ Noam Atar. #ITP #LeanProver
• Boolean rings (in Lean prover). ~ Bryan Gin-ge Chen. #ITP #LeanProver #Math
• HGeometry: Computational Geometry in Haskell. #Haskell #FunctionalProgramming #Math
• Formalising mathematics: workshop 7 (quotients). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Tutorial: Cellular automata and comonads. ~ Siddharth Bhat. #Haskell #FunctionalProgramming
• These are the 10 toughest math problems ever solved. ~ Dave Linkletter. #Math
• L’informatique, quelques questions pour se fâcher entre amis. ~ Serge Abiteboul, Inria Paris, Gilles Dowek. #CompSci
• A brief history of Logic. ~ Moshe Y. Vardi (2003). #Logic #Math #CompSci via @prathyvsh
• Experimental mathematics approach to Gauss diagrams realizability. ~ A. Khan, A. Lisitsa, A. Vernitski. #Prolog #LogicProgramming #Math
• Short introduction to Topology (for Computer Science grad students). ~ Mark Jason Dominus (2010). #Math via @CompSciFact
• Using Nix for Haskell development in Emacs with LSP. ~ Jonas Collberg. #Haskell #Emacs
• Towards a notion of basis for knowledge-based systems – Applications. ~ Gonzalo A. Aranda, Joaquín Borrego, Juan Galán, Daniel Rodríguez. #Math #CompSci
• AI and Theorem Proving [Video]. ~ Josef Urban. #ATP #ITP #MachineLearning #AI
• AI and Theorem Proving [Slides]. ~ Josef Urban. #ATP #ITP #MachineLearning #AI
• Language modeling for mathematical reasoning [Video]. ~ Christian Szegedy. #Logic #Math #AI
• Language modeling for mathematical reasoning [Slides]. ~ Christian Szegedy. #Logic #Math #AI
• Arrows Zoo. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
• Introducing my fall 1987 course on Mathematical Methodology. ~ Edsger W.Dijkstra. #Math
• The sunflower lemma of Erdős and Rado (in Isabelle/HOL). ~ René Thiemann. #ITP #IsabelleHOL #Math
• 12² beautiful mathematical theorems with short proofs. ~ Jörg Neunhäuserer. #Math via @@lizardbill
• Proofs in Mathematics. ~ Alexander Bogomolny. #Math