Resumen de lecturas compartidas durante enero de 2021

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

• Paul Cohen, el matemático que por resolver un problema terminó creando dos mundos. ~ Dalia Ventura. #Matemáticas
• HELIX: From math to verified code. ~ Vadim Zaliva. #PhD_Thesis #ITP #Coq #Math
• Implementing the decomposition of soundness proofs of abstract interpreters in Coq. ~ Jens de Waard. #MSc_Thesis #ITP #Coq
• Longest segment of balanced parentheses: an exercise in program inversion in a segment problem (Functional Pearl). ~ Shin-Cheng Mu, Tsung-Ju Chiang. #Haskell #FunctionalProgramming
• A greedy algorithm for dropping digits (Functional Pearl). ~ Richard Bird, Shin-Cheng Mu. #Haskell #FunctionalProgramming
• Formalising mathematics: Workshop 2 (Groups and subgroups). ~ Kevin Buzzard. #ITP #LeanProver #Math
• Building a passphrase generator in Haskell. ~ Mathias Jean Johansen. #Haskell #FunctionalProgramming
• What do we mean by equality? ~ Kevin Buzzard. #Logic #Math
• ¿Cuántos infinitos existen?️ El teorema de Cantor. ~ Urtzi Buijs. #Matemáticas
• IMO 2013 Q5 in Lean. ~ David Renshaw. #ITP #LeanProver #Math
• Evolution of artificial intelligence languages, a systematic literature review. ~ Emmanuel Adetiba, Temitope John, Adekunle Akinrinmade, Funmilayo Moninuola, Oladipupo Akintade, Joke Badejo. #AI #Programming
• Edición de textos científicos con LaTeX. (Composición, gráficos, Inkscape, Tikz y presentaciones Beamer). ~ Alexánder Borbón, Walter Mora. #LaTeX
• IMO 2011 Q3 in Lean. ~ David Renshaw. #ITP #LeanProver #Math
• Teaching algorithms and data structures with a proof assistant. ~ Tobias Nipkow. #ITP #IsabelleHOL
• 2-Adjoint equivalences in Homotopy Type Theory. ~ Daniel Carranza, Jonathan Chang, Krzysztof Kapulkin, Ryan Sandford. #ITP #LeanProver #HoTT
• The Agda universal algebra library and Birkhoff’s theorem in Martin-Löf dependent type theory. ~ William DeMeo. #ITP #Agda #Math
• Formal verification of authenticated, append-only skip lists in Agda. ~ Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva, Guy L. Steele Jr. #ITP #Agda
• A Haskell implementation of the Lyness-Moler’s numerical differentiation algorithm. ~ Weng Kin Ho, Chu Wei Lim. #Haskell #FunctionalProgramming #Math
• Let’s not dumb down the history of computer science. ~ Donald E. Knuth, Len Shustek. #CompSci
• Formalising mathematics: workshop 1. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Sums of consecutive reciprocals. ~ John D. Cook. #Math
• Descubriendo la programación funcional: Lisp con Diego Sevilla. #Lisp #CommonLisp #ProgramaciónFuncional12
• Las bases matemáticas de la programación funcional. ~ Héctor Iván Patricio Moreno. #ProgramaciónFuncional
• Proceedings of the 2020 Scheme and Functional Programming Workshop. #FunctionalProgramming
• Machine-learning mathematical structures. ~ Yang-Hui He. #MachineLearning #Math
• Ten computer codes that transformed science. ~ Jeffrey M. Perkel. #CompSci via @vardi
• Tablas para cálculos en org-mode. #Emacs #OrgMode
• Teaching Haskell means teaching important concepts. ~ Jonathan Thaler. #Haskell #FunctionalProgramming
• Formalising mathematics: an introduction. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Capturing call stack with Haskell exceptions. ~ Maxim Koltsov. #Haskell #FunctionalProgramming
• The Common Lisp Cookbook [in EPUB and PDF format]./#download-in-epub #eBook #CommonLisp
• El número de Dottie. ~ M.A. Morales. #Matemáticas
• Domain-specific languages of Mathematics [Draft of January 17, 2021]. ~ Patrik Jansson, Cezar Ionescu, Jean-Philippe Bernardy. #Haskell #FunctionalProgramming #Math
• DSLsofMath: Domain-specific languages of Mathematics [Repo]. ~ Patrik Jansson et als. #Haskell #FunctionalProgramming #Math
• A novice-friendly induction tactic for Lean. ~ Jannis Limperg. #ITP #LeanProver
• Towards Hoare logic for a small imperative language in Haskell. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
• Computer Science as the continuation of Logic by other means. ~ Georg Gottlob. #Logic #CompSci
• Formalizing Galois Theory in Lean [Slides]. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math
• Formalizing Galois Theory in Lean [Vídeo]. ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math
• Las Matemáticas son suficientes para mí. ~ Juan Arias de Reyna. #Matemáticas
• org-special-block-extras (A unified interface for special blocks and links: defblock). ~ Musa Al-hassy./#Judgements-Inference-rules-and-proof-trees #Emacs #OrgMode
• Model theory in Lean. ~ Vaibhav Karve. #ITP #LeanProver #Logic
• Machine-checked computer-aided mathematics. ~ Assia Mahboubi. #ITP #Coq #Math
• Towards efficient and verified virtual machines for dynamic languages. ~ Martin Desharnais, Stefan Brunthaler. #ITP #IsabelleHOL
• From Aristotle to the iPhone. ~ Moshe Y. Vardi. #Logic #CompSci
• Axiomatic Geometry in Lean. ~ Vaibhav Karve, Lawrence Zhao, Edward Kong, Alex Dolcos, Nicholas Phillips. #ITP #LeanProver #Math
• Axiomatic Geometry in Lean [Video]. ~ Vaibhav Karve. #ITP #LeanProver #Math
• Axiomatic Geometry in Lean [Code]. ~ Vaibhav Karve, Lawrence Zhao, Edward Kong, Alex Dolcos, Nicholas Phillips. #ITP #LeanProver #Math
• Lebesgue integration. (Detailed proofs to be formalized in Coq). ~ François Clément, Vincent Martin. #ITP #Coq #Math
• Permutate parsers, don’t validate. ~ Ju Liu. #Haskell #FunctionalProgramming
• An introduction to ghc-debug: precise memory analysis for Haskell programs. ~ Matthew Pickering. #Haskell #FunctionalProgramming
• Why exactly I want Boring Haskell to happen. ~ Artyom Kazak. #Haskell #FunctionalProgramming
• Beginner’s guide to mathematical constructivism. ~ Jan Gronwald. #Math
• En toute logique: une origine de l’ordinateur. ~ Frédéric Prost. #Logic #CompSci
• Publicar HTML con Org-Mode. #Emacs #OrgMode
• A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems. ~ Alexander Lochmann, Aart Middeldorp, Fabian Mitterwallner, Bertram Felgenhauer. #ITP #IsabelleHOL
• A formal proof of PAC learnability for decision stumps. ~ Joseph Tassarotti, Koundinya Vajjha, Anindya Banerjee, Jean-Baptiste Tristan. #ITP #LeanProver
• The friendship theorem in Lean. ~ Aaron Anderson. #ITP #LeanProver #Math
• CertRL: Formalizing convergence proofs for value and policy iteration in Coq. ~ Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry Trager, Nathan Fulton. #ITP #Coq
• Abel-Ruffini Theorem as a Mathematical Component. ~ Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. #ITP #Coq #Math
• Making an IO. ~ Lúcás Meier. #Haskell #FunctionalProgramming
• Contextual refinement of the Michael-Scott queue (Proof pearl). ~ Simon Friis Vindum, Lars Birkedal. #ITP #Coq
• Reasoning about monotonicity in separation logic. ~ Amin Timany, Lars Birkedal. #ITP #Coq
• Developing and certifying Datalog optimizations in Coq/MathComp. ~ Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin. #ITP #Coq
• An Isabelle/HOL formalization of AProVE’s termination method for LLVM IR. ~ Max W. Haslbeck, René Thiemann. #ITP #IsabelleHOL #Haskell
• Certified quantum computation in Isabelle/HOL. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL
• Automatically generalising theorems using typeclasses in Lean [Slides]. ~ Alex J. Best./#/#ITP #LeanProver #Math
• Automatically generalising theorems using typeclasses in Lean [Video]. ~ Alex J. Best. #ITP #LeanProver #Math
• Implementation of two layers type theory in Dedukti and application to Cubical Type Theory. ~ Bruno Barras, Valentin Maestracci. #ITP #Dedukti
• Lean Together 2021. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Formalizing category theory in Agda. ~ Jason Z.S. Hu, Jacques Carette. #ITP #Agda #CategoryTheory #Math
• Formal verification of semi-algebraic sets and real analytic functions. ~ J. Tanner Slagel, Lauren White, Aaron Dutle. #ITP #PVS #Math
• On the formalisation of Kolmogorov complexity. ~ Elliot Catt, Michael Norrish. #ITP #HOL4
• Haskell: (.) . (.) explained (Let’s get a grasp of composition equivalences in Haskell). #Haskell #FunctionalProgramming
• Formalizing the ring of Witt vectors. ~ Robert Y. Lewis. #ITP #LeanProver #Math
• Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading. ~ Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber. #ITP #HOL4
• Object-level reasoning with logics encoded in HOL Light. ~ Petros Papapanagiotou, Jacques Fleuriot. #ITP #HOL_Light #Logic
• Deductive systems and coherence for skew prounital closed categories. ~ Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. #ITP #Agda
• Why Haskell is our first choice for building production software systems. ~ Christian Charukiewicz. #Haskell #FunctionalProgramming
• 144 is the largest square in the Fibonacci Sequence (A formalisation of Cohn’s Proof). ~ Harun Khan #ITP #LeanProver #Math via @XenaProject
• The Eudoxus real numbers in Lean. ~ Xiang Li. #ITP #LeanProver #Math via @XenaProject
• Set theory, type theory and the future of proof verification software. ~ James Palmer. #ITP #LeanProver #Math via @XenaProject
• A formal proof of correctness of a recursive integer square root algorithm. ~ Mark Dickinson. #ITP #LeanProver #Math
• Schemes in Lean. ~ Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, Scott Morrison. #ITP #LeanProver #Math
• Performance aspects of correctness-oriented synthesis flows. ~ F. Bornebusch, C. Lüth, R. Wille, R. Drechsler. #ITP #Coq
• An anti-locally-nameless approach to formalizing quantifiers. ~ Olivier Laurent. #ITP #Coq
• Formal verification of arithmetic RTL: Translating Verilog to C++ to ACL2. ~ David M. Russinoff. #ITP #ACL2
• Formalizing 100 theorems. ~ Freek Wiedijk. #ITP #Math
• Formalizing 100 theorems in Lean. #ITP #Math #LeanProver
• Trouble in paradise: Fibonacci. #Haskell #FunctionalProgramming
• Indexed optics dilemma. ~ Oleg Grenrus. #Haskell #FunctionalProgramming
• Algorithmic problem solving. ~ Johan Sannemo. #eBook #Programming #Algorithms
• La saga del infinito, de Mates Mike. ~ M.A. Morales. #Matemáticas
• LeanStep: a dataset and environment for (interactive) neural theorem proving [Video]. ~ Jason Rute. #ITP #Leanprover #MachineLearning
• LeanStep: a dataset and environment for (interactive) neural theorem proving [Slides]. ~ Jason Rute. #ITP #Leanprover #MachineLearning
• Theorem proving and algebra. ~ Joseph A. Goguen. #eBook #ITP #Math
• Elementary programming. ~ Michael Peyton Jones. #Haskell #Programming
• A first look at info table profiling. ~ Matthew Pickering, David Eichmann. #Haskell #FunctionalProgramming
• Benchmarks of discrimination package. ~ Oleg Grenrus. #Haskell #FunctionalProgramming
• CLP(FD) and CLP(ℤ): Prolog integer arithmetic. ~ Markus Triska. #Prolog #LogicProgramming #CLP
• ECLIPSE (A tutorial introduction). ~ Andrew M. Cheadle et als. #Prolog #LogicProgramming #CLP
• Programación lógica con restricciones. #Prolog #CLP
• Soluciones lógicas de problemas lógicos. #Prolog #ProgramaciónLógica #CLP
• ACL2 induction heuristics. ~ J Strother Moore. #ITP #ACL2
• Word problem for one-relator groups. ~ Chris Hughes. #ITP #LeanProver #Math
• A Lean introduction to pure mathematics. ~ Gihan Marasingha. #ITP #LeanProver #Logic #Math
• MTH1001 (Mathematical structures) in Lean. ~ Gihan Marasingha. #ITP #LeanProver #Logic #Math
• EMS reals (A project for investigating the real number system via the interactive theorem prover Lean). ~ Gihan Marasingha. #ITP #LeanProver #Logic #Math
• Lassie: HOL4 tactics by example. ~ Heiko Becker et als.. #ITP #HOL4
• Formalizing domain models of the typed and the untyped lambda calculus in Agda. ~ David Lidell. #MSc_Thesis #ITP #Agda
• On the unreasonable effectiveness of SAT Solvers. ~ Vijay Ganesh, Moshe Y. Vardi. #Logic #ATP #SAT_Solvers
• Riemann Hypothesis in Lean. ~ Brandon H. Gomes, Alex Kontorovich. #ITP #LeanProver #Math
• An example of a manifold [Slides]. ~ Heather Macbeth. #ITP #LeanProver #Math
• An example of a manifold [Video]. ~ Heather Macbeth. #ITP #LeanProver #Math
• Symbolic computation in Maude: Some tapas. ~ José Meseguer. #ITP #Maude
• Compile-time evaluation in Haskell. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
• Predictions for 2021. | Gödel’s Lost Letter and P = NP. ~ R.J. Lipton & K.W. Regan. #CompSci
• Formalizing Hall’s Marriage Theorem in Lean. ~ Alena Gusakov, Bhavik Mehta, Kyle A. Miller. #ITP #LeanProver #Math
• Finiteness in cubical type theory. ~ Donnacha Oisín Kidney. #MSc_Thesis #ITP #Agda #HoTT
• An overview of Lean 4. ~ Leonardo de Moura, Sebastian Ullrich. #ITP #LeanProver
• Measure theory in Lean [slides]. ~ Floris van Doorn. #ITP #LeanProver #Math
• Measure theory in Lean

  . ~ Floris van Doorn. #ITP #LeanProver #Math

