Resumen de lecturas compartidas durante junio de 2021

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

• A Perron–Frobenius theorem for deciding matrix growth. ~ RenéThiemann. #ITP #IsabelleHOL #Math
• CoqQFBV: A scalable certified SMT quantifier-free bit-vector solver. ~ Xiaomu Shi et als. #ITP #Coq
• On a machine-checked proof for an optimized method to multiply polynomials. ~ S.D. Meshveliani.f#page=88 #ITP #Agda #Math
• Augmenting the human mathematician. ~ H.K. Sørensen, M.W. Johansen, R. Hoekzema, H. Breman. #ITP #ATP #Math
• Towards finding longer proofs. ~ Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, Josef Urban. #ATP #MachineLearning
• Towers of Hanoi from a random start. ~ Chris Smith. #Haskell #FunctionalProgramming
• Well-founded recursion. ~ Gihan Marasingha. #ITP #LeanProver #Math
• A modular formalisation of finite group theory. ~ Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, LaurentThéry. #ITP #Coq #Math
• SAT solver-prover in Lean 4. ~ Siddhartha Gadgil. #ITP #LeanProver #Logic
• ProvingGround: Automated Theorem proving by learning. ~ Siddhartha Gadgil. #ITP #LeanProver #MachineLearning
• Automating Mathematics? ~ Siddhartha Gadgil.l#/ #Math #ATP #ITP #AI
• Euclidean geometry by high-performance solvers? ~ Siddhartha Gadgil, Anand Tadipatri. #Math #ATP #SAT #SMT
• A formally verified proof of the central limit theorem. ~ Luke Serafin. #PhD_Thesis #ITP #IsabelleHOL #Math
• A formally verified proof of Kruskal’s tree theorem in Lean. ~ Minchao Wu. #ITP #LeanProver #Math
• Typed programs don’t leak data. ~ Mistral Contrastin. #Haskell #FunctionalProgramming
• Historia de desafíos matemáticos. Cómo ganar un millón de dólares. ~ Antonio Pérez. #Matemáticas vía @manuel_de_leon
• La prova del software (in Italian). ~ Riccardo Brasca et als. #ITP #LeanProver #Math
• Groundwork for a fallibilist account of Mathematics. ~ Silvia De Toffoli. #Math
• Associated types in two different ways. #Haskell #FunctionalProgramming
• Creación artística y creación matemática. ~ Juan Arias de Reyna. #Matemáticas #ITP #LeanProver
• Abstract algebra: Theory and applications. ~ Thomas W. Judson et als. #eBook #Math #Sage
• Taller de Sage. ~ Antonio Behn. #Sage #Matemáticas
• MiniSail: A kernel language for the ISA specification language SAIL in Isabelle/HOL. ~ Mark Wassell. #ITP #IsabelleHOL
• Public announcement logic (in Isabelle/HOL). ~ Asta Halkjær From. #ITP #IsabelleHOL
• Formalized soundness and completeness of epistemic logic. ~ Asta Halkjær From et als. #Logic #ITP #IsabelleHOL
• Results in modal and dynamic epistemic logic (A formalization in Lean). ~ Paula Neeley. #Logic #ITP #LeanProver
• Hito de las demostraciones asistidas por ordenador en Nature. ~ Nerea Diez López. #DAO #LeanProver #Matemáticas
• Embedding Youtube videos with org-mode links. ~ Artur Malabarba. #OrgMode #Emacs
• Verified model checking for conjunctive positive logic. ~ Alex Abuin et als. #ITP #Dafny
• CoStar: a verified ALL (*) parser. ~ Sam Lasser et als. #ITP #Coq
• Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8. ~ Kyeongmin Cho et als. #ITP #Coq
• Las matemáticas que estudian los límites de los ordenadores. ~ Daniel Graça, Ágata A. Timón. #Matemáticas #Computación
• A formalization of elementary group theory in the proof assistant Lean. ~ Andrew Zipperer. #ITP #LeanProver #Math
• Types versus sets in math and programming languages. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• The dawn of formalized mathematics. ~ Andrej Bauer. #ITP #Math
• Van der Waerden’s theorem in Isabelle/HOL. ~ Katharina Kreuzer, Manuel Eberl. #ITP #IsabelleHOL #Math
• Deconstructing classes. ~ Nicholas Clarke. #Haskell #FunctionalProgramming
• A formally verified checker for first-order proofs. ~ Seulkee Baek. #ITP #Agda #Logic
• Reaching for the star: Tale of a monad in Coq. ~ Pierre Nigron, Pierre-Évariste Dagand. #ITP #Coq
• Mechanising complexity theory: The Cook-Levin theorem in Coq. ~ Lennard Gäher, Fabian Kunze. #ITP #Coq
• A mechanized proof of the max-flow min-cut theorem for countable networks. ~ Andreas Lochbihler. #ITP #IsabelleHOL
• Formalization of basic combinatorics on words. ~ Štěpán Holub, Štěpán Starosta. #ITP #IsabelleHOL
• Proof Pearl: Playing with the Tower of Hanoi formally. ~ Laurent Théry. #ITP #Coq
• The CakeML project’s quest for ever stronger correctness theorems. ~ Magnus O. Myreen. #ITP #HOL4
• A natural formalization of the mutilated checkerboard problem in Naproche. ~ Adrian De Lon, Peter Koepke, Anton Lorenzen. #ITP #Naproche
• Verified progress tracking for timely dataflow. ~ M. Brun, S. Decova, A. Lattuada, D. Traytel. #ITP #IsabelleHOL
• Ptolemy’s Theorem in Lean. ~ Manuel Candales, Benjamin Davidson. #ITP #LeanProver #Math
• Formal software verification measures up. ~ Samuel Greengard. #FormalVerification
• Program verification: Vision and reality. ~ Moshe Y. Vardi. #FormalVerification
• Consequence relations (An introduction to the Tarski-Lindenbaum method). ~ Alex Citkin, Alexey Muravitsky. #eBook #Logic #Math
• From proof theory to proof assistants (Challenges of responsible software and AI). ~ Klaus Mainzer. #ITP #Coq #AI
• A shorter compiler correctness proof for language IMP. ~ Pasquale Noce. #ITP #IsabelleHOL
• Isabelle community conventions. #ITP #IsabelleHOL
• FindFacts: Experimental search platform for Isabelle and the AFP./# #ITP #IsabelleHOL
• Isabelle quick access links. #ITP #IsabelleHOL
• HMock: first rate mocks in Haskell. ~ Chris Smith. #Haskell #FunctionalProgramming
• A new kind of programming: Tactic metaprogramming in Haskell. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Testing smart contracts with QuickCheck. ~ John Hughes. #Haskell #FunctionalProgramming
• Lift unliftable (and unlift liftable). ~ Veronika Romashkina. #Haskell #FunctionalProgramming
• Algebras for weighted search. ~ Donnacha Oisín Kidney, Nicolas Wu. #Haskell #FunctionalProgramming
• Competitive programming in Haskell: folding folds. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Molecular dynamic simulations in Haskell. ~ Sascha Bubeck. #Haskell #FunctionalProgramming
• Mathematicians welcome computer-assisted proof in ‘grand unification’ theory. ~ Davide Castelvecchi. #ITP #LeanProver #Mat
• Formal verification of composable security proofs. ~ Seyed Reza Sefidgar. #PhDThesis #ITP #IsabelleHOL
• An alternative axiomatic presentation of Nelson algebras. ~ Juan Manuel Cornejo, Andrés Gallardo, Luiz Monteiro, Ignacio Viglizzo. #ATP #Prover9 #Mace4 #Math
• La gran familia de los números. ~ Raúl Ibáñez. #Matemáticas
• Computer says ‘I don’t know’ (The case for Honest AI). ~ Peter Flach. #AI via @hakankj
• Finite abstract algebra in Haskell. ~ Ben Selfridge. #Haskell #FunctionalProgramming #Math
• Undecidability and incompleteness of second-order logic. ~ Mark Koch. #ITP #Cog #Logic #Math
• Integration verification across software and hardware for a simple embedded system. ~ A. Erbsen, S. Gruetter, J. Choi, C. Wood, A. Chlipala. #ITP #Coq
• Don’t mind the formalization gap: The design and usage of Hs-to-Coq. ~ Antal Spector-Zabusky. #PhD_Thesis #ITP #Coq #Haskell #FunctionalProgramming
• Hybrid systems verification with Isabelle/HOL: Simpler syntax, better models, faster proofs. ~ Simon Foster, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth. #ITP #IsabelleHOL
• Median heaps in Haskell. ~ Micah Cantor. #Haskell #FunctionalProgramming
• Theorem proving and Artificial Intelligence (A brief introduction). ~ Josef Urban. #ATP #ITP #AI #MachineLearning
• Towards a human-like reasoning system. ~ Mateja Jamnik. #ATP #AI
• Mathematical reasoning in humans. ~ Jay McClelland. #AI #Math
• From Hammer to Scalpel: Progress in Automated Theorem Proving. ~ Markus Rabe. #ATP #AI
• Training a first-order theorem prover from synthetic data. ~ Vlad Firoiu et als. #ATP #AI #MachineLearning
• Training a first-order theorem prover from synthetic data. ~ Vlad Firoiu et als. #ATP #AI #MachineLearning
• Proof artifact co-training for theorem proving with language models. ~ Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas Polu. #ITP #LeanProver #MachineLearning
• Neural theorem proving in Lean using proof artifact co-training and language models. ~ Jesse Michael Han. #ITP #LeanProver #MachineLearning
• Video series “Haskell by Example”. ~ Michael Oswald. #Haskell #FunctionalProgramming
• Formalisation du théorème de décomposition de Hahn avec le démonstrateur interactif Isabelle. ~ Marie Cousin. #ITP #IsabelleHOL #Math
• Synthetic completeness for a terminating Seligman-Style tableau system. ~ Asta Halkjær From. #ITP #IsabelleHOL #Logic #Math
• Teaching computers about numbers. ~ Kevin Buzzard . #ITP #LeanProver #Math
• Towards a verified compiler from Cogent to LLVM. ~ Harrison Jay Scott. #BsC_Thesis #ITP #Coq
• Birkhoff’s completeness theorem for multi-sorted algebras formalized in Agda. ~ Andreas Abel. #ITP #Agda #Math
• Global optimisation with constructive reals. ~ Dan R. Ghica, odd Waugh Ambridge. #ITP #Agda #Math
• Haskell and the elegant attack. ~ Tony Day. #Haskell #FunctionalProgramming
• Demostración del teorema de Cantor-Schröder-Bernstein. ~ Urtzi Buijs. #Matemáticas
• The fixed point. ~ Rebecca Skinner. #Haskell #FunctionalProgramming
• What the rec? Types dependent on terms, Lean eliminators, and threshold concepts. ~ Gihan Marasingha. #ITP #LeanProver
• Practical Haskell use cases. #Haskell #FunctionalProgramming
• Introducing Haskell in Soisy. ~ Marco Perone. #Haskell #FunctionalProgramming
• Programming puzzles. ~ Tal Schuster, Ashwin Kalyan, Oleksandr Polozov, Adam Tauman Kalai. #Programming #Python
• Python Programming Puzzles (P3). #Programming #Python
• Des bibliothèques aux logiciels: une histoire d’amour! ~ Sabrina Granger. #Programming
• Jornada sobre Inteligencia Artificial de los Institutos de Investigación de la Universidad de Zaragoza. #IA
• Certified quantum computation in Isabelle/HOL. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL
• Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. ~ Julien Narboux, Viviane Durand-Guerrier. #ITP #Coq #Math
• A framework for certified program synthesis. ~ Yasunari Watanabe. #PhDThesis #ITP #Coq
• Learning to guide a saturation-based theorem prover. ~ Ibrahim Abdelaziz et als. #ATP #MachineLearning
• Learning set theory through Coq (part 1). ~ Kyle Stemen. #ITP #Coq #Math
• Learning set theory through Coq (part 2). ~ Kyle Stemen. #ITP #Coq #Math
• Learning set theory through Coq (part 3). ~ Kyle Stemen. #ITP #Coq #Math
• Formally verified convergence of policy-rich DBF routing protocols. ~ Matthew L. Daggitt, Timothy G. Griffin. #ITP #Agda
• Teaching a HOL course: experience report. ~ Konrad Slind et als. #ITP #HOL4
• Why A.I. Moonshots Miss (Ambitious predictions about the future powers of computers keep turning out to be wrong). ~ Jeffrey Funk, Gary Smith. #AI
• Online machine learning techniques for Coq: a comparison. ~ #ITP #Coq #MachineLearning
• Learning proofs for the classification of nilpotent semigroups. ~ Carlos Simpson. #ATP #MachineLearning #Math
• Re-inventing the Monad wheel. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
• Why Kleisli arrows matter. ~ Douglas M. Auclair (geophf). #Haskell #FunctionalProgramming
• TypeFunc: This repository collects some links and resources for learning about type theory, functional programming, and related subjects. ~ Avatar William DeMeo. #ITP #FunctionalProgramming #Agda #Coq #Haskell #Idris #LeanProver #Scala
• Roger Penrose explains Godel’s incompleteness theorem in 3 minutes. #Logic #Math
• Half a year of the Liquid Tensor Experiment: Amazing developments. ~ Peter Scholze. #ITP #LeanProver #Math
• A formalization of dynamic epistemic logic. ~ Paula Neeley. #ITP #LeanProver #Logic
• Verified quadratic virtual substitution for real arithmetic. ~ Matias Scharager, Katherine Cordwell, Stefan Mitsch, André Platzer. #ITP #IsabelleHOL #Logic #Math
• Verifying value iteration and policy iteration in Coq. ~ David M. Masters. #MSc_Thesis #ITP #Coq #MachineLearning
• A toolbox for mechanised first-order logic. ~ Johannes Hostert, Mark Koch, Dominik Kirst. #ITP #Coq #Logic #Math
• The role of entropy in guiding a connection prover. ~ Zsolt Zombori, Josef Urban, Miroslav Olšák. #ATP #MachineLearning
• Declaration groups: where order of declarations suddenly matters in Haskell. ~ Artyom Kazak. #Haskell #FunctionalProgramming
• Final tagless encodings have little to do with typeclasses. ~ Ben Levy. #Haskell #FunctionalProgramming
• Getting started with Haskell projects using Scotty. ~ Juan Pedro Villa Isaza. #Haskell #FunctionalProgramming
• Phantom types and globbing bugs. ~ Patrick Brisbin. #Haskell #FunctionalProgramming
• Probability for Slay the Spire fanatics. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming #Math
• Bach as mathematician. ~ David H Bailey. #Math #Music #Bach
• El Teorema de Cantor-Schröder-Bernstein. ~ Urtzi Buijs @archimedestub. #Lógica #Matemática
• Mathematicians identify threshold at which shapes give way. ~ Mordechai Rorvig. #Math
• Using dependent types to write proofs in Haskell. ~ Jan Mas Rovira. #Haskell #FunctionalProgramming #Logic
• Functional Programming – the True Silver Bullet. ~ Ilya Suzdalnitski. #FunctionalProgramming
• How a simple arithmetic puzzle can guide discovery. ~ Pradeep Mutalik. #Math
• Relations in Lean. ~ Gihan Marasingha. #ITP #LeanProver #Math
• Decidable propositions I. ~ Gihan Marasingha. #ITP #LeanProver #Math
• Decidable propositions II. ~ Gihan Marasingha. #ITP #LeanProver #Math
• Decidable propositions III. ~ Gihan Marasingha. #ITP #LeanProver #Math
• Vectors and dependent function types. ~ Gihan Marasingha. #ITP #LeanProver #Math
• The limits of computation. ~ A. Powell. #CompSci #LambdaCalculus #TypeTheory
• Practical normalization by evaluation for EDSLs. ~ N. Valliappan, A. Russo, S. Lindley. #Haskell #FunctionalProgramming
• Hook: An embedded domain-specific language for fusing implicit interactions to explicit event handlers. ~ Tomoki Shibata, Usamatthew Ahrens, Usarobert J.K. Jacob. #Haskell #FunctionalProgramming
• Some axioms for mathematics. ~ Frédéric Blanqui et als. #Logic #Math
• Set of support, demodulation, paramodulation: a historical Perspective. ~ Maria Paola Bonacina. #ATP #Logic #Math
• Lifting the exponent. ~ Jakub Kądziołka. #ITP #IsabelleHOL #Math