Resumen de lecturas compartidas durante julio de 2021

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

• Formalisation of interval methods for nonlinear root-finding. ~ Daniel Seidl. #BSc_Thesis #ITP #IsabelleHOL #Math
• New algebraic normative theories for ethical and legal reasoning in the LogiKEy framework. ~ Ali Farjami. #ITP #IsabelleHOL
• The categorical origin of monads in Haskell. ~ Marien Matser. #BSc_Thesis #Haskell #FunctionalProgramming #CategoryTheory
• What separates AI from an idiot savant is common sense: Hector Levesque. #AI #KRR
• Computer theorem prover verifies sophisticated new result. ~ David H Bailey. #ITP #ATP #Math #AI
• Ethical AI for Social Good. ~ Ramya Akula, Ivan Garibay. #AI
• Composable data validation with Haskell. ~ Ben Levy, Christian Charukiewicz. #Haskell #FunctionalProgramming
• Ode to a streaming ByteString (Or: lazy I/O without shooting yourself in the foot). ~ Patrick Thomson. #Haskell #FunctionalProgramming
• Strictness of foldr’ from containers. ~ Marcin Szamotulski. #Haskell #FunctionalProgramming
• Formalization of Gambler’s Ruin Problem in Isabelle/HOL. ~ Zibo Yang. #ITP #IsabelleHOL #Math
• Formalization of RBD-based Cause Consequence Analysis in HOL. ~ Mohamed Abdelghany, Sofiene Tahar. #ITP #HOL4
• Inductive Benchmarks for Automated Reasoning. ~ Márton Hajdu, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, Andrei Voronkov. #ATP
• Formalizing the Gromov-Hausdorff Space. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
• Formalizing rotation number and its properties in Lean. ~ Yury Kudryashov. #ITP #LeanProver #Math
• Scalar actions in Lean’s Mathlib. ~ Eric Wieser. #ITP #LeanProver #Math
• A formalization of the (compositional) Z property. ~ Flávio L. C. de Moura,a Leandro O. Rezende. #ITP #Coq
• Confluence via the Z property in Coq. ~ Flávio L. C. de Moura, Leandro O. Rezende. #ITP #Coq
• The who in explainable AI: How AI background shapes perceptions of AI explanations. ~ Upol Ehsan, Samir Passi, Q. Vera Liao, Larry Chan, I-Hsiang Lee, Michael Muller, Mark O. Riedl. #AI #XAI
• The QED Manifesto. #ATP #ITP
• Proof assistant makes jump to big-league Math. ~ Kevin Hartnett. #ITP #LeanProver #Math
• Integrating an automated prover for projective geometry as a new tactic in the Coq proof assistant. ~ Nicolas Magaud. #ITP #Coq #Math
• Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? ~ Zoltán Kovács, Tomás Recio, Robert Vajda, M. Pilar Vélez. #GeoGebra #Math
• Is computer algebra ready for conjecturing and proving geometric inequalities in the classroom? [Slides] ~ Zoltán Kovács, Tomás Recio, Robert Vajda, M. Pilar Vélez. #GeoGebra #Math
• A formalization of properties of continuous functions on closed intervals. ~ Yaoshun Fu, Wensheng Yu. #ITP #Coq #Math
• Formal analysis in Coq. #ITP #Coq #Math
• GeoLogic – Graphical interactive theorem prover for Euclidean geometry. ~ Miroslav Olsak. #ITP #Logic #Math
• GeoLogic: Tool for euclidean geometry aware of logic. ~ Miroslav Olsak. #ITP #Logic #Math
• Case studies in formal reasoning about lambda-calculus: Semantics, Church-Rosser, standardization and HOAS. ~ Lorenzo Gheri, Andrei Popescu. #ITP #IsabelleHOL
• An introduction to the Naproche natural language proof checker. ~ Peter Koepke. #ITP #IsabelleHOL #Naproche #Logic #Math
• Intuitionistic epistemic logic in Coq. ~ Christian Albert Hagemeier. #BSc_Thesis #ITP #Coq #Logic
• What does saying that ‘Programming is hard’ really say, and about whom? ~ Brett A. Becker. #Programming
• Formalization in Lean of IMO 2021 Q1. ~ Mantas Baksys. #ITP #LeanProver #Math #IMO
• Formalizing Galois theory (in Lean). ~ Thomas Browning, Patrick Lutz. #ITP #LeanProver #Math
• Hakyll how-to: pages without source files. ~ Fraser Tweedale. #Haskell #FunctionalProgramming
• Why math is an art, not a science. ~ Peter Flom. #Math
• Combinatorics in Lean. ~ Bhavik Mehta. #ITP #LeanProver #Math
• First-order languages and structures in Lean. ~ Aaron Anderson, Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Logic #Math
• Schur–Zassenhaus theorem in Lean. ~ Thomas Browning. #ITP #LeanProver #Math
• Univalence from a computer science point-of-view. ~ Dan Licata. #Logic #Math #CompSci
• Haskell (The most gentle introduction ever). ~ Mateusz Podlasin. #Haskell #FunctionalProgramming
• A comparison of the mathematical proof languages Mizar and Isar. ~ Freek Wiedijk, Markus Wenzel. #ITP #Mizar #IsabelleHOL #Isar
• The mathematical vernacular. ~ Freek Wiedijk. #ITP #Mizar #IsabelleIsar
• The Krein-Milman theorem in Lean. ~ Yaël Dillies. #ITP #LeanProver #Math
• Sets and logic in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Logic #Math
• Functions and equivalence relations in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Logic #Math
• A computer verified, monadic, functional implementation of the integral. ~ Russell O’Connor, Bas Spitters. #ITP #Coq #Math
• Static analysis using Haskell and Datalog. ~ Luc Tielen. #Haskell #FunctionalProgramming
• foralls in Data Types. ~ Brandon Chinn. #Haskell #FunctionalProgramming
• Every group is a McCune group (in Lean). ~ Bhavik Mehta. #ITP #LeanProver #Math
• Balancing automation and control for formal verification of microprocessors. #ITP #ACL2
• Learning theorem proving components. ~ Karel Chvalovský, Jan Jakubův, Miroslav Olšák, Josef Urban. #ATP #MachineLearning
• Connecting constructive notions of ordinals in Homotopy Type Theory. ~ Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu. #HoTT #ITP #Agda #Logic #Math
• Artificial intelligence (A textbook). ~ Charu C. Aggarwal.3#v=onepage&q&f=false #eBook #AI
• Announcing a new newsletter on mechanizing mathematics. ~ Michael Harris. #ITP #ATP #Math
• Silicon Reckoner: an opinionated newsletter about the implications of mechanization of mathematics. ~ Michael Harris. #ITP #ATP #Math
• IsaSAT and Kissat entering the EDA Challenge 2021. ~ Mathias Fleury. #ITP #IsabelleHOL #SATSolvers
• Waterproof: an educational environment for writing mathematical proofs in interactive notebooks. #ITP #Coq #Math
• Measure theory in Waterproof (Interactive theorem-proving for measure theory in an educational setting). ~ Jan Moraal. #ITP #Coq #Math
• Compositional optimizations for CertiCoq. ~ Zoe Paraskevopoulou, John M. Li, Andrew W. Appel. #ITP #Coq
• Noetherian induction for computer-assisted first-order reasoning. ~ Sorin Stratulat. #ITP #Coq #Logic #Math
• Verification of linked data structures in Dafny. ~ Jorge Blázquez Saborido. #TFG #ATP #SMT #Dafny
• Probability tree diagrams. Recursion schemes. Why finding the right solution is sometimes hard? ~ Robert Peszek. #Haskell #FunctionalProgramming
• Purely-functional reverse-mode automatic differentiation with delimited continuations. ~ Marco Zocca. #Haskell #FunctionalProgramming
• Proceedings of ICML 2021 workshop on theoretic foundation, criticism, and application trend of explainable AI. #AI #MachineLearning #XAI
• Publishing articles and books with Org Mode export. ~ Peter Prevos. #Emacs #OrgMode #LaTeX
• The Hales-Jewett theorem (in Lean). ~ David Wärn. #ITP #LeanProver #Math
• Emacs, el editor de texto libre con vocación de sistema operativo: sus ‘extensiones’ más usadas suplen toda clase de aplicaciones. ~ Marcos Merino. #Emacs
• Of all the programming languages in the world, why Haskell? ~ Charles Hoskinson. #Haskell #FunctionalProgramming #Cardano
• Emacs Application Framework (EAF). #Emacs
• Incremental vulnerability detection via back-propagating symbolic execution of insecurity separation logic. ~ Toby Murray, Pengbo Yan, Gidon Ernst. #ITP #IsabelleHOL
• Integrating an automated prover for projective geometry as a new tactic in the Coq proof assistant. ~ Nicolas Magaud. #ITP #Coq #Math
• Reasoning on figures of theoretical geometry theorems. ~ Eirini Vandorou. #MSc_Thesis #Clojure #FunctionalProgramming #Prolog #LogicProgramming #Math
• Hspec hooks. ~ Matt Parsons. #Haskell #FunctionalProgramming
• Distributing intersection and union types with splits and duality (Functional pearl). ~ Xuejing Huang, Bruno C.D.S. Oliveira. #Haskell #FunctionalProgramming
• A defense of logicism. ~ Hannes Leitgeb, Uri Nodelman, Edward N. Zalta. #Logic #Math
• Facilitating meta-theory reasoning. ~ Giselle Reis. #Logic #CompSci #SELLF #TATU #QUATI #OCaml #FunctionalProgramming
• Touring the MetaCoq project. ~ Matthieu Sozeau. #ITP #Coq
• Automating induction by reflection. ~ Johannes Schoisswohl, Laura Kovács. #ATP #Logic
• Automated induction by reflection. ~ Johannes Schoisswohl. #MSc_Thesis #ATP #Logic
• Countability of inductive types formalized in the object-logic level. ~ Qinxiang Cao, Xiwei Wu. #ITP #Coq
• SMLtoCoq: Automated generation of Coq specifications and proof obligations from SML programs with contracts. ~ Laila El-Beheiry, Giselle Reis, Ammar Karkour. #ITP #Coq #SML #FunctionalProgramming
• Systematic translation of formalizations of type theory from intrinsic to extrinsic style. ~ Florian Rabe, Navid Roux. #MMT #LogicalFramework
• A reinforcement learning environment for mathematical reasoning via program synthesis. ~ Joseph Palermo, Johnny Ye, Alok Singh. #AI #MachineLearning #Math
• Explainable AI: current status and future directions. ~ Prashant Gohel, Priyanka Singh, Manoranjan Mohanty. #XAI #AI #MachineLearning
• Cheap interpreter, part 4: stack machines. ~ Gary Verhaegen. #Haskell #FunctionalProgramming
• Haskell series part 1. ~ Pierre Guillemot. #Haskell #FunctionalProgramming
• Template Haskell performance tips. ~ Matt Parsons. #Haskell #FunctionalProgramming
• Artificial Intelligence, Robotics & Data Science (CSIC Scientific Challenges: Towards 2030, Volume 11). #AI #DataScience #MachineLearning
• Copilot, el asistente de AI de GitHub recibió fuertes críticas de la comunidad open source. ~ Darkcrizt. #AI #Copilot #Programación
• HR’s role in understanding and mitigating AI bias. ~ Laura Baldwin. #AI
• (Risp (in (Rust) (Lisp))). ~ Stepan Parunashvili. #Rust #Lisp
• Writing an (overly) idiomatic Fizzbuzz with Rust. ~ Ryan Frazier. #RustLang
• Is Rust used safely by software developers? ~ Ana Nora Evans, Bradford Campbell, Mary Lou Soffa. #RustLang
• Explainability and auditability in ML: Definitions, techniques, and tools. ~ Ejiro Onose. #AI #MachineLearning #XAI
• Reinforcement learning for interactive theorem proving (Creating an artificial student). ~ Jolijn Cottaar. #ITP #Coq #MachineLearning
• Game development in Haskell. ~ Jan Rychlý. #BSc_Thesis #Haskell #FunctionalProgramming
• A mechanised proof of the time invariance thesis for the weak call-by-value λ-calculus. ~ Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke. #ITP #Coq #CompSci
• A classification of artificial intelligence systems for mathematics education. ~ Steven Van Vaerenbergh, Adrián Pérez-Suay. #AI #Math
• GHC: Dependency analysis of Haskell declarations. ~ Artyom Kuznetsov. #Haskell #FunctionalProgramming
• Finitely generated abelian groups (in Isabelle/HOL). ~ Joseph Thommes, Manuel Eberl. #ITP #IsabelleHOL #Math
• Formalizing the Gromov-Hausdorff space. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
• A flexible approach to argumentation framework analysis using theorem proving. ~ David Fuenmayor, Alexander Steen.f#page=26 #ITP #IsabelleHOL
• Express: Applications of dynamically typed Haskell expressions. ~ Rudy Matela. #Haskell #FunctionalProgramming
• Learning about proof with the theorem prover Lean: the abundant numbers task. ~ Athina Thoma, Paola Iannone. #ITP #LeanProver #Math
• Haskell books: a tagged index of English books related to the Haskell programming language. ~ Travis Cardwell. #Haskell #FunctionalProgramming
• General automation in Coq through modular transformations. ~ Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial. #ITP #Coq
• Synthetic undecidability of MSELL via FRACTRAN mechanised in Coq. ~ Dominique Larchey-Wendling. #ITP #Coq
• Type-theoretic constructions of the final coalgebra of the finite powerset functor. ~ Niccolò Veltri. #ITP #Agda
• Alethe: Towards a generic SMT proof format. ~ Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine. #ATP #SMT
• Conjectures, tests and proofs: An overview of theory exploration. ~ Moa Johansson, Nicholas Smallbone. #Haskell #FunctionalProgramming #QuickSpec
• A framework for proof-carrying logical transformations. ~ Quentin Garchery. #FunctionalProgramming #OCaml #Why3
• Isabelle’s metalogic: Formalization and proof checker. ~ Tobias Nipkow, Simon Roßkopf.f#page=104 #ITP #IsabelleHOL
• Reliable reconstruction of fine-grained proofs in a proof assistant. ~ Hans-Jörg Schurr, Mathias Fleury, Martin Desharnais.f#page=459 #ATP #SMT #ITP #IsabelleHOL
• The Isabelle/Naproche natural language proof assistant. ~ Adrian De Lon et als.f#page=619 #ITP #IsabelleHOL
• Turing machines in Lean. ~ Mario Carneiro et als. #ITP #LeanProver #CompSci
• Exploring linear Traversable using generics. ~ Sjoerd Visscher. #Haskell #FunctionalProgramming
• What OpenAI and GitHub’s “AI pair programmer” means for the software industry. ~ Ben Dickson. #AI #Programming #Copilot
• Using AI to Drill Down in Physics. ~ Bennie Mols. #AI
• Matemáticas dinámicas: estupendas visualizaciones a partir de código abierto. ~ @Alvy. #Matemáticas #Computación
• Dynamic mathematics (Interactive mathematical applets & animations). ~ Juan Carlos Ponce. #Math
• Formalización del teorema de existencia de modelo en Isabelle/HOL. ~ Sofı́a Santiago Fernández. #TFM #ITP #IsabelleHOL #Lógica #Matemática
• Formalized signature extension results for confluence, commutation and unique normal forms. ~ A. Lochmann, F. Mitterwallner, A. Middeldorp. #ITP #IsabelleHOL
• Answers to some open questions of Ulrich & Meredith. ~ Matthew Walsh, Branden Fitelson. #ATP #Otter #Logic #Math
• SpecCheck: Specification-based testing for Isabelle/ML. ~ Kevin Kappelmann, Lukas Bulwahn. #ITP #IsabelleHOL
• Coq meets CλaSH (Proposing a hardware design synthesis flow that combines proof assistants with functional hardware description languages). ~ Fritjof Bornebusch. #PhD_Thesis #ITP #Coq
• Models for software verification: Proving program correctness. ~ Boro Sitnikovski, Lidija Goracinova-Ilieva, Biljana Stojcevska. #FormalVerification #Coq #Dafny
• Using LSTM to predict tactics in Coq. ~ X. Luan, X. Zhang, M. Sun. #ITP #Coq #MachineLearning #NeuralNetwork
• A theory of higher-order subtyping with type intervals. ~ Sandro Stucki, Paolo G. Giarrusso. #ITP #Agda
• Curry-Howard correspondence: An intuitive language for mathematics. ~ Xiao Tan. #MSc_Thesis #Logic #CompSci
• Practical suggestions for mathematical writing. ~ R. Bell, B. Kadets, P. Srinivasan, N. Triantafillou, I. Vogt. #Math
• Complementing the digital programming tutor Ask-Elle with program synthesis. ~ Gustav Engsmyre, Karl Wikström. #MSc_Thesis #Haskell #FunctionalProgramming
• Code Lean contenant les preuves d’un cours standard sur les espaces métriques. ~ Frederic Le Roux. #ITP #LeanProver #Math
• Function application: Using the dollar sign ($). ~ James Bowen. #Haskell #FunctionalProgramming
• A brief introduction to Template Haskell. ~ Heitor Toledo Lassarote de Paula. #Haskell #FunctionalProgramming
• Will AI rewrite coding? ~ Samuel Greengard. #AI
• Groups I. Omar Harhara. #ITP #LeanProver #Math
• Chinese remainder encoding for hamiltonian cycles [Slides]. ~ Marijn Heule. #ATP #SATSolvers #Math
• Chinese remainder encoding for hamiltonian cycles [Video]. ~ Marijn Heule. #ATP #SATSolvers #Math
• DiMo: Discrete modelling using propositional logic [Slides]. ~ Norbert Hundeshagen, Martin Lange and Georg Siebert. #Logic #Math
• DiMo: Discrete modelling using propositional logic [Video]. ~ Norbert Hundeshagen, Martin Lange and Georg Siebert. #Logic #Math
• DiMo: A tool for discrete modelling using propositional logic (version 0.2.2). ~ Martin Lange. #Logic #Math
• Verifying correctness of Haskell programs using the programming language Agda and framework agda2hs. ~ Dixit Sabharwal, Jesper G.H. Cockx, Lucas F.B. Escot. #ITP #Agda #Haskell #FunctionalProgramming
• Security verification in the context of 5G sensor networks. ~ Piotr Remlein, Urszula Stachowiak. #Haskell #FunctionalProgramming
• Deriving a symbolic executor for definitional interpreters suitable for the study of heuristics. ~ Laura-Ana Pîrcalaboiu, Casper Bach Poulsen, Cas van der Rest. #Haskell #FunctionalProgramming
• Goodbye C developers: The future of programming with certified program synthesis. ~ Kiran Gopinathan. #ITP #Coq
• Certifying the synthesis of heap-manipulating programs. ~ Y. Watanabe, K. Gopinathan, George Pîrlea, Nadia Polikarpova, I. Sergey. #ITP #Coq
• Formalizing higher-order termination in Coq. ~ Deivid Vale, Niels van der Weide.f#page=71 #ITP #Coq
• Formalization of a sign determination algorithm in real algebraic geometry. ~ Cyril Cohen. #ITP #Coq #Math
• The Cantor-Schröder-Bernstein for homotopy types, or ∞-groupoids, in Agda. ~ Martin Escardo. #ITP #Agda #Logic #Math
• The Cantor–Schröder–Bernstein Theorem for ∞-groupoids. ~ Martin Escardo. #Logic #Math
• Practical verification of the Haskell ranged-sets library. ~ Ioana Savu, Jesper Cockx, Lucas Escot. #ITP #Agda #Haskell #FunctionalProgramming
• Producing a verified implementation of sequences using agda2hs. ~ Shashank Anand, Jesper Cockx, Lucas Escot. #ITP #Agda #Haskell #FunctionalProgramming
• Reflective programs in tree calculus. ~ Barry Jay. #eBook #ITP #Coq
• Proofs in Coq for the book “Reflective programs in tree calculus”. ~ Barry Jay. #ITP #Coq
• A tutorial implementationof a dependently typed lambda calculus. ~ Andres Löh, Conor McBride, Wouter Swierstra. #ITP #Agda
• Formalising contemporary mathematics in simple type theory. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• Isabelle’s metalogic: Formalization and proof checker. ~ Tobias Nipkow, Simon Roßkopf. #ITP #IsabelleHOL
• Arming polysemy with Arrows. ~ Robert Peszek. #Haskell #FunctionalProgramming
• Functors and monads for people who have read too many “Tutorials”. ~ Jeremy Bowers. #Haskell #FunctionalProgramming