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
forall
s 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