Resumen de lecturas compartidas durante diciembre de 2020
Esta entrada es una recopilación de lecturas compartidas, durante diciembre 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.
- Dijkstra monads forever: termination-sensitive specifications for interaction trees. ~ Lucas Silver, Steve Zdancewic. #ITP #Coq
- A minimalistic verified bootstrapped compiler (Proof Pearl). ~ Magnus O. Myreen. #ITP #HOL4
- Advent of Code 2020: Haskell solution reflections for all 25 days. ~ Justin Le. #Haskell #FunctionalProgramming
- Haskell tutorial and cookbook, Second edition. ~ Mark Watson. #eBook #Haskell #FunctionalProgramming
- Examples for “Haskell tutorial and cookbook, Second edition”. ~ Mark Watson. #Haskell #FunctionalProgramming
- Functional programming: Enemy of the state. ~ Onur Gümüş. #FunctionalProgramming
- The simplest MonadFail instance. ~ Kazuki Okamoto. #Haskell #FunctionalProgramming
- StateT vs IORef: a benchmark. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence Paulson. #ITP #IsabelleHOL #Math
- Learnings from solving Advent of Code 2020 in Haskell. ~ Abhinav Sarkar. #Haskell #FunctionalProgramming
- Haskell type-level functions shenanigans (An introduction to some useful language extensions). ~ Antoine Leblanc. #Haskell #FunctionalProgramming
- Ephemeral purely functional data structure and linear type. ~ Kazuki Okamoto. #Haskell #FunctionalProgramming
- Programming language families (Procedural, object oriented, logic, and functional languages). ~ Jobelle Firme, Nicolas Valera, Yunus Canemre, Stephen Burchill, Beenish Khurshid. #Programming
- Cofinality and the delta system lemma (in Isabelle). ~ Pedro Sánchez Terraf. #ITP #IsabelleZF #Logic #Math
- Counting bits with Haskell (The bad and the good way). ~ Flavio Corpa. #Haskell #FunctionalProgramming
- (Haskell in Haskell) 3: Parsing. ~ Lúcás Meier. #Haskell #FunctionalProgramming
- My first type theory. ~ Arved Friedemann. #TypeTheory
- Trees indexed by a Cayley Monoid. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- Lean prover: Frequently Asked Questions. #ITP #LeanProver
- Monad transformers and effects with Backpack. ~ Ollie Charles. #Haskell #FunctionalProgramming
- Refactoring using type classes and optics. ~ Fraser Tweedale. #Haskell #FunctionalProgramming
- Santa Wrap. ~ Lucas Di Cioccio. #Haskell #FunctionalProgramming #MiniZinc
- Essential thinking. The art of creative thinking for problem solving. ~ Antoni Ligeza. #ProblemSolving #Prolog #CLP #AI
- A Lisp programmer living in Python-land: The Hy programming language. ~ Mark Watson. #eBook #Lisp #Python #Programmig
- Python programming and scientific computation. ~ Tran Nam Trung. #eBook #Python #Programming
- Descubriendo la programación funcional: Elixir con Erick Navarro. #Elixir #ProgramaciónFuncional vía @republicawebes
- Formalization of Euler summation formula (in Lean). ~ Marc Masdeu. #ITP #LeanProver #Math
- For a few dollars more (Verified fine-grained algorithm analysis down to LLVM). ~ Maximilian P. L. Haslbeck, Peter Lammich. #ITP #IsabelleHOL
- Towards formally verified compilation of tag-based policy enforcement. ~ CHR Chhak, Andrew Tolmach, Sean Anderson. #ITP #Coq
- λS: Computable semantics for differentiable programming with higher-order functions and datatypes. ~ Benjamin Sherman, Jesse Michel, Michael Carbin. #Haskell #FunctionalProgramming
- The year in Math and Computer Science. ~ Bill Andrews. #Math #CompSci
- Lisp, Slime y Emacs. #Lisp #Emacs
- Topological semantics for paraconsistent and paracomplete logics. ~ David Fuenmayor. #ITP #IsabelleHOL #Math
- Don’t think, just defunctionalize. ~ Joachim Breitner. #Haskell #FunctionalProgramming
- Sistemas deductivos proposicionales. ~ Fernando Sancho. #Lógica
- A concise sequent calculus for teaching first-order logic. ~ Asta Halkjær From, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
- The generalised continuum hypothesis implies the axiom of choice in Coq. ~ Dominik Kirst, Felix Rech. #ITP #Coq #Logic #Math
- GeoGebra reasoning tools for humans and for automatons. ~ Zoltán Kovács, Tomás Recio. #ATP #GeoGebra #Math
- Lower case Haskell. ~ @tonyday567. #Haskell #FunctionalProgramming #AdventOfHaskell
- Optics by example cheat sheets. ~ Chris Penner. #Haskell #FunctionalProgramming
- Reconciling concepts from FP and OOP. ~ Thomas Mahler. #Haskell #FunctionalProgramming #AdventOfHaskell
- vector: Efficient packed-memory data representations. ~ @FPComplete. #Haskell #FunctionalProgramming
- Scripting the Hell out of Trello with Haskell. ~ Riccardo Odone. #Haskell #FunctionalProgramming #AdventOfHaskell
- A Coq proof of the correctness of X25519 in TweetNaCl. ~ P. Schwabe, B. Viguier, T. Weerwag, F. Wiedijk. #ITP #Coq
- Dependently typed folds (folds that change type at each step!). ~ Ryan Orendorff. #Haskell #FunctionalProgramming #AdventOfHaskell
- Getting acquainted with Lens (part 1). ~ Pawel Szulc. #Haskell #FunctionalProgramming
- Foo to bar: Naming conventions in Haskell. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- Descubriendo la programación funcional: Haskell con Héctor Navarro. #Haskell #ProgramaciónFuncional
- An experience report on writing usable DSLs in Coq. ~ Clément Pit-Claudel, Thomas Bourgeat. #ITP #Coq
- Hackage search: Regex-based online code search. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
- Haskell study plan. ~ Gil Mizrahi. #Haskell #FunctionalProgramming
- Classical programming topics with functional programming. ~ Visnovitz Márton #FunctionalProgramming #TypeScript
- Logic: A study guide. ~ Peter Smith. #Logic
- Formalization of PAL⋅S5 in proof assistant. ~ Jiatu Li. #ITP #LeanProver #Logic
- Formal proof of the main theorem for surreal. ~ Jiatu Li. #ITP #LeanProver
- An introduction to property-based testing with QuickCheck. ~ Jesper Cockx. #Haskell #FunctionalProgramming #QuickCheck
- Beauty and the bytestring. ~ Norman Liu. #Haskell #FunctionalProgramming #AdventOfHaskell
- Haskell memoization and evaluation model. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
- A novice-friendly induction tactic for Lean. ~ Jannis Limperg. #ITP #LeanProver
- Talking about Toys. ~ Alejandro Serrano. #Haskell #FunctionalProgramming #AdventOfHaskell
- Haskell – Doomed to succeed? ~ Ari Fordsham. #Haskell #FunctionalProgramming
- A new perspective of paramodulation complexity by solving massive 8 puzzles. ~ Ruo Ando, Yoshiyasu Takefuji. #ATP #Otter
- The Fibonacci sequence as a functor. ~ Tai-Danae Bradley. #CategoryTheory
- A vivid christmas carol. #Haskell #FuncionalProgramming #AdventOfHaskell
- On the Lean proof assistant, Part 1. ~ Jason Polak. #ITP #LeanProver
- On the formal verification of the Stellar Consensus Protocol. ~ G. Losa, M. Dodds. #ITP #IsabelleHOL
- Authenticated data structures as functors in Isabelle/HOL. ~ A. Lochbihler, O. Marić. #ITP #IsabelleHOL
- On the use of formal methods to model and verify neuronal archetypes. ~ E. de Maria et als. #ITP #Coq
- Mechanized formal model of bitcoin’s blockchain validation procedures. ~ K. Rupić, L. Rožić, A. Derek. #ITP #Coq
- Enumerating trees. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming #Agda
- Pattern matching. ~ Michael Snoyman. #Haskell #FunctionalProgramming
- At the interface of algebra and statistics. ~ Tai-Danae Bradley. #Math #CategoryTheory
- Personal website in org. #Emacs #OrgMode
- Precise typing implies functional programming. ~ Pavel Potoček. #Haskell #FunctionalProgramming
- Structure your errors. ~ Tikhon Jelvis. #Haskell #FunctionalProgramming #AdventOfHaskell
- Roll your own Holly Jolly streaming combinators with Free. ~ Justin Le. #Haskell #FunctionalProgramming #AdventOfHaskell
- Asymptotic reasoning in a proof assistant. ~ Manuel Eberl. #PhD_Thesis #ITP #IsabelleHOL #Math
- An answer to the Bose-Nelson sorting problem for 11 and 12 channels. ~ Jannis Harder. #ITP #IsabelleHOL
- Programmer = démontrer? La correspondance de Curry-Howard aujourd’hui. ~ Xavier Leroy. #Logic #Math #CompSci #ITP
- (Haskell in Haskell) 0. Introduction. ~ Lúcás Meier. #Haskell #FunctionalProgramming
- (Haskell in Haskell) 1. Setup. ~ Lúcás Meier. #Haskell #FunctionalProgramming
- (Haskell in Haskell) 2. Lexing. ~ Lúcás Meier #Haskell #FunctionalProgramming
- Functional Christmas (2020). #FunctionalProgramming
- Elm Christmas (2020). #Elm #FunctionalProgramming
- How the slowest computer programs illuminate math’s fundamental limits. ~ John Pavlus. #Math #CompSci
- Patterns that eventually fail. ~ John Baez. #Math
- Emacs family editors. #Emacs
- The future of Mathematics? ~ R.J. Lipton. #ITP #Math
- The ‘retry’ package. ~ Wander Hillen. #Haskell #FunctionalProgramming #AdventOfHaskell
- Haskell coreutils: tee. ~ Austin Gandalf. #Haskell #FunctionalProgramming
- Parser combinators: a walkthrough (Or: Write you a Parsec for great good). ~ Antoine Leblanc. #Haskell #FunctionalProgramming
- The shrinks applicative. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- sydtest: An experimental testing framework for Haskell. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- A SAT-based resolution of Lam’s problem. ~ Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh. #ATP #SAT_Solvers #Math
- Extracting smart contracts tested and verified in Coq. ~ D. Annenkov, M. Milo, J.B. Nielsen, B. Spitters. #ITP #Coq
- Simpler and safer API design using GADTs. ~ Chris Penner. #Haskell #FunctionalProgramming #AdventOfHaskell
- “A damn stupid thing to do” – the origins of C. ~ Richard Jensen. #Programming
- Denotational design. ~ Armando Santos. #Haskell #FunctionalProgramming #AdventOfHaskell
- What is functional programming? ~ Mike Loukides. #FunctionalProgramming
- Favorite Emacs packages. ~ Bozhidar Batsov. #Emacs
- The relational method with message anonymity for the verification of cryptographic protocols. ~ Pasquale Noce. #ITP #IsabelleHOL
- Relational minimum spanning tree algorithms (in Isabelle/HOL). ~ Walter Guttmann, Nicolas Robinson-O’Brien. #ITP #IsabelleHOL #Algorithms
- Computable analysis for verified exact real computation. ~ M. Konečný, F. Steinberg, H. Thies. #ITP #Coq #Math
- Mechanized verification of a fine-grained concurrent queue from Facebook’s Folly library. ~ S.F. Vindum, D. Frumin, L. Birkedal. #ITP #Coq
- The Pigeonhole principle. ~ Jonathan Prieto-Cubides. #ITP #Agda #Math
- The halting problem (part 1). ~ Callan McGill. #Haskell #FunctionalProgramming #Logic #Math
- The halting problem (part 2). ~ Callan McGill. #ITP #Agda #Logic #Math
- Voevodsky’s unachieved project. ~ Andrei Rodin. #ITP #Math
- Haskell documentation with Haddock: Wishes’n’tips. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- The development of proof theory. ~ Jan von Plato. #Logic #ATP
- Automated reasoning. ~ Frederic Portoraro. #ATP #ITP #Logic #Math #LogicProgramming
- Benefits of statically typed functional programming? Wrong question. ~ Mikael Tönnberg. #FunctionalProgramming #AdventOfHaskell
- Cultures of programming: Understanding the history of programming through controversies and technical artifacts. ~ Tomas Petricek. #Programming #Emacs
- Whirlwind tour of Stack for beginners. ~ School of FP. #Haskell #FunctionalProgramming
- Bits instance of Integer. ~ Ken T Takusagawa. #Haskell #FuncionalProgramming
- Capturing the magic of Prelude.interact. ~ Samuel. #Haskell #FuncionalProgramming #AdventOfHaskell
- Liquid tensor experiment. ~ Peter Scholze. #ITP #LeanProver #Math
- Named goals in Coq. ~ Joachim Breitner. #ITP #Coq
- The group-theory package. ~ Emily Pillmore. #Haskell #FunctionalProgramming #Math
- Building a bulletin board using Scotty and friend. ~ Gil Mizrahi. #Haskell #FunctionalProgramming
- Ambassadors of Logic. #Logic
- Lolisa: Formal syntax and semantics for a subset of the Solidity programming language in mathematical tool Coq. ~ Zheng Yang. #ITP #Coq
- The Haskell runtime is what sets it apart from the competition. ~ Harpo Roeder. #Haskell #FunctionalProgramming
- Processing CodeBlocks in Hakyll. ~ Mario Lang. #Haskell #FunctionalProgramming #Hakyll #AdventOfHaskell
- Una recopilación de algoritmos para calcular el valor del número π. ~ @Alvy. #Matemáticas #Algoritmos #Programación
- Yet another π computation algorithms. ~ Thomas Joly. #Math #Algorithms #Programming
- NandGame: un juego de lógica binaria en el que hay que construir circuitos cada vez más complejos. ~ @Alvy. #Lógica #Computación
- The Nand Game. #Logic #CompSci
- The Free Num is a Sequence of Bags. ~ Tony Day. #Haskell #FunctionalProgramming #AdventOfHaskell
- Haskell, in Elm terms: Type Classes. ~ @terezk_a #Haskell #FuncionalProgramming #Elm
- Another tool in the box: Why use formal methods for autonomous systems? ~ Matt Luckcuck. #FormalMethods
- My journey into Haskell. ~ Gustavo Franke. #Haskell #FunctionalProgramming
- Complicated Haskell words – Isomorphism. ~ Ju Liu. #Haskell #FunctionalProgramming
- Composition in trick-taking card games. ~ Ben Fiedler. #Haskell #FunctionalProgramming
- Advent of Code 2020 with Haskell. ~ Ariel Kwiatkowski. #Haskell #FunctionalProgramming #AdventOfCode
- An experience report on writing usable DSLs in Coq. ~ Clément Pit-Claudel, Thomas Bourgeat. #ITP #Coq
- Program = Proof. ~ Samuel Mimram. #eBook #Logic #Math #ITP #Agda
- Finite map extras (in Isabelle/HOL). ~ Javier Díaz. #ITP #IsabelleHOL
- Haskell solutions to Advent of Code 2020. #Haskell #FunctionalProgramming #AdventOfCode
- Haskell solutions to Advent of Code 2020. ~ Justin Le. #Haskell #FunctionalProgramming #AdventOfCode
- Advent of Code 2020 solutions in Lean 4. ~ Reid Barton. #LeanProver #ITP #FuncionalProgramming
- Machine-checking the universal verifiability of Election Guard. ~ Thomas Haines, Rageev Goré, Jack Stodart. #ITP #Coq
- A note on right abelian distributive AG-groupoids. ~ Bashar Khan et als. #ATP #Prover9 #Mace4 #Math