• The visitor pattern is essentially the same thing as Church encoding. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming
• Functional Pearl: It’s easy as 1,2,3. ~ Graham Hutton. #Haskell #FunctionalProgramming
• Trying to compose non-composable: monads. ~ Murat Kasimov. #Haskell #FunctionalProgramming
• Learning TypeFamilies together! ~ Flavio Corpa. #Haskell #FunctionalProgramming
• Tautology checkers in Isabelle and Haskell. ~ Jørgen Villadsen. #Logic #ITP #IsabelleHOL #Haskell #FunctionalProgramming
• Theorem proving for Lewis logics of counterfactual reasoning. ~ Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato. #ATP #Logic #Prolog #LogicProgramming
• Deterministic Finite Automata (DFA) in Lean. ~ Fox Thomson. #ITP #LeanProver
• Nondeterministic Finite Automata (NFA) in Lean. ~ Fox Thomson. #ITP #LeanProver
• Theory of iteration and recursion. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• Bind the gap (Monthly digital functional programming magazine) [Issue 2, Dec 2020]. #Haskell #FunctionalProgramming
• Mirror mirror: Reflection and encoding via. ~ Matt Parsons. #Haskell #FunctionalProgramming
• Lessons learned from a year of writing Haskell. ~ Adam Wespiser. #Haskell #FunctionalProgramming
• Coindexed optics. ~ Oleg Grenrus.l#Haskell #FunctionalProgramming
• Dihedral groups in Lean. ~ Shing Tak Lam. #ITP #LeanProver #Math
• Verifying C11-style weak memory libraries. ~ Sadegh Dalvandi, Brijesh Dongol. #ITP #IsabelleHOL
• Lean 4 manual. #Lean4 #FunctionalProgramming #ITP
• Formalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu. #ITP #Coq #Math
• A Coq formalization of data provenance. Véronique Benzaken et als. #ITP #Coq
• Synthetic undecidability proofs in Coq. ~ Dominik Kirst. #ITP #Coq
• Two reasons why you found learning haskell hard. ~ School of FP. #Haskell #FunctionalProgramming
• Learn just enough about linear types. ~ Artyom Kazak. #Haskell #FunctionalProgramming