Resumen de lecturas compartidas durante noviembre de 2020
Esta entrada es una recopilación de lecturas compartidas, durante noviembre de 2020, 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.
- #ForMatUS: Libro “Ejercicios de lógica proposicional con Lean”. #DAO #LeanProver #Lógica #Matemática #ProgramaciónFuncional
- Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information. ~ Anthony Bordg, Hanna Lachnitt, Yijun He. #ITP #IsabelleHOL
- Formalising ordinal partition relations using Isabelle/HOL. ~ Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL #Math
- Bind the gap (Pilot issue, November 2020). #Haskell #FunctionalProgramming
- Proving theorems with computers. ~ Kevin Buzzard. #ITP #LeanProver #Math
- A formally verified compiler for a simple language with numbers and sums. ~ Jordan Scales. #ITP #LeanProver
- nuha: Multidimensional arrays, linear algebra, numerical analysis. ~ Johannes Kropp. #Haskell #FunctionalProgramming #Math
- An introduction to proof via inquiry-based learning. ~ Dana C. Ernst. #eBook #Logic #Math
- Introduction to infinity categories. (Some notes on a short introductory video on some foundational aspects of infinity categories). ~ Zack Garza. #CategoryTheory
- Gradualizing the Calculus of Inductive Constructions. ~ Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter. #ITP #Coq
- A brief introduction to Smtlink. ~ Carl Kwan. #ITP #ACL2 #SMT #Z3
- Hazel tutor: Guiding novices through type-driven development strategies. ~ Hannah Potter, Cyrus Omar. #FunctionalProgramming
- Hazel: a live functional programming environment featuring typed holes. #FunctionalProgramming
- Formalising ordinal partition relations using Isabelle/HOL. ~ Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence Paulson. #ITP #IsabelleHOL #Math
- Program correctness. ~ Graham Hutton. #Haskell #FunctionalProgramming
- Logic: A study guide — First order logic. ~ Peter Smith. #Logic
- Mathematics for human flourishing. ~ Francis Su. #Book #Math
- A modular Isabelle framework for verifying saturation provers. ~ Sophie Tourret, Jasmin Blanchette. #ITP #IsabelleHOL
- Virtual record fields using lenses. ~ Chris Penner. #Haskell #FunctionalProgramming
- Existential Haskell. ~ Patrick Thomson. #Haskell #FunctionalProgramming
- Haskell in the Real World. ~ Sandy Maguire. #Haskell #FunctionalProgramming
- The history of Standard ML. ~ David Macqueen, Robert Harper, John Reppy. #SML #FunctionalProgramming
- Correctness of a compiler for arithmetic expressions in Lean. ~ Xi Wang. #ITP #LeanProver
- A queue for effectful breadth-first traversals (Part 10 of a 10-part series on breadth-first traversals). ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- hs-to-coq and Data.Sequence. ~ Li-yao Xia. #Haskell #Coq #FunctionalProgramming #ITP
- Intuitionistic logic in Haskell. ~ Isaac van Bakel. #Logic #Haskell
- Theorem proving in Haskell. ~ Isaac van Bakel. #Logic #Haskell #ITP
- Haskell and the Curry-Howard isomorphism (Part 1). ~ Ben Sherman. #Haskell #Logic
- The Curry-Howard correspondence in Haskell. ~ Tim Newsham. #Logic #Haskell
- Adventures in Classical-Land. ~ Dan Piponi.f#page=17 #Logic #Haskell
- Curry-Howard isomorphism down-to-earth. ~ Jannis Grimm. #Logic #Haskell
- A survey into the Curry-Howard isomorphism & type systems. ~ Phillip Mates. #Logic #Haskell
- Lisp books (Most of Lisp books in one place). ~ Vsevolod Dyomkin. #Lisp #Programming
- Two applications of logic programming to Coq. ~ M. Manighetti, D. Miller, A. Momigliano. #ITP #Coq #LogicProgramming
- Untangling mechanized proofs. ~ Clément Pit-Claude. #ITP #Coq
- Coming to terms with your choices: An existential take on dependent types. ~ Georg Stefan Schmid, Olivier Blanvillain, Jad Hamza, Viktor Kunčak. #ITP #Coq #Scala
- Shallowly embedding type theories as presheaf models in Agda. ~ J. Ceulemans, D. Devriese. #ITP #Agda
- List of important publications in mathematics. #Books #Math
- Best math books (A comprehensive reading list). #Book #Math
- Release of the NASA PVS Library (NASALib) v7.1. #ITP #PVS
- BioShake: a Haskell EDSL forbioinformatics workflows. ~ Justin Bedo. #Haskell #FunctionalProgramming
- Common Lisp by Example (A compilation of notes from various sources). ~ Ashok Khanna. #CommonLisp
- Le problème des 8 reines. ~ Maxime Amblard. #Algorithms via @interstices_eu
- Certified optimisation of stream operations using heterogeneous staging. ~ J. Lowenthal, J. Yallop. #ITP #Agda
- Verifying replicated data types with typeclass refinements in Liquid Haskell. ~ Yiyun Liu et als. #Haskell #FuncBl%C3%B6ndal.pdf #MSc_Thesis #Haskell #FunctionalProgramming #LiquidHaskelltionalProgramming #LiquidHaskell
- Deriving Via (Type-directed instances). ~ Baldur Blöndal. #MSc_Thesis #Haskell #FunctionalProgramming
- Superpowered keyword args in Haskell. ~ Ben Kovach. #Haskell #FunctionalProgramming
- Logical English. ~ Robert Kowalski. #LogicProgramming #Prolog
- Shuffling things up: Applying Group Theory in Advent of Code. ~ Justin Le.l#.X7Vk_XYPDuk.twitter #Haskell #FunctionalProgramming #Math
- The type theory of Lean. ~ Mario Carneiro. #ITP #LeanProver #Logic #Math #TypeTheory
- Arithmetic and casting in Lean. ~ Paul-Nicolas Madelaine. #MSc_Thesis #ITP #LeanProver #Math
- Meta-programming with the Lean proof assistant. ~ Pablo Le Hénaff. #ITP #LeanProver
- Formulations and solutions of IMO problemsin Isabelle/HOL. Filip Marić, Sana Stojanović-Ðurđević. #ITP #IsabelleHOL #Math #IMO
- Selected problems from the International Mathematical Olympiad 2019. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- Bibliografía sobre Lean. #ITP #LeanProver
- The significance of the Curry-Howard isomorphism. ~ Richard Zach. #Logic #CompSci
- Awesome-Lisp-companies: A list of companies using Lisp in production. #CommonLisp
- #SEP: Combinatory logic. ~ Katalin Bimbó. #Logic
- List of events for World Logic Day 2021. #Logic
- A verified optimizer for quantum circuits. ~ Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, Michael Hicks. #ITP #Coq
- Formas prenex, de Skolem y teorema de Herbrand. ~ Fernando Sancho. #Lógica
- Logic and Artificial Intelligence. ~ Richmond Thomason. #Logic #AI
- Formally verified SAT-based AI planning. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL
- Philosophy of mathematics — a reading list. ~ Peter Smith. #Math
- Untangling mechanized proofs. ~ Clément Pit-Claudel. #ITP #Coq
- Video: Untangling mechanized proofs. ~ Clément Pit-Claudel. #ITP #Coq
- De-mystifying Emacs, lsp-haskell and haskell-language-server Setup. ~ Guru Devanla. #Haskell #Emacs
- AI planning languages semantics (in Isabelle/HOL). ~ Mohammad Abdulaziz, Peter Lammich. #ITP #IsabelleHOL #AI
- Verified SAT-based AI planning. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL #AI
- A formalisation of biochemical process languages in Lean. ~ Jonathan Coates. #ITP #LeanProver
- Mechanizing hyperdual numbers in Isabelle/HOL. ~ Filip Smola. #ITP #IsabelleHOL #Math
- Extending equational monadic reasoning with monad transformers. ~ Reynald Affeldt, David Nowak. #ITP #Coq
- Mathlib naming conventions. ~ Jeremy Avigad. #ITP #LeanProver
- IMO 1964 Q1 in Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Ranas, pájaros … y la hipótesis de Riemann. ~ Juan Arias de Reyna. #Matemáticas
- Exotic programming ideas: Part 1 (Module systems). ~ Stephen Diehl. #Haskell #FunctionalProgramming
- Pure destination-passing style in Linear Haskell. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- Métodos numéricos básicos con Octave. ~ Antonia M. Delgado, Juanjo Nieto, Aureliano M. Robles, Óscar Sánchez. #Octave #Matemáticas
- Algoritmos básicos de Cálculo Científico programados con Octave. ~ Óscar Sánchez. #Octave #Matemáticas
- Programming metamorphic algorithms: An experiment in type-driven algorithm design. ~ Hsiang-Shang Ko. #ITP #Agda #FunctionalProgramming
- Formas normales, cláusulas y algoritmo DPLL. ~ Fernando Sancho. #Lógica
- Inside the secret math society known simply as Nicolas Bourbaki. ~ Kevin Hartnett. #Math
- Verified optimizations for functional languages. ~ Zoe Paraskevopoulou. #ITP #Coq #PhD_Thesis
- Generation and use of hints and feedback in a Hilbert-style axiomatic proof tutor. ~ Josje Lodder, Bastiaan Heeren, Johan Jeuring, Wendy Neijenhuis. #Logic #Teaching
- Separate your views; reify your reasoning. ~ Sandy Maguire. #Haskell #FunctionalProgramming
- Pretty-print syntax trees with this one simple trick. ~ Gabriel Gonzalez. #Haskell #FunctionalProgramming
- Opinionated Common Lisp resources 2020. ~ Shubhamkar Ayare. #Programming #CommonLisp
- Writing for reasons. ~ Robin Schroer.
- Category theory: The math behind mathematics. ~ Cole Persch. #Math #CategoryTheory
- A trustful monad for axiomatic reasoning with probability and nondeterminism. ~ Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa. #ITP #Coq
- Towards a certified reference monitor of the Android 10 permission system. ~ Guido De Luca, Carlos Luna. #ITP #Coq
- ιDOT: A DOT calculus with object initialization. ~ Ifaz Kabir, Yufeng Li, Ondřej Lhoták. #ITP #Coq
- A mechanically assisted examinationof vacuity and question beggingin Anselm’s ontological argument. ~ John Rushby. #ITP #PVS
- Implementation of affine arithmetic in Haskell. ~ Joosep Jääger. #BSc_Thesis #Haskell #FunctionalProgramming #Math
- Your orphan instances are probably fine. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming
- A story of an arrow and a comma. ~ Murat Kasimov. #Haskell #FunctionalProgramming
- Construir un buscador (en espacios de estados) desde cero. ~ Fernando Sancho. #Algoritmos #IA
- Inference in Agda (a tutorial on how Agda infers things). ~ Andreas Abel. #ITP #Agda
- Clojure en production. ~ Mathieu Corbin. #Clojure
- How to define things by recursion. ~ Alex Kavvos. #Logic #Math
- Les assistants de preuve et applications à l’apprentissage du raisonnement mathématique. ~ Julien Narboux. #Logic #Math #ITP
- A new chapter for Haskell: The Haskell Foundation. #Haskell #FunctionalProgramming
- The Proof Manifesto. #Logic
- Quantifiers and quantification. ~ Gabriel Uzquiano. #Logic
- Más rompecabezas matemáticos con números. ~ Raúl Ibáñez. #Matemáticas
- Advent of Haskell 2020 (Call for participation). #Haskell #FunctionalProgramming
- The nature of infinity — and beyond (An introduction to Georg Cantor and his transfinite paradise). ~ Jørgen Veisdal. #Logic #Math
- Formally verified SAT-based AI planning. ~ Mohammad Abdulaziz, Friedrich Kurz. #ITP #IsabelleHOL #AI
- An analysis of implementing PVS in SPARK Ada. ~ A. Benjamin Hocking, Jonathan C. Rowanhill, Ben L Di Vito. #ITP #PVS
- Formal verification of Ethereum smart contracts using Isabelle/HOL. ~ Maria Saraiva de Campos Mendes Ribeiro. #ITP #IsabelleHOL
- Whole Haskell is best Haskell. ~ Ashley Yakeley. #Haskell #FunctionalProgramming
- Learning to prove theorems by learning to generate theorems. ~ Mingzhe Wang, Jia Deng. #ATP #ITP #MachineLearning
- Haskell LSP (bonus: for Vim). ~ Monique Oliveira. #Haskell #FunctionalProgramming
- TacTok: Semantics-aware proof synthesis. ~ Emily First, Yuriy Brun, Arjun Guha. #ITP #Coq
- Big Math and the one-brain barrier: The tetrapod model of mathematical knowledge. ~ Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe. #Math #CompSci
- Efficient mixing of arbitrary ballots with everlasting privacy: How to verifiably mix the PPATC scheme . ~ Kristian Gjøsteen, Thomas Haines, Morten Rotvold Solberg. #ITP #Coq
- Glossy Haskell game. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming #Game
- Composable filters using Witherable optics. ~ Chris Penner. #Haskell #FunctionalProgramming