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