Resumen de lecturas compartidas durante octubre de 2020
Esta entrada es una recopilación de lecturas compartidas, durante octubre 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.
- Cellular automaton in Haskell (II). WireWorld. ~ Claes-Magnus Berg. #Haskell #FunctionalProgramming
- Accidentally-quadratic HashMaps. ~ Jack Kelly. #Haskell #FunctionalProgramming
- Handling of uncaught exceptions in Haskell. ~ Ivan Gromakovsky. #Haskell #FunctionalProgramming
- Plucking In, Plucking Out. ~ Matt Parsons. #Haskell #FunctionalProgramming
- Formally verified constraints solvers (A guided tour). ~ Catherine Dubois. #ITP #Coq #CSP
- Competitive programming in Python (128 algorithms to develop your coding skills). ~ Christoph Dürr, Jill-Jênn Vie.1#v=onepage&q&f=false #Programming #Python
- Efficient automatic differentiation made easy via category theory. ~ Conal Elliott. #Haskell #CategoryTheory
- Teaching interactive proofs to mathematicians. ~ M. Ayala-Rincón, T.A. de Lima. #ITP #PVS #Math
- Isabelle/HOL as a meta-language for teaching logic. ~ Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn. #ITP #IsabelleHOL #Logic
- Formalizing IMO problems and solutions in Isabelle/HOL. ~ Filip Marić, Sana Stojanović-Đurđević. #ITP #IsabelleHOL #Math
- Formalization of IMO solutions in Isabelle/HOL. ~ Filip Marić. #ITP #IsabelleHOL #Math
- Haskell: The good parts. ~ Marc Scholten. #Haskell #FunctionalProgramming
- Rompecabezas matemáticos con números. ~ Raúl Ibáñez. #Matemáticas
- Quicksort in Haskell. ~ Alexander Vershilov. #Haskell #FunctionalProgramming
- How I use org-mode. ~ Yann Esposito. #Emacs #OrgMode
- Tableros semánticos en lógica de primer orden. ~ Fernando Sancho. #Lógica
- Why I prefer functional programming. ~ G. Gonzalez. #FunctionalProgramming
- A sound type system for physical quantities, units, and measurements in Isabelle/HOL. ~ Simon Foster, Burkhart Wolff. #ITP #IsabelleHOL
- Tautology checkers in Isabelle and Haskell. ~ Jørgen Villadsen. #ITP #IsabelleHOL #Haskell #Logic
- IMO 1981 Q3 in Lean. ~ Kevin Lacker. #ITP #LeanProver #Math #IMO
- Haskell: The bad parts, part 1. ~ Michael Snoyman. #Haskell #FunctionalProgramming
- Formal verification of a certified policy language. ~ Amir Eaman, Amy Felty. #ITP #Coq
- Actris 2.0: Asynchronous session-type based reasoning in separation logic. ~ Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers. #ITP #Coq
- Development method of three kinds of typical tree structure algorithms and Isabelle-based machine assisted verification. ~ Changjing Wang et als. #ITP #IsabelleHOL
- An infinite universe of number systems. ~ Kelsey Houston-Edwards. #Math
- Tableros semánticos en lógica proposicional. ~ Fernando Sancho. #Lógica #Matemática
- Automated theorem proving, fast and slow. ~ Michael Rawson, Giles Reger. #ATP #MachineLearning
- SeLFiE: Modular semantic reasoning for induction in Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL
- The Map of Mathematics. #Math
- A formalization of “Correctness of a compiler for arithmetic expressions” (McCarthy and Painter 1967) using the Lean theorem prover. ~ Xi Wang. #ITP #LeanProver
- Why fintech companies use Haskell. ~ Roman Alterman. #Haskell #FunctionalProgramming
- The coin change problem in Haskell. ~ Aron. #Haskell #FunctionalProgramming
- The greatest mathematician that never lived. ~ Pratik Aghor. #Math
- Quien utiliza Haskell?? ~ Emanuel Goette. #Haskell #ProgramaciónFuncional
- IMO 1998 Q2 in Lean. ~ Oliver Nash. #ITP #LeanProver #Math #IMO
- Una colección de falacias lógicas ilustradas con ejemplos. ~ @Alvy. #Lógica
- Common logical fallacies (A handy collection of the most common logical fallacies for you to bookmark). #Logic
- EvoLogic: Sistema tutor inteligente para ensino de Lógica. ~ Cristiano Galafassi, Fabiane F.P. Galafassi, Eliseo B. Reategui, Rosa M. Vicari. #Logic #AI
- Emacs user survey. #Emacs
- crdt.el: a real-time collaborative editing environment for Emacs using Conflict-free Replicated Data Types. #Emacs
- nntwitter: A Gnus backend for Twitter. #Emacs #Twitter
- Awesome Elisp: a list of resources linked to Emacs LISP (Elisp) development. #Emacs #Elisp
- Verified textbook algorithms (A biased survey). #ITP #IsabelleHOL
- Theorem proving for Catlab 2: Let’s try Z3 this time. Nope. ~ Philip Zucker #CategoryTheory #JuliaLang
- Implementing cellular automata with comonads and dependent types. #Haskell #FunctionalProgramming
- Fun with Lambda Calculus. ~ Stepan Parunashvili. #Clojure #FunctionalProgramming #LambdaCalculus
- IMO 2019 problem 4 in Lean. ~ Floris van Doorn. #ITP #LeanProver #Math #IMO
- Fun with combinators. ~ Donnacha Oisín Kidney. #Logic #CompSci #Combinators
- Sintaxis y semántica de la lógica de primer orden. ~ Fernando Sancho. #Lógica #Matemática
- A formal correctness proof of Boruvka’s minimum spanning tree algorithm. ~ Nicolas Robinson-O’Brien. #MSc_Thesis #ITP #IsabelleHOL #Math
- Formalizing graph trail properties. ~ Hanna Elif Lachnitt. #Thesis #ITP #IsabelleHOL #Math
- Model structure on the universe of all types in interval type theory. ~ Simon Boulier, Nicolas Tabareau. #ITP #Coq
- Symbolic Artificial Intelligence (Lecture 1: Introduction to description logics and ontologies). ~ Natalia Díaz Rodríguez. #AI #Logic
- Logics and symbolic AI: Knowledge representation and reasoning. ~ Isabelle Bloch, Natalia Dı́az Rodrı́guez. #AI #Logic
- Course: Logics and symbolic AI. ~ Isabelle Bloch, Natalia Dı́az Rodrı́guez. #AI #Logic
- What is an algorithm? How computers know what to do with data. ~ Jory Denny. #Algorithms
- Drawing Git Graphs with Graphviz and Org-Mode. ~ Correl Roush. #Emacs #OrgMode
- Things to do to an algorithm. ~ Bertrand Meyer. #Algorithms
- The pros and cons of online lab classes for Computer Science – 2020 pandemic edition. ~ Philip Guo. #CompSci
- Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda. ~ Sebastián Urciuoli, Álvaro Tasistro Nora Szasz. #ITP #Agda
- Resolución de los 99 ejercicios de Prolog. #Prolog #ProgramaciónLógica
- Formalisation and meta-theory of type theory. ~ Théo Winterhalter. #ITP #Coq #TypeTheory
- Refinement types: A tutorial. ~ Ranjit Jhala, Niki Vazou. #Haskell #FunctionalProgramming
- Production Haskell (Succeeding in industry with Haskell). ~ Matt Parsons. #Haskell #FunctionalProgramming
- Bottlenecked on Haskell’s text library. ~ Falco Peijnenburg. #Haskell #FunctionalProgramming
- Sintaxis y semántica de la lógica proposicional. ~ Fernando Sancho. #Lógica #Matemática
- Reflective programs in tree calculus. ~ Barry Jay. #ITP #Coq #Logic
- Silly job interview questions in Haskell. ~ Chris Penner. #Haskell #FunctionalProgramming
- The Hitchhiker’s Guide to Logical Verification (2020 Standard Edition (October 12, 2020)). ~ Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl. #eBook #ITP #LeanProver
- The unreasonable effectiveness of the Julia programming language. ~ Lee Phillips. #JuliaLang #Programming
- Towards tactic metaprogramming in Haskell. ~ Sandy Maguire. #Haskell #FunctionalProgramming
- Normal forms. ~ Travis Whitaker. #Haskell #FunctionalProgramming
- What are algebraic data types? ~ @dicabrejas. #Haskell #FunctionalProgramming
- Emacs might not be doomed after all. ~ Oivvio Polite. #Emacs
- Inductive logic programming at 30: a new introduction. ~ Andrew Cropper, Sebastijan Dumančić. #ILP #MachineLearning #LogicProgramming
- Delivering with Haskell. ~ Sam Halliday. #Haskell #FunctionalProgramming
- Dyadic deontic logic in HOL: Faithful embedding and meta-theoretical experiments. ~ Christoph Benzmüller, Ali Farjami, Xavier Parent. #ITP #IsabelleHOL #Logic
- Public announcement logic in HOL. ~ Sebastian Reiche, Christoph Benzmüller. #ITP #IsabelleHOL
- An antiquotation for locale graphs. ~ Clemens Ballarin. #ITP #IsabelleHOL
- Tutorial: Verify Haskell programs with hs-to-coq. ~ Li-yao Xia. #ITP #Coq #Haskell #FunctionalProgramming
- Embracing a mechanized formalization. ~ Li-yao Xia. #ITP #Coq #Haskell #FunctionalProgramming
- Separation logic-based verification atop a binary-compatible filesystem model. ~ Mihir Mehta, William Cook. #ITP #ACL2
- The anarchist abstractionist: Who was Alexander Grothendieck? ~ Jørgen Veisdal. #Math
- A novice-friendly induction tactic for Lean (Draft). ~ Jannis Limperg. #ITP #LeanProver
- Proving quantum programs correct. ~ Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, Michael Hicks. #ITP #Coq
- Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu. #ITP #Coq #Logic #Math
- On the Nielsen-Schreier theorem in homotopy type theory. ~ Andrew W Swan. #ITP #Agda #Math #HoTT
- Digging for fold: Synthesis-aided API discovery for Haskell. ~ Michael B. James et als. #Haskell #FunctionalProgramming
- Mathematical fallacy proofs. ~ Xing Yuan. #Logic #Math
- Building problem solvers. ~ Kenneth D. Forbus, Johan de Kleer. #eBook #AI #CommonLisp
- Computer scientists break traveling salesperson record. ~ Erica Klarreich. #Algorithms #CompSci
- Reasoning about monotonicity in separation logic. ~ Amin Timany, Lars Birkedal. #ITP #Coq
- The Arcane Algorithm Archive (a collaborative effort to create a guide for all important algorithms in all languages). #Algorithms #Programming
- Formalizing the ring of Witt vectors. ~ Johan Commelin, Robert Y. Lewis. #ITP #LeanProver #Math
- On characterizing Nat in Agda. ~ Callan McGill. #ITP #Agda #Logic #Math
- Course: Higher-Dimensional Type Theory. ~ Favonia. #TypeTheory #ITP #Agda
- Higher-dimensional type theory (Lecture recordings). ~ Favonia. #TypeTheory
- Scientists solve 90-year-old geometry problem. ~ Byron Spice. #Math #ATP #SAT_solver
- Course “Functional Programming”. ~ Bob Atkey. #Haskell #FunctionalProgramming
- Collect in Rust, traverse in Haskell and Scala. Michael Snoyman. #Haskell #Rust #Scala #FunctionalProgramming via @FPComplete
- Knowledge is good. ~ R.J. Lipton. #Logic #Math
- Smart induction for Isabelle/HOL (Tool paper). ~ Yutaka Nagashima. #ITP #IsabelleHOL
- Chain of events: Modular process models for the law. ~ Søren Debois et als. #ITP #IsabelleHOL
- Formalisation: Chain of events: Modular process models for the law. ~ Søren Debois #ITP #IsabelleHOL
- Combinatorial geometries in Lean. ~ Adam Topaz. #ITP #LeanProver #Math
- Proof repair across type equivalences. ~ Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman. #ITP #Coq
- All about strictness. ~ Michael Snoyman. #Haskell #FunctionalProgramming via @FPComplete
- Starting Haskellings! ~ James Bowen. #Haskell #FunctionalProgramming
- Blogging with Emacs & Org-mode. ~ Musa Al-hassy. #Emacs #OrgMode
- Calculational Mathematics and CalcCheck. ~ Musa Al-hassy. #Math #CalcCheck
- Mechanized logical relations for termination-insensitive noninterference. ~ S.O. Gregersen, J. Bay, A. Timany, L. Birkedal. #ITP #Coq
- Combinatorics in Lean. ~ Bhavik Mehta. #ITP #LeanProver #Math
- Optics and Kleisli arrows. ~ Alejandro Serrano. #Haskell #FunctionalProgramming
- Tool supported specification and verification of highly available applications. ~ Peter Zeller. #ITP #IsabelleHOL
- Generating mutually inductive theorems from concise descriptions. ~ Sol Swords. #ITP #ACL2
- Ethereum’s recursive length prefix in ACL2. ~ Alessandro Coglio. #ITP #ACL2 #Ethereum
- Isomorphic data type transformations. ~ Alessandro Coglio, Stephen Westfold. #ITP #ACL2
- Set theory from Cantor to Cohen. ~ Akihiro Kanamori. #Logic #Math vía @logicians
- Fixed points theorems for non-transitive relations. ~ Jérémy Dubut, Akihisa Yamada. #ITP #IsabelleHOL #Math
- Computing and proving well-founded orderings through finite abstractions. ~ Rob Sumners. #ITP #ACL2
- Quadratic extensions in ACL2. ~ Ruben Gamboa, John Cowles, Woodrow Gamboa. #ITP #ACL2 #Math
- Essential logic for computer science. ~ Rex Page, Ruben Gamboa.1#v=onepage&q&f=true #eBook #Logic #ITP #ACL2
- Grzegorczyk hierarchy. #Logic #Math #CompSci
- Matemáticas vs Coronavirus: recursos matemáticos para la docencia online. #Matemáticas
- Cambiando el blog a org-static-blog. #Emacs
- Learning-assisted theorem proving with millions of lemmas. ~ Cezary Kaliszyk, Josef Urban. #ITP #ATP #MachineLearning
- Build scripts with perfect dependencies. ~ Sarah Spall, Neil Mitchell, Sam Tobin-Hochstadt. #Haskell #FunctionalProgramming
- Building the mathematical library of the future. ~ Kevin Hartnett. #ITP #LeanProver #Math