Resumen de lecturas compartidas durante octubre de 2019

Esta entrada es una recopilación de lecturas compartidas, durante octubre de 2019, 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.

• Proving the correctness of a compiler. ~ Xavier Leroy. #ITP #Coq
• Lean Library currently studying for a degree at Imperial College. ~ Kevin Buzzard. #ITP #LeanProver #Math
• Didactic emacs-lisp macro example (ie. a tutorial). ~ Shane Mulligan (@mullikine). #Emacs #Lisp
• Tutorial for the lens library. #Haskell #FunctionalProgramming
• Mapping of ND proof templates to Isabelle formalization. ~ A. Steen. #ITP #IsabelleHOL #Logic
• Type-checking session-typed π-calculus with Coq. ~ Uma Zalakain. #MSc_Thesis #ITP #Coq
• Constructing finitary inductive types from natural numbers. ~ Andras Kovacs (@andrasKovacs6). #ITP #Agda #Math
• Programming cognitive robots. ~ Hector J. Levesque. #eBook #AI #DeclarativeProgramming #Schem #Racket
• Homoiconic Prolog: Explain yourself! ~ Paul Brown. #Prolog #LogicProgramming
• What is good about Haskell? ~ Donnacha Oisín Kidney (@oisdk). #Haskell #FunctionalProgramming
• The science of functional programming (A tutorial, with examples in Scala). ~ Sergei Winitzki. #eBook #FunctionalProgramming #Scala
• Computer science and metaphysics: A cross-fertilization. ~ Christoph Benzmüller et als. #ITP #Isabelle-HOL
• Verifying the titular properties of a leftist heap. ~ Mistral Contrastin (@madgen_). #Haskell #FunctionalProgramming #Algorithms
• Learning logic and proof with an interactive theorem prover. ~ J. Avigad. #ITP #LeanProver #Logic
• Proof technology in mathematics research and teaching. #eBook #ATP #ITP #Math
• A common type of rigorous proof that resists Hilbert’s programme. ~ A. Bundy, M.A. Jamnik. #Logic #Math
• Bayesian optimisation with Gaussian processes for premise selection. ~ Agnieszka Słowik et als. #ATP #Vampire #MachineLearning
• You are already smart enough to write Haskell. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
• Didactical issues at the interface of mathematics and computer science. ~ V. Durand-Guerrier, A. Meyer, S. Modeste. #Math #ComSci
• 10 famous bugs in the computer science world. #CompSci #Programming
• The correspondence between monads in category theory and monads in Haskell. ~ D. Kalemis (@dkalemis). #Haskell #FunctionalProgramming #CategoryTheory
• AgdaCheatSheet: Basics of the dependently-typed functional language Agda. ~ Musa Al-hassy. #ITP #Agda
• Verification of GPU program optimizations in Lean. ~ B. Fischer. #MSc_Thesis #ITP #LeanProver
• A promising path towards autoformalization and general Artificial Intelligence. ~ Christian Szegedy. #AI #PLN #ITP
• Number theory in a proof assistant. ~ John Thickstun. #ITP #LeanProver #Math
• Automatic and scalable detection of logical errors in functional programming assignments. ~ Dowon Song et als. #OCaml #FunctionalProgramming
• An assertional proof of red–black trees using Dafny. ~ Ricardo Peña. #Dafny
• GRIFT: A richly-typed, deeply-embedded RISC-V semantics written in Haskell. ~ Benjamin Selfridge. #Haskell #FunctionalProgramming
• NetLogo: Grafos. F. Sancho (@sanchocaparrini). #NetLogo
• Proof engineering for large-scale verification projects. ~ Ahmet Celik. #PhD_Thesis #ITP #Coq
• Ormolu: a formatter for Haskell source code. ~ Mark Karpov, Utku Demir. #Haskell #FunctionalProgramming
• The next 7000 programming languages. ~ Robert Chatley, Alastair Donaldson, and Alan Mycroft. #Programming
• With category theory, mathematics escapes from equality. ~ Kevin Hartnett. #Math #CategoryTheory
• Verified extraction for Coq. ~ Olivier Savary Bélanger. #PhD_Thesis #ITP #Coq
• From definitional interpreter to symbolic executor. ~ Adrian D. Mensing et als. #Haskell #FunctionalProgramming
• Competitive programming in Haskell: reading large inputs with ByteString. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• OpenLibra: Un enorme banco de libros con licencia libre. #OpenLibra
• Planificación: Fundamentos (y NetLogo). ~ Fernando Sancho (@sanchocaparrini). #IA #NetLogo
• The ethics of AI ethics (An evaluation of guidelines). ~ Thilo Hagendorff. #AI
• Monads as graphs. ~ Neil Mitchell. #Haskell #FunctionalProgramming
• Prolog: forwards and backwards. ~ Paul Brown. #Prolog #LogicProgramming
• Hello, Tau Prolog! ~ Paul Brown. #Prolog #LogicProgramming
• The Lean mathematical library. ~ The mathlib Community. #ITP #LeanProver #Math
• Functors, vectors, and quantum circuits. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
• The resolution of Keller’s conjecture. ~ J. Brakensiek, M. Heule, J. Mackey. #ATP #SAT #Math via @ozanerdem
• How to design co-programs. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• Clean: An abstract imperative programming language and its theory. ~ F. Tuong, B. Wolff. #ITP #IsabelleHOL
• Aristotle’s assertoric syllogistic in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki (@AngelikiKoutso1). #ITP #IsabelleHOL #Logic
• Beating C with 80 lines of Haskell: wc. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
• Partial application using flip. ~ Jasper Van der Jeugt (@jaspervdj). #Haskell #FunctionalProgramming
• Un procesador de expresiones epistémicas en programas lógicos. ~ Javier Garea Cidre. #TFG #LogicProgramming #ASP
• Sigma protocols and commitment schemes. ~ David Butler, Andreas Lochbihler. #ITP #IsabelleHOL
• What type soundness theorem do you really want to prove? ~ Derek Dreyer et als. #CompSci #TypeTheory
• Improving rebindable syntax. ~ Neil Mitchell. #Haskell #FunctionalProgramming
• Painless Haskell. ~ Paweł Szulc (@rabbitonweb). #Haskell #FunctionalProgramming
• The inner magic behind the Z3 theorem prover. ~ Nikolaj Bjørner, Leonardo de Moura. #ATP #SMT #Z3
• A categorical view of computational effects. ~ Emily Riehl (@emilyriehl). #CategoryTheory #FunctionalProgramming
• So I used Erlang … is my system as scalable as they say it’d be? ~ Laura M. Castro (@lauramcastro). #Erlang #FunctionalProgramming
• Writing programs that write tests: better testing with Scala. ~ Adam Rosien (@arosien). #Scala #FunctionalProgramming
• Software written in Haskell: Stories of success. ~ Yulia Gavrilova, Gints Dreimanis. #Haskell #FunctionalProgramming
• Mathematics for machine learning. ~ Marc Peter Deisenroth, A Aldo Faisal, Cheng Soon Ong. #eBook #MachineLearning #Math
• Refactoring recursion. ~ Harold Carr (@haroldcarr). #Haskell #FunctionalProgramming
• Fun with categories. ~ Marco Perone (@marcoshuttle). #CategoryTheory #Idris #FunctionalProgramming
• The sandwich theorem. ~ Kevin Buzzard. #ITP #LeanProver #Math
• A verified optimizer for quantum circuits. ~ Kesha Hietala et als. #ITP #Coq
• Liquid types vs. Floyd-Hoare logic. ~ Ranjit Jhala (@RanjitJhala). #LiquidHaskell #Haskell #FunctionalProgramming
• Prüfer encoding/decoding of a tree in Common Lisp. ~ Atabey Kaygun (@Atabey_Kaygun). #CommonLisp #Algorithms
• Course: Advanced topics in logic (Automated reasoning and satisfiability). ~ Marijn Heule and Ruben Martins. #ATP #SAT
• Programming and symbolic computation in Maude. ~ F. Durán et als. #ITP #Maude
• The Lean mathematical library. ~ The mathlib Community. #ITP #LeanProver #Math
• Rapid prototyping formal systems in MMT: 5 case studies. ~ Dennis Müller, and Florian Rabe. #ITP #MMT #Logic
• A weakly initial algebra for higher-order abstract syntax in Cedille. ~ Aaron Stump. #ITP #Cedille
• Haskell for madmen: Setup. #Haskell #FunctionalProgramming
• Haskell for madmen: Hello, monad! #Haskell #FunctionalProgramming
• A curated list of amazingly awesome Haskell articles and talks for beginners. ~ Daniel Pfefferkorn (@albohlabs). #Haskell #FunctionalProgramming
• Gmail Gnus GPG Guide (GGGG). ~ Alex Schroeder. #Emacs #Gmail #Gnus #GPG
• Logical verification in Lean. ~ A. Bentkamp, J. Blanchette, J. Hölzl. #eBook #ITP #LeanProver #Logic #FunctionalProgramming
• Automated Reasoning in the Cloud with John Harrison. #ATP
• A distributed and trusted web of formal proofs. ~ Dale Miller. #Logic #ITP #ATP
• A first step in the translation of Alloy to Coq. ~ Salwa Souaf, Frédéric Loulergue. #ITP #Coq #Alloy
• Can computers prove theorems? ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Logical verification (Course notes). ~ F. van Raamsdonk. #eBook #ITP #Coq #Logic
• Applicative without currying. ~ Chris Smith (@cdsmithus). #Haskell #FunctionalProgramming
• System F in Agda, for fun and profit. ~ J. Chapman, R. Kireev, C. Nester, P. Wadler. #ITP #Agda
• Formalising Σ-protocols and commitment schemes using CryptHOL. ~ D. Butler, A. Lochbihler, D. Aspinall, A. Gascón. #ITP #IsabelleHOL
• VerifyThis 2019 (Polished Isabelle solutions). ~ P. Lammich, S. Wimmer. #ITP #IsabelleHOL
• Functional programming and verification. ~ T. Nipkow. #Haskell #FunctionalProgramming
• DeepXplore: Automated whitebox testing of deep learning systems. ~ K. Pei, Y. Cao, J. Yang, S. Jana. #DeepLearning
• Simon Marlow, Simon Peyton Jones, and Satnam Singh win Most Influential ICFP Paper Award. #Hsakell #FunctionalProgramming
• Chalkdust, and the natural number game! ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
• Åqvist’s dyadic deontic logic E in HOL. ~ C. Benzmüller, A. Farjami, X. Parent. #ITP #IsabelleHOL #Logic
• Fifty years of Hoare’s Logic. K.R. Apt, E.R. Olderog. #Logic #Verification #CompSci
• Programming algorithms: Graphs. ~ Vsevolod Dyomkin. #CommonLisp #Algorithms
• Infinite types and existential newtypes. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• Proof assistants: from symbolic logic to real mathematics? ~ Lawrence C Paulson #ITP #Logic #Math
• List of software bugs. ~ Wikipedia #Programming
• Deep reinforcement learning in HOL4. ~ T. Gauthier #ITP #HOL4 #DeepLearning
• Formally verified Mathematics. ~ J. Avigad, J. Harrison. #ITP #Math
• Les assistants de preuve, ou comment avoir confiance en ses démonstrations. ~ J. Narboux. #ITP #Coq
• IMO Grand Challenge (Automated problem solving). #ITP #Math #IMO
• Metamath Zero: The cartesian theorem prover. ~ M. Carneiro #ITP #MetamathZero
• Earliest uses of symbols of set theory and logic. ~ J. Miller #Logic #Math
• Dex: array programming with typed indices. ~ D. Maclaurin et als #Haskell #FunctionalProgramming
• Dex: a research language for array processing in the Haskell/ML family. #Haskell #FunctionalProgramming
• The Zen of Haskell. ~ #Haskell
• Gestionar bibliografía con Emacs. #Emacs
• Formalising perfectoid spaces. ~ K. Buzzard, J. Commelin, P. Massot. #ITP #LeanProver #Math
• The reasonable effectiveness of the continuation monad. ~ Li-yao Xia. #Haskell #FunctionalProgramming
• A monad is just a submonad of the continuation monad, what’s the problem? ~ Li-yao Xia. #Haskell #FunctionalProgramming
• Computer-supported exploration of a categorical axiomatization of modeloids. ~ L. Tiemens, D.S. Scott, C. Benzmüller, M. Benda. #ITP #IsabelleHOL
• Completeness of an axiomatization of graph isomorphism via graph rewriting in Coq. ~ C. Doczkal, D. Pous. #ITP #Coq
• Formalisation tools for classical analysis (A case study in control theory). ~ D. Rouhling. #PhD_Thesis #ITP Coq #Math
• Short proof of Menger’s Theorem in Coq (Proof Pearl). ~ C. Doczkal. #ITP #Coq #Math
• La Wayback Machine ahora permite conservar páginas de forma fiable junto con todas las páginas a las que enlazan. ~ @Alvy. #Internet
• Computing pi with bc. ~ John D. Cook. #Math #CompSci