Resumen de lecturas compartidas durante agosto de 2020
Esta entrada es una recopilación de lecturas compartidas, durante agosto 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.
- Type-driven neural programming by example. ~ Kiara Grouwstra. #PhD_Thesis #Haskell #FunctionalProgramming #NeuralNetwork
- Typed neuro-symbolic program synthesis for the typed lambda calculus. ~ Kiara Grouwstra. #Haskell #FunctionalProgramming #NeuralNetwork
- Ackermann’s function in iterative form: A subtle termination proof with Isabelle/HOL. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Math
- Formalising cryptography using CryptHOL. ~ David Thomas Butler. #PhD_Thesis #ITP #IsabelleHOL
- Describing console I/O behavior for testing student submissions in Haskell. ~ Oliver Westphal, Janis Voigtländer. #Haskell #FunctionalProgramming
- Haskell from 0 to IO (Maybe Hero). #Haskell #FunctionalProgramming
- Knowledge representation and reasoning with Answer Set Programming. ~ Natalie Kuster. #ASP #LogicProgramming
- How close are computers to automating mathematical reasoning? ~ Stephen Ornes. #ATP #ITP #Math #CompSci
- Computer scientists attempt to corner the Collatz conjecture. ~ Kevin Hartnett. #ATP #SAT_Solver #Math #CompSci
- Finding the hardest formulas for resolution. ~ Tomáš Peitl, Stefan Szeider. #ATP #SAT_Solver #Logic
- What is Haskell, and who should use it? ~ Jason McClellan. #Haskell #FunctionalProgramming
- Towards a verified model of the Algorand consensus protocol in Coq. ~ Musab A. Alturki et als. #ITP #Coq
- Relational disjoint-set forests in Isabelle/HOL. ~ Walter Guttmann. #ITP #IsabelleHOL
- Verifiable C. ~ Andrew W. Appel, Qinxiang Cao. #eBook #ITP #Coq
- Do more with your types: GADTs and LiquidHaskell. ~ Alejandro Serrano, Haskeller. #Haskell #FunctionalProgramming #LiquidHaskell
- OCaml scientific computing (Functional programming meets Data Science). ~ Liang Wang, Jianxin Zhao. #eBook #OCaml #FunctionalProgramming #DataScience
- Automating proofs of lattice inequalities in Coq with reinforcement learning and duality. ~ Anshula Gandhi, Favio E. Miranda-Perea, Lourdes del Carmen Gonz. #ITP #Coq #MachineLearning
- Getting started with proving math theorems through reinforcement learning (An experiment at MIT’s Brains, Minds, and Machines Lab). ~ Anshula Gandhi. #ITP #Coq #MachineLearning
- Guaranteeing proof termination (Dealing with infinite proof search in reinforcement-learning automated proofs). ~ Anshula Gandhi. #ITP #Coq #MachineLearning
- LiquidHaskell is a GHC plugin. ~ Ranjit Jhala. #Haskell #FunctionalProgramming
- Functional programming is awesome!! ~ Amandeep Singh. #FunctionalProgramming #Haskell
- An introduction to formal logic. ~ Peter Smith. #eBook #Logic
- An introduction to Gödel’s theorems. ~ Peter Smith. #eBook #Logic
- Some more list algorithms. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
- Introduction to Homotopy Type Theory. ~ Egbert Rijke. #HoTT #ITP #Agda #Coq
- Adventures in mathematical reasoning. ~ Toby Walsh. #ATP #Math
- Understanding memory fragmentation. ~ David Eichmann. #Haskell #FunctionalProgramming
- Probabilistic programming with continuations. ~ Jules Hedges. #Haskell #FunctionalProgramming
- Five stages of accepting constructive mathematics. ~ Andrej Bauer. #Logic #Math
- Logic symbols (A comprehensive collection of the most notable symbols in formal/mathematical logic). ~ Math Vault. #Logic #Math
- Formal Mathematics and the Lean theorem prover. ~ Jeremy Avigad. #Logic #Math #ITP #LeanProver
- Formal Mathematics and the Lean theorem prover [Video]. ~ Jeremy Avigad. #Logic #Math #ITP #LeanProver
- Effect handlers in Haskell, evidently. ~ Ningning Xie, Daan Leijen. #Haskell #FunctionalProgramming
- Scripted signal functions. ~ David A. Stuart. #Haskell #FunctionalProgramming
- Types as axioms, or: playing god with static types. ~ Alexis King. #Haskell #FunctionalProgramming
- Inductive logic programming at 30: a new introduction. ~ Andrew Cropper, Sebastijan Dumančić. #ILP #MachineLearning #LogicProgramming
- Computer search settles 90-year-old Math problem. ~ Kevin Hartnett. #Math #CompSci #ATP #SAT_Solvers
- Whirlwind tour of Cabal for beginners. #Haskell #FunctionalProgramming
- How stylish-haskell works. ~ Felix Mulder. #Haskell #FunctionalProgramming
- A graded Monad for deadlock-free concurrency (Functional Pearl). ~ Andrej Ivašković, Alan Mycroft. #Haskell #FunctionalProgramming
- Finger trees explained anew, and slightly simplified (Functional Pearl). ~ Koen Claessen. #Haskell #FunctionalProgramming
- Enhancing functor structures step-by-step (Part 1). ~ Justin Le. #Haskell #FunctionalProgramming
- Enhancing functor structures step-by-step (Part 2). ~ Justin Le. #Haskell #FunctionalProgramming
- Set theory symbols. ~ Math Vault. #Math
- Ordinal partitions in Isabelle/HOL. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
- Post-quantum verification of Fujisaki-Okamoto. ~ Dominique Unruh. #ITP #IsabelleHOL
- Logipedia: towards a Wikipedia of formal proofs. ~ Gilles Dowek. #ITP #Math
- Topology (A categorical approach). ~ Tai-Danae Bradley, Tyler Bryson, and John Terilla. #Ebook #Math #CategoryTheory
- Hybrid logic in the Isabelle proof assistant: Benefits, challenges and the road ahead. ~ Asta Halkjær From.f#page=27 #ITP #IsabelleHOL #Logic
- A formalisation of the SPARC TSO memory model for multi-core machine code. ~ Zhe Hou, David Sanan, Alwen Tiu, Yang Liu, Jin Song Dong. #ITP #IsabelleHOL
- Generalised Veltman semantics in Agda. ~ J.M. Rovira, L. Mikec, J.J. Joosten.f#page=90 #ITP #Agda #Logic
- Penrose: from mathematical notation to beautiful diagrams. ~ K. Ye, W. Ni, M. Krieger, D. Ma’ayan, J. Wise, J. Aldrich. #DSL #Haskell #FunctionalProgramming #Math
- Automatic verification of annotated sequential imperative programs. ~ Alinda Harmanny. #Haskell #FunctionalProgramming #Logic
- Un poco más sobre magit. #Emacs #Git
- A proof of the Sprague-Grundy theorem and other results related to impartial games in Lean. ~ Fox Thomson. #ITP #LeanProver
- HOList: An environment for machine learning of higher-order theorem proving. ~ Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, Stewart Wilcox. #ITP #HOL_Light #MachineLearning
- Haskell mini-patterns handbook. ~ Dmitrii Kovanikov, Veronika Romashkina. #Haskell #FunctionalProgramming
- Proof-carrying plans: a resource logic for AI planning. ~ Alasdair Hill, Ekaterina Komendantskaya, Ronald P. A. Petrick. #ITP #Agda #AI
- Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. ~ Ralph Bottesch, Max W. Haslbeck, René Thiemann. #ITP #IsabelleHOL
- The Mathlib formalisation project needs your help (A serious effort to formalise modern mathematics). ~ Oliver Nash. #ITP #LeanProver #Math
- A verified tableau prover for modal logic K- ~ Minchao Wu. #ITP #LeanProver #Logic
- Cross wolf, goat and cabbage across the river with effects. ~ Murat Kasimov #Haskell #FunctionalProgramming
- Generic Haskell. ~ Jonathan Dowland. #Haskell #FunctionalProgramming
- Towards provably correct probabilistic flight systems. ~ Elkin Cruz-Camacho, Saswata Paul, Fotis Kopsaftopoulos, Carlos A. Varela. #ITP #Agda
- Amicable numbers in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
- Using Lean with undergraduate mathematicians. ~ Kevin Buzzard. #ITP #LeanProver #Math
- mathlib: Lean’s mathematical library. ~ Johannes Hölzl. #ITP #LeanProver #Math
- Embedding specialized proof languages into Lean (A case study). ~ Simon Hudon. #ITP #LeanProver #Logic
- A formal proof of Hensel’s lemma over the p-adic integers. ~ Robert Y. Lewis. #ITP #LeanProver #Math
- How to design co-programs. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
- Quantitative typing with non-idempotent intersection types. ~ Bob Atkey. #ITP #Agda
- Datatypes as quotients of polynomial functors. ~ Jeremy Avigad. #ITP #LeanProver
- Model categories in Lean. ~ Reid Barton. #ITP #LeanProver #CategoryTheory
- A formalization of a Henkin-style completeness proof for propositional modal logic in Lean. ~ Bruno Bentzen. #ITP #LeanProver #Logic
- So what are hammers good for? ~ Jasmin Blanchette. #ITP #IsabelleHOL
- Data vs Control: a tale of two functors. ~ Arnaud Spiwack. #Haskell #FunctionalProgramming
- Building a web library using super hard Haskell. ~ Marcin Rzeźnicki. #Haskell #FunctionalProgramming
- Zero-overhead abstractions in Haskell using staging. ~ Andres Löh. #Haskell #FunctionalProgramming
- Safety and conservativity of definitions in HOL and Isabelle/HOL. ~ Ondřej Kunčar, Andrei Popescu. #Logic #ITP #HOL #IsabelleHOL
- Coq Coq correct! (Verification of type checking and erasure for Coq, in Coq). ~ M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, T. Winterhalter. #ITP #Coq
- FreeSpec: Specifying, verifying and executing impure computations in Coq. ~ Thomas Letan, Yann Régis-Gianas. #ITP #Coq
- CoCon: A conference management system with formally verified document confidentiality. ~ Andrei Popescu, Peter Lammich, Ping Hou. #ITP #IsabelleHOL
- Haskell to core: Understanding Haskell features through their desugaring. ~ Vladislav Zavialov. #Haskell #FunctionalProgramming
- Agile generation of Cloud API bindings with Haskell. ~ Michal Gajda. #Haskell #FunctionalProgramming
- GraphQL :heart: Haskell. ~ Alejandro Serrano. #Haskell #FunctionalProgramming
- Formalising undergraduate mathematics. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Formalising undergraduate mathematics [Slides]. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Read you a blaze. ~ Guru Devanla. #Haskell #FunctionalProgramming
- Down to the wire. ~ Eric Torreborre. #Haskell #FunctionalProgramming
- Getting acquainted with Lens. ~ Pawel Szulc. #Haskell #FunctionalProgramming
- Stan: Haskell static analyser. ~ Veronika Romashkina, Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- El lenguaje Prolog: un ejemplo del paradigma de programación lógica. ~ Marcos Merino #Prolog #ProgramaciónLógica
- Testing Haskell code with Stack, Ghcid and Hspec. ~ Iori Matsuhara. #Haskell #FunctionalProgramming
- How a Haskell programmer wrote a tris in Purescript. ~ Henri Tuhola. #Haskell #Purescript #FunctionalProgramming
- Lorentz: Achieving correctness with Haskell Newtypes. ~ Kostya Ivanov. #Haskell #FunctionalProgramming
- Functional dependencies. ~ Michael Snoyman. #Haskell #FunctionalProgramming
- Clojure basics: How code is evaluated. #Clojure #FunctionalProgramming
- Elastic sheet-defined functions. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
- The many faces of isOrderedTree. ~ Joachim Breitner. #Haskell #FunctionalProgramming
- Bit vectors without compromises. ~ Andrew Lelechenko. #Haskell #FunctionalProgramming
- Verified textbook algorithms (A biased survey). ~ T. Nipkow, M. Eberl, M.P.L. Haslbeck. #ITP #FormalVerification #Algorithms
- Tools for teaching Theoretical Computer Science. ~ Sam Lowenstein. #ITP #Coq
- Haskell – Extracting IO. ~ Ken Aguilar. #Haskell #FunctionalProgramming
- Lenses for tree traversas. ~ Michael Peyton Jones. #Haskell #FunctionalProgramming
- Definitional lawfulness: proof by inspection testing. ~ Li-yao Xia. #Haskell #FunctionalProgramming
- Finding proofs in Tarskian geometry. ~ M. Beeson, L. Wos. #ATP #Otter #Math via @SandMouth
- Defunctionalizing arithmetic to an abstract machine. ~ Philip Zucker. #Haskell #FunctionalProgramming #Math
- The Tactician (extended version): A seamless, interactive tactic learner and prover for Coq. ~ Lasse Blaauwbroek, Josef Urban, Herman Geuvers. #ITP #Coq #MachineLearning
- Theorem proving in Lean (Release 3.18.4, Aug 06, 2020). ~ Jeremy Avigad, Leonardo de Moura, Soonho Kong. #eBook #ITP #LeanProver
- Formalizing 100 theorems in Lean. #ITP #LeanProver #Math
- Designing critical digital systems (Formal verification of a token player for synchronously executed Petri Nets). ~ Vincent Iampietro. #ITP #Coq
- Formalizing foundational notions in Naproche-SAD. ~ P. Koepke, J. Penquitt, M. Schütz, E. Sturzenhecker. #ITP #NaprocheSAD #Math
- «Four in a Row» in Haskell (Part I: Background and General Considerations). ~ Patrick Bucher. #Haskell #FunctionalProgramming
- «Four in a Row» in Haskell (Part II: Implementation of the Board Logic). ~ Patrick Bucher. #Haskell #FunctionalProgramming
- Some fundamental theorems in Mathematics. ~ Oliver Knill. #Math
- Eliminating bugs with dependent Haskell(Experience report). ~ Noam Zilberstein. #Haskell #FunctionalProgramming
- Staged sums of products. ~ Matthew Pickering, Andres Löh, Nicolas Wu. #Haskell #FunctionalProgramming
- GHC exercises (A little course to learn about some of the more obscure GHC extensions). ~ Tom Harding. #Haskell #FunctionalProgramming
- Generic traversals with applicative difference lists. ~ Li-yao Xia. #Haskell #FunctionalProgramming
- Effect handlers in Haskell, evidently. ~ N. Xie, D. Leijen. #Haskell #FunctionalProgramming
- Stitch: the sound type-indexed type checker (functional pearl). ~ R.A. Eisenberg. #Haskell #FunctionalProgramming
- Composing effects into tasks and workflows. ~ Y. Parès, J.P. Bernardy, R.A. Eisenberg. #Haskell #FunctionalProgramming
- Type your matrices for great good (Functional pearl): A Haskell library of typed matrices and applications. ~ Armando Santos. #Haskell #FunctionalProgramming #Math
- A mathematical formulation of the tax code? (Reverse engineering the tax code and analysis by automated theorem proving). ~ Denis Merigoux. #ATP #SMT
- Problem solving strategies. ~ Terence Tao (2010). #Math
- Emacs for statisticians (Part 1): Analyzing data on remote servers using Spacemacs and ESS. ~ Sergio Olmos. #Emacs #Rstat
- Lectures on mathematical computing with Python. ~ Jay Gopalakrishnan. #eBook #Python #Math
- #ForMatUS: Libro “Matemáticas en Lean”. #DAO #LeanProver #Matemáticas
- Checkpoint: Implementing linear relations for linear time invariant systems. ~ Philip Zucker. #JuliaLang #CategoryTheory
- Describing microservices using modern Haskell. ~ Alejandro Serrano. #FuncionalProgramming #Haskell
- Solving text adventure games via symbolic execution. ~ Gergő Érdi. #Haskell #FunctionalProgramming #SMT