Esta entrada es una recopilación de lecturas compartidas, durante abril de 2024, en Mastodon fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Mastodon.

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.

• Mechanised uniform interpolation for modal logics K, GL, and iSL. ~ Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito. #ITP #Coq #Logic
• Solving quantified modal logic problems by translation to classical logics. ~ Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller. #ATP #Logic
• Type inference for Isabelle2Cpp. ~ Dongchen Jiang, Chenxi Fu. #ITP #IsabelleHOL

• Experiments in the irrationality of Sqrt 2 with SMT. ~ Philip Zucker (@sandmouth@types.pl). #ATP #SMT #Math

• Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv, Cezary Kaliszyk. #ATP #Prover9

• Serokell’s Work on GHC: Dependent types, Part 3. #FunctionalProgramming #Haskell

• The number of primitive words of unbounded exponent in the language of an HD0L-system is finite. ~ Karel Klouda, Štěpán Starosta. #ITP #IsabelleHOL

• Error credits: Resourceful reasoning about error bounds for higher-order probabilistic programs. ~ Alejandro Aguirre et als. #ITP #Coq

• On the systematic creation of faithfully rounded commutative truncated booth multipliers. ~ Theo Drane, Samuel Coward, Mertcan Temel, Joe Leslie-Hurd. #ITP #ACL2

• Stalnaker's epistemic logic in Isabelle/HOL. ~ Laura P. Gamboa Guzman, Kristin Y. Rozier. #ITP #IsabelleHOL

• Embedding differential dynamic logic in PVS. ~ J. Tanner Slagel, Mariano Moscato, Lauren White, César A. Muñoz, Swee Balachandran, Aaron Dutle. #ITP #PVS
• Formalizing factorization on euclidean domains and abstract euclidean algorithms. ~ Thaynara Arielly de Lima, Andréia Borges Avelar, André Luiz Galdino, Mauricio Ayala-Rincón. #ITP #PVS #Math

• Computing education in the era of generative AI. ~ Paul Denny et als. #AI #Education

• Human-machine collaboration in the teaching of proof. ~ Gila Hanna, Brendan Larvor, Xiaoheng Kitty Yan. #ITP #Lean4 #Math

• LiberAbaci: Teaching mathematics with the help of Coq. #ITP #Coq #Math
• Benefits of functional programming. ~ Ada Beat. #FunctionalProgramming

• Mathematics and computation. ~ Avi Wigderson. #eBook #Math #CompSci

• Using the proof assistant Lean in undergraduate mathematics classrooms. ~ Brendan Larvor, Gila Hanna, Xiaoheng Yan. #ITP #Lean4 #Math

• Teaching divisibility and binomials with Coq. ~ Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin. #ITP #Coq #Math
• Compfiles: Catalog of math problems formalized in Lean. ~ David Renshaw (@david@social.wub.site) et als. #ITP #Lean4 #Math #IMO
• Lean 99: Ninety-nine Lean problems. ~ Kitamado. #FunctionalProgramming #Lean4
• Getting your Haskell executable statically linked with Nix. ~ Tom Sydney Kerckhove. #FunctionalProgramming #Haskell #Nix

• A note about coercions. ~ Oleg Grenrus (@phadej). #FunctionalProgramming #ITP #Agda

• Chain Bounding and the leanest proof of Zorn's lemma. ~ Guillermo L. Incatasciato, Pedro Sánchez Terraf. #ITP #Lean4 #Math

• Formalization of derived categories in Lean/mathlib. ~ Joël Riou. #ITP #Lean4 #Math #CategoryTheory
• Effective parallel formal verification of reconfigurable discrete-event systems formalizing with Isabelle/HOL. ~ Sohaib Soualah, Mohamed Khalgui & Allaoua Chaoui. #ITP #IsabelleHOL
• Can language models solve olympiad programming? ~ Quan Shi et als. #LLMs #Programming
• AI index: State of AI in 13 charts. ~ Shana Lynch. #AI

• Cyc: history's forgotten AI project. ~ I. A. Fisher. #AI

• The formal verification of the ctm approach to forcing. ~ Emmanuel Gunther et als. #ITP #Isabelle #Math

• A verified proof checker for metric first-order temporal logic. ~ Andrei Herasimau, Jonathan Julian Huerta y Munive, Leonardo Lima, Martin Raszyk, Dmitriy Traytel. #ITP #IsabelleHOL
• Applying large language models to enhance the assessment of parallel functional programming assignments. ~ Skyler Grandel, Douglas C. Schmidt, Kevin Leach. #FunctionalProgramming #LLMs #ChatGPT
• Two announcements: AI for Math resources, and erdosproblems.com. ~ Terence Tao (@tao@mathstodon.xyz). #AI #Math

• Why engineers should study Philosophy. ~ Marco Argenti. #AI #Philosophy

• Core inspection. ~ Oleg Grenrus. #Haskell #FunctionalProgramming

• Why streaming is my favourite Haskell streaming library. ~Jack Kelly. #FunctionalProgramming #Haskell

• ViCAR: Visualizing categories with automated rewriting in Coq. ~ Bhakti Shah et als. #ITP #Coq

• Symbolic computation for all the fun. ~ Chad E. Brown, Mikoláš Janota, Mirek Olšák. #AIMO #ATP #SMT #Math
• Towards a certified proof checker for deep neural network verification. ~ Remi Desmartin et als. #ITP #Imandra #DeepLearning
• A survey on deep learning for theorem proving. ~ Zhaoyu Li et als. #ITP #DeepLearning

• Category theory (Course notes). ~ Domini Corchard, Marco Paviotti. #CategoryTheory

• Exact arithmetic on the Stern–Brocot tree. ~ Milad Niqui (2007). #ITP #Coq #Math

• The Haskell Unfolder Episode 23: specialisation. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming
• History of Lisp. ~ John McCarthy (1979). #Lisp

• The algorithms (Open source resource for learning data structures & algorithms and their implementation in any programming language). ~ @The_Algorithms. #Algorithms #Programming

• Logic in mathematics and computer science. ~ Richard Zach (@rrrichardzach@mathstodon.xyz). #Logic #Math #CompSci

• IsaRare: Automatic verification of SMT rewrites in Isabelle/HOL. ~ Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds, Haniel Barbosa, Andres Nötzli, Clark Barrett & Cesare Tinelli. #ITP #IsabelleHOL #SMT
• Protein folding by recursive backtracking. ~ Bjørn Kjos-Hanssen. #ITP #Lean4
• Live verification in an interactive proof assistant. ~ Samuel Gruetter, Viktor Fukala, Adam Chlipala. #ITP #Coq
• A state-of-the-art Karp-Miller algorithm certified in Coq. ~ Thibault Hilaire, David Ilcinkas & Jérôme Leroux. #ITP #Coq
• Foundational integration verification of a cryptographic server. ~ Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel & Adam Chlipala. #ITP #Coq

• Asymptotics for the standard block size in primal lattice attacks: second order, formally verified. ~ Daniel J. Bernstein. #ITP #HOL_Light

• Large-scale formal proof for the working mathematician (lessons learnt from the ALEXANDRIA project). ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math

• Evasiveness through Binary Decision Diagrams. ~ Jesús Aransay, Laureano Lambán, Julio Rubio. #ITP #IsabelleHOL
• Category theory in Isabelle/HOL as a basis for meta-logical investigation. ~ Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott. #ITP #IsabelleHOL
• Isabelle formalisation of original representation theorems. ~ Marco B. Caminati. #ITP #IsabelleHOL #Math
• Formalization quality in Isabelle. ~ Fabian Huch, Yiannos Stathopoulos. #ITP #IsabelleHOL
• Formalizing free groups in Isabelle/HOL: The Nielsen-Schreier theorem and the conjugacy problem. ~ Aabid Seeyal Abdul Kharim et als. #ITP #IsabelleHOL #Math
• Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method. ~ Mohit Tekriwal et als. #ITP #Coq #Math
• Multiple-inheritance hazards in dependently-typed algebraic hierarchies. ~ Eric Wieser. #ITP #LeanProver
• Nominal AC-matching. ~ Mauricio Ayala-Rincón et als. #ITP #PVS
• CoProver: A recommender system for proof construction. ~ Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar. #ITP #PVS
• From foundations to frontiers: Mastering Haskell programming. ~ Byte Sorcery. #Haskell #FunctionalProgramming
• AI for Math resources. ~ Talia Ringer et als. #AI #Math

• Reimagining middle school education: The synergy of AI and Montessori principles (Next-level AI curriculum development). ~ Nick Potkalitsky, Sam Bobo. #AI #Education

• Course: Interactive theorem proving. ~ Jasmin Blanchette et als. #ITP #Lean4

• Mathlib4 tactics. ~ Kitamado. #ITP #Lean4 #Mathlib

• A formal proof for the correctness of tangle learning. ~ Suzanne Ellen van der Veen. #ITP #IsabelleHOL

• Knuth–Morris–Pratt illustrated. ~ Cameron Moy. #FunctionalProgramming #Haskell

• Asymptotic speedup via effect handlers. ~ Daniel Hillerström, Sam Lindley, John Longley. #FunctionalProgramming

• Wu's method can boost symbolic AI to rival silver medalists and AlphaGeometry to outperform gold medalists at IMO geometry. ~ Shiven Sinha et als. #AI #ATP #IMO #Math

• Coq tactics in plain english. ~ Charles Averill. #ITP #Coq
• Formal program verification (Rigorous proof of program correctness and security). ~ Charles Averill. #ITP #Coq
• Ann: ob-coq (A package for Coq developments in Org Mode). ~ Michael Herstine (@unwoundstack). #ITP #Coq #Emacs #OrgMode
• Dyadic Decomposition using Functional lenses. ~ Eduardo Lemos. #Haskell #FunctionalProgramming
• Solving Advent of Code ’23 “Aplenty” by Compiling. ~ Abhinav Sarkar (@abnv@fantastic.earth). #Haskell #FunctionalProgramming
• Neural networks for mathematical reasoning: Evaluations, capabilities, and techniques. ~ Yuhuai Tony Wu. #NeuralNetwork #Reasoning #Math

• Epsilon: Scientific research at your fingertips (Epsilon uses AI to answer research questions with academic literature). #AI

• The mathematics of Prolog. ~ David S Warren. #Prolog #LogicProgramming #Math

• Mechanised hypersafety proofs about structured data: extended version. ~ Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, Ilya Sergey. #ITP #Coq

• Teaching higher-order logic using Isabelle. ~ Simon Tobias Lund, Jørgen Villadsen. #ITP #IsabelleHOL #Logic

• Interactive formal specification for mathematical problems of engineers. ~ Walther Neuper. #ITP #IsabelleHOL
• Uncertainty principle (in Isabelle/HOL). ~ Alexander Treml. #ITP #IsabelleHOL
• Lean into verified software development. ~ Kesha Hietala, Emina Torlak. #ITP #LeanProver
• A Coq library of sets for teaching denotational semantics. ~ Qinxiang Cao, Xiwei Wu, Yalun Liang. #ITP #Coq
• The elements of differentiable programming. ~ Mathieu Blondel, Vincent Roulet. #Math #CompSci
• Evaluation of an LLM in identifying logical fallacies: A call for rigor when adopting LLMs in HCI research. ~ Gionnieve Lim, Simon T. Perrault. #LLMs #Reasoning #Logic
• Reason from fallacy: Enhancing large language models' logical reasoning through logical fallacy understanding. ~ Yanda Li et als. #LLMs #Reasoning #Logic

• Creating a blog. #Emacs #OrgMode #Blog

• From mechanized semantics to verified compilation: the Clight semantics of CompCert. ~ Sandrine Blazy. #ITP #Coq

• A comprehensive specification and verification of the L4 microkernel API. ~ Leping Zhang, Yongwang Zhao, Jianxin Li. #ITP #IsabelleHOL

• Towards trustworthy automated program verifiers: Formally validating translations into an intermediate verification language. ~ Gaurav Parthasarathy et als. #ITP #IsabelleHOL

• Program synthesis from graded types. ~ Jack Hughes, Dominic Orchard. #Haskell #FunctionalProgramming

• The Radon-Nikodým theorem and the Lebesgue-Stieltjes measure in Coq. ~ Yoshihiro Ishiguro, Reynald Affeldt. #ITP #Coq #Math

• GFLean: An autoformalisation framework for Lean via GF. ~ Shashank Pathak. #Lean #Autoformalization #FunctionalProgramming #Haskell

• Alias the current module with Imp. ~ Taylor Fausak. #Haskell #FunctionalProgramming

• Implicit arguments. ~ Oleg Grenrus. #Haskell #FunctionalProgramming

• Combinatorial applications of the compactness theorem. ~ Fabián Fernando Serrano Suárez, Mauricio Ayala-Rincón, Thaynara Arielly de Lima. #ITP #IsabelleHOL

• Certified first-order AC-unification and applications. ~ Mauricio Ayala-Rincón et als. #ITP #PVS
• Isabelle-verified correctness of Datalog programs for program analysis. ~ Anders Schlichtkrull, René Rydhof Hansen, Flemming Nielson. #ITP #IsabelleHOL

• All tactics in mathlib4. ~ Haruhisa Enomoto. #ITP #LeanProver #Mathlib

• Broadcast Psi-calculi (in Isabelle/HOL). ~ Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber. #ITP #IsabelleHOL

• Enhancing formal theorem proving: A comprehensive dataset for training AI models on Coq code. ~ Andreas Florath. #ITP #Coq #LLMs
• Improving the Diproche CNL through autoformalization via Large Language Models. ~ Merlin Carl. #ITP #Diproche #LLMs
• A formal proof of R(4,5)=25. ~ Thibault Gauthier, Chad E. Brown. #ITP #HOL4 #Math
• Using large language models for (de-)formalization and natural argumentation exercises for beginner's students. ~ Merlin Carl. #LLMs #Autoformalization #Logic
• AI Mathematical Olympiad – Progress Prize Competition now open. ~ Terence Tao (@tao@mathstodon.xyz). #AI #Math

• Generative logic, teaching Prolog in art & design. ~ Christian Jendreiko. #Prolog #LogicProgramming

• Resolution proving I. ~ Philip Zucker (@sandmouth@types.pl). #Logic #ATP #Python

• Conditional separation as a binary relation. A Coq assisted proof. ~ Jean-Philippe Chancelier, Michel de Lara , Benjamin Heymann. #ITP #Coq

• How machines can make mathematics more congressive. ~ Eugenia Cheng. #CompSci

• Some thoughts on automation and mathematical research. ~ Akshay Venkatesh. #Math #CompSci
• Mathematics, word problems, common sense, and artificial intelligence. ~ Ernest Davis. #Math #AI #LLMs #GPT
• Abstraction boundaries and spec driven development in pure mathematics. ~ Johan Commelin, Adam Topaz. #Math #ITP #LeanProver
• Strange new universes: Proof assistants and synthetic foundations. ~ Michael Shulman. #Math #ITP #LLMs
• Mathematical reasoning and the computer. ~ Kevin Buzzard. #Math #AI #NeuralNetwork #LLMs #ITP #LeanProver
• Automation compels mathematicians to reflect on our values. ~ Michael Harris. #Math #AI
• Is deep learning a useful tool for the pure mathematician? ~ Geordie Williamson. #Math #AI #DeepLearning
• Mathematics and the formal turn. ~ Jeremy Avigad. #Math #AI #ITP #MachineLearning
• Proof in the time of machines. ~ Andrew Granville. #Math #ITP