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