Resumen de lecturas compartidas durante abril de 2024
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.f#page=203 #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.f#page=17 #ITP #IsabelleHOL #Math
- Evasiveness through Binary Decision Diagrams. ~ Jesús Aransay, Laureano Lambán, Julio Rubio.f#page=49 #ITP #IsabelleHOL
- Category theory in Isabelle/HOL as a basis for meta-logical investigation. ~ Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott.f#page=81 #ITP #IsabelleHOL
- Isabelle formalisation of original representation theorems. ~ Marco B. Caminati.f#page=110 #ITP #IsabelleHOL #Math
- Formalization quality in Isabelle. ~ Fabian Huch, Yiannos Stathopoulos.f#page=154 #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.f#page=65 #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