Resumen de lecturas compartidas durante septiembre de 2018
Esta entrada es una recopilación de lecturas compartidas, durante septiembre de 2018, 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.
- Hello, Scala (Learn Scala fast with small, easy lessons). ~ A. Alexander (@alvinalexander). #eBook #FunctionalProgramming #Scala
- GLC: Resumen de lecturas compartidas durante julio de 2018. #FunctionalProgramming #ITP
- GLC: Resumen de lecturas compartidas durante agosto de 2018. #FunctionalProgramming #ITP
- Top schools for AI: New study ranks the leading U.S. artificial intelligence grad programs. #AI
- When you should use lists in Haskell (mostly, you should not). ~ J. Waldmann. #FunctionalProgramming #Haskell
- How I teach functional programming. ~ J. Waldmann. #FunctionalProgramming #Haskell
- How do we store data, then? ~ J. Waldmann. #FunctionalProgramming #Haskell
- Introduction to the Lens Library. ~ J. Waldmann. #FunctionalProgramming #Haskell
- On the formalization of higher inductive types and synthetic homotopy theory. ~ F. van_Doorn. #ITP #Lean #HoTT
- Declarative GTK+ programming with Haskell. ~ O. Wickström (@owickstrom) #FunctionalProgramming #Haskell
- Declarative GTK+ programming in Haskell. ~ O. Wickström (@owickstrom) #FunctionalProgramming #Haskell
- Scipy Lecture Notes (One document to learn numerics, science, and data with Python). #Programming #Python
- Introduction and overview of the main features of the containers package. #FunctionalProgramming #Haskell
- REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting. ~ J. Divasón, J. Aransay. #ITP #IsabelleHOL #Math #Vestigium
- Org-Mode is one of the most reasonable markup languages to use for text. ~ Karl Voit. #Emacs #OrgMode
- A blog in pure Org/Lisp (A pamphlet for hackable website systems). ~ Pierre Neidhardt #Emacs #OrgMode
- Making the jump II: Using more monads. ~ James Bowen (@james_OWA) #FunctionalProgramming #Haskell
- The CBC (Cipher Block Chaining) encryption and decryption. ~ Ken T Takusagawa #FunctionalProgramming #Haskell
- Stream fusion (from lists to streams to nothing at all). ~ D. Coutts, R. Leshchinskiy, D. Stewart. #FunctionalProgramming #Haskell
- The Budan-Fourier theorem and counting real roots with multiplicity in Isabelle/HOL. ~ W. Li. #ITP #IsabelleHOL #Math
- Dependent types in Haskell: Binomial heaps 101. ~ Jasper Van der Jeugt (@jaspervdj) #FunctionalProgramming #Haskell
- Update monads: Variation on state monads. ~ Chris Penner (@chrislpenner) #FunctionalProgramming #Haskell
- Compositional zooming for StateT and ReaderT using lens. ~ Edsko de Vries (@EdskoDeVries). #FunctionalProgramming #Haskell
- Demystifying DList. #FunctionalProgramming #Haskell
- A logic-algebraic tool for reasoning with Knowledge-Based Systems. ~ J.A. Alonso, G.A. Aranda, J. Borrego, M.M. Fernández, M.J. Hidalgo #Logic #Math #CompSci
- Automated reasoning in the age of the Internet. ~ A. Bundy. #ATP
- Vestigium: A formal proof of the computation of Hermite normal form in a general setting by J. Divasón and J. Aransay. #ITP #IsabelleHOL #Math
- Reading for graduate students. Matt Might (@mattmight) #CompSci
- My top nine favourite math texts. ~ Jason Polak #Math
- Intuitionistic logic. ~ Joan Moschovakis #Logic
- Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs. ~ Y. Bertot. #ITP #Coq #Math #Vestigium
- Categories of optics. ~ M. Riley. #CategoryTheory #Haskell
- Fast parser combinator library for Haskell with two strategies (Fast acceptor and slower reporter with decent error messages). ~ D. Mendler. #FunctionalProgramming #Haskell
- A very quick tour of R. ~ Jason Polak #Rstats
- On reasonably sure proofs. ~ Jason Polak #Math
- Theorems for a price: Tomorrow’s semi-rigorous mathematical culture. ~ D. Zeilberger #Math
- Branching processes for QuickCheck generators. ~ A. Mista, A. Russo, J. Hughes. #Haskell
- Vestigium: Comparison of two theorem provers: Isabelle/HOL and Coq. #ITP #IsabelleHOL #Coq
- The unreasonable effectiveness of metaphor. ~ Julie Moronuki (@argumatronic) #Math #Haskell #Linguistics
- A formally verified heap allocator. ~ A. Sahebolamri, S.J. Chapin, S.D. Constable #ITP #IsabelleHOL
- Formal semantics and mechanized soundness proof for fast gradually typed JavaScript. ~ E. Arteca. #ITP #Coq #JavaScript
- The pocket reasoner (automatic reasoning on small devices). ~ J. Otten #ATP #Prolog
- Type variables in patterns. ~ Richard A. Eisenberg, Joachim Breitner, Simon Peyton Jones. #Haskell
- 12 tips for reading math books. ~ Jason Polak #Math
- El yin-yang y el número áureo. ~ M.A. Morales (@gaussianos). #Matemáticas
- Logical truth. ~ M. Gómez #Logic
- Philosophy of technology. ~ M. Franssen et als. #Logic
- Formalizing basic quaternionic analysis. ~ A. Gabrielli, M. Maggesi #ITP #HOL_Light #Math
- Quaternions in Isabelle/HOL. ~ L.C. Paulson. #ITP #IsabelleHOL #Math
- A formal verification approach to process modelling and composition. ~ P. Papapanagiotou. #PhD_Thesis #ITP #HOL_Light
- Correct-by-construction process composition using classical linear logic inference. ~ P. Papapanagiotou, J. Fleuriot. #ITP #HOL_Light
- Picnic: put containers into a backpack. ~ D. Kovanikov (@ChShersh). #FunctionalProgramming #Haskell
- The Pentagon is investing $2 billion into artificial intelligence. ~ Matt McFarland (@mattmcfarland) #AI
- Goodbye VSCode, hello Emacs (again). ~ Bryan Willson Berry (@bryanwb) #Emacs #VSCode #JavaScript
- Grandes ideas de la Filosofía: Lógica. #Lógica
- Inductive programming as approach to comprehensible machine learning. ~ Ute Schmid #ILP #MachineLearnig
- On linear logic, functional programming, and attack trees. ~ Harley Eades III, Jiaming Jiang, and Aubrey Bryant #Haskell
- The formalization of the semantics of the attack tree linear logic. ~ Harley D. Eades III #Agda
- Automated reasoning in quantified non-classical logics. #AutomatedReasoning
- Implementations of natural logics. ~ Lawrence S. Moss #Logic #Sage
- Some thoughts about FOL-translations in Vampire. ~ Giles Reger #AutomatedTheoremProving #Vampire
- Forking and ContT. ~ Lennart Spitzner #FunctionalProgramming #Haskell
- Checking dependent types with normalization by evaluation: a tutorial. ~ David Thrane Christiansen #FunctionalProgramming #Racket
- Google launches new search engine to help scientists find the datasets they need. ~ James Vincent #DataScience
- What is systems programming, really? ~ Will Crichton (@wcrichton) #Programming
- Vestigium: Hammer for Coq (automation for dependent type theory). #ITP #Coq
- Logical rule induction and theory learning using neural theorem proving. ~ A. Campero et als. #MachineLearnig #AutomatedTheoremProving
- Common (but not so common) monads. ~ James Bowen (@james_OWA) #FunctionalProgramming #Haskell
- range: An efficient and versatile range library. ~ Robert Massaioli #FunctionalProgramming #Haskell
- Course: SAT/SMT solving. ~ S. Winkler #Logic #ATP #SAT #SMT
- Learning proof search in proof assistants. ~ M. Färber #PhD_Thesis #ITP #ATP #MachineLearning
- Mechanizing confluence: Automated and certified analysis of first- and higher-order rewrite systems. ~ J. Nagele #PhD_Thesis #ITP #IsabelleHOL
- Automatic inductive equational reasoning. ~ J. Mas Rovira #Haskell #Logic #ATP
- Towards formal foundations for game theory. ~ J. Parsert and C. Kaliszyk. #ITP #IsabelleHOL #Math
- Exploring Nix & Haskell (Part 1: project setup). ~ Christian Henry #FunctionalProgramming #Haskell #Nix
- Towards Coq formalisation of {log} set constraints resolution. ~ C. Dubois and S. Weppe. #ITP #Coq
- Automated theorem proving with extensions of first-order logic. ~ E. Kotelnikov #PhD_Thesis #ATP #Vampire #Logic
- The essence of codata and its implementations. ~ Z. Sullivan #MsC_Thesis #Haskell
- Towards certified virtual machine-based regular expression parsing. ~ T.A. Delfino and R. Ribeiro (@rodrigogeraldo). #FunctionalProgramming #Haskell #QuickCheck
- An operational semantics for greedy regular expression parsing. ~ R. Ribeiro (@rodrigogeraldo). #FunctionalProgramming #Haskell #QuickCheck #ITP #Coq
- O isomorfismo de Curry-Howard (Ou sobre a similaridade entre provas e programas). ~ R. Ribeiro (@rodrigogeraldo). #Logic #CompSci
- Curso: Uma introdução ao assistente de provas Coq. ~ R. Ribeiro (@rodrigogeraldo). #ITP #Coq #Logic
- Programação com tipos dependentes em Agda. ~ R. Ribeiro (@rodrigogeraldo). #FunctionalProgramming #Agda
- A translation of Pierce’s Coq book “Software foundations” to Agda. ~ R. Ribeiro (@rodrigogeraldo). #ITP #Agda
- Aligning concepts across proof assistant libraries. T. Gauthier and C. Kaliszyk. #ITP #MachineLearning
- A mechanized textbook proof of a type unification algorithm. ~ R. Ribeiro and C. Camarão. #ITP #Coq
- Formal verification of folklore and miscellaneous results in number theory. ~ José Manuel Rodríguez Caballero #ITP #IsabelleHOL #Math
- DARPA announces $2 billion in funding for ‘AI next’ campaign. #AI
- Verifying the compositeness of the 20th Fermat number. ~ Ken T Takusagawa. #Math #CompSci
- Libro de exámenes de programación funcional con Haskell (versión del 13 de septiembre de 2018). #ProgramacionFuncional #Haskell #I1M2017
- A beginner’s look at lambda calculus. ~ Prateek Joshi (@prateekvjoshi) #LambdaCalculus
- Fun with typed type-level programming in PureScript. ~ CT Wu (@wu_ct) #FunctionalProgramming #PureScript
- Isabelle formalization of set theoretic structures and set comprehensions. ~ C. Kaliszyk and K. Pąk. #ITP #IsabelleHOL #Math
- Papers with code: list of research papers with links to the source code, updated weekly. ~ Zaur Fataliyev (@fvzaur). #MachineLearning
- Una introducción a la filosofía de la ciencia. ~ R. Carnap #Filosofía #Ciencia
- Rudolf Carnap y los fundamentos de la lógica y las matemáticas. ~ A. Church. #Filosofía #Ciencia
- TacticToe: Learning to prove with tactics. ~ T. Gauthier et als. #ITP #HOL4 #MachineLearning
- The ups and downs of STEM standards. ~ Chris Smith (@cdsmithus) #Teaching #CompSci
- Modal and relevance logics for qualitative spatial reasoning. ~ Pranab Kumar Ghosh. #Msc_Thesis #ITP #Coq #Logic
- A framework for interactive verification of architectural design patterns in Isabelle/HOL. ~ D. Marmsoler. #ITP #IsabelleHOL
- Experimenting with monadic equational reasoning in Coq. ~ R. Affeldt and D. Nowak. #ITP #Coq
- Proving tree algorithms for succinct data structures. ~ R. Affeldt, J. Garrigue, X. Qi, Kazunari Tanaka. #ITP #Coq #Vestigium
- Introductions to advanced Haskell topics. ~ G. Gonzalez (@GabrielG439). #FunctionalProgramming #Haskell
- You could have invented Monads! (and maybe you already have). ~ Dan Piponi (@sigfpe) #FunctionalProgramming #Haskell
- Monad transformers step by step. ~ Martin Grabmüller. #FunctionalProgramming #Haskell
- Functional pearls: Monadic parsing in Haskell. ~ G. Hutton, E. Meijer. #FunctionalProgramming #Haskell
- Why free monads matter. ~ G. Gonzalez (@GabrielG439). #FunctionalProgramming #Haskell
- Functional programming with overloading and higher-order polymorphism. M.P. Jones. #FunctionalProgramming #Haskell
- Vestigium: “Concrete semantics” with Coq and CoqHammer. #ITP #Coq #IsabelleHOL
- Octonions in Isabelle/HOL. ~ Angeliki Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
- CPS based functional references. ~ Twan van Laarhoven #FunctionalProgramming #Haskell
- Compiling to lambda-calculus: Turtles all the way down. ~ Matt Might (@mattmight). #FunctionalProgramming #LambdaCalculus
- Extensa colección de libros de matemáticas. ~ M.A. Morales (@gaussianos). #Matemáticas
- Free mathematics books. #eBooks #Math
- Diez formas de pensar como un matemático. ~ M.A. Morales (@gaussianos). #Matemáticas
- Vestigium: Formal verification of a geometry algorithm (A quest for abstract views and symmetry in Coq proofs). #ITP #Coq #Math
- Aggregation algebras in Isabelle/HOL. ~ Walter Guttmann. #ITP #IsabelleHOL #Math
- CodeWorld update — September 17, 2018. ~ Chris Smith (@cdsmithus) #FunctionalProgramming #haskell #CodeWorld
- Numeric constraint solving in Haskell. ~ Matt Keeter (@impraxical). #FunctionalProgramming #Haskell
- Cours vidéo de Coq. ~ Y. Bertot. #ITP #Coq
- #Vestigium: Proving tree algorithms for succinct data structures. #ITP #Coq
- Isabelle/HoTT: An experimental implementation of HoTT in the interactive theorem prover Isabelle. ~ Josh Chen (@jaycech3n). #ITP #Isabelle #IsabelleHoTT
- Classical analysis with Coq. ~ R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling, P.Y. Strub. #ITP #Coq #Math
- Classical analysis with Coq (Slides). ~ R. Affeldt, C. Cohen, A. Mahboubi, D. Rouhling, P.Y. Strub. #ITP #Coq #Math
- Verifying distributed systems (slides). ~ Zachary Tatlock. #ITP #Coq
- Programming and proving with distributed protocols. ~ I. Sergey, J.R. Wilcox, Z. Tatlock. #ITP #Coq
- A Coq mechanised formal semantics for real life SQL queries: Formally reconciling SQL and (extended) relational algebra (slides). ~ Véronique Benzaken and Évelyne Contejean. #ITP #Coq
- A Coq mechanised formal semantics for realistic SQL queries: Formally reconciling SQL and bag relational algebra. ~ V. Benzaken, É. Contejean #ITP #Coq
- Functional programming for compiling and decompiling computer-aided design. ~ C. Nandi, J.R. Wilcox, P. Panchekha, T. Blau, D. Grossman, Z. Tatlock. #FunctionalProgramming #OCaml
- A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. ~ A. Guéneau, A. Charguéraud, F. Pottier. #ITP #Coq
- Procrastination: A proof engineering technique (slides). ~ A. Guéneau. #ITP #Coq
- Exploring life through logic programming: Logic programming in bioinformatics. ~ A. Dal Palù, A. Dovier, A. Formisano, E. Pontelli. #LogicProgramming #ASP #Bioinformatics
- Introduction to Coq (slides). ~ T. Pietrzak. #ITP #Coq #Logic
- Le raisonnement logique dans l’assistant de preuve Coq. ~ R. Affeldt #ITP #Coq #Logic
- What is the foreign function interface of the Coq programming language? (slides). ~ S. Boulmé. #ITP #Coq
- Preliminary report on the Yalla library: Yet Another deep embedding of linear logic in Coq (slides). ~ O. Laurent. #ITP #Coq #Logic
- ComplCoq: Rewrite Hint construction with completion procedures (slides). ~ M. Ikebuchi, K. Nakano. #ITP #Coq
- ComplCoq: Rewrite Hint construction with completion procedures. ~ M. Ikebuchi, K. Nakano. #ITP #Coq
- From guarded to well-founded: Formalizing Coq’s guard condition (slides). ~ C. Mangin, M. Sozeau. #ITP #Coq
- What is applied category theory? ~ Tai-Danae Bradley. #CategoryTheory
- Fighting spam with Haskell. ~ Simon Marlow (@simonmar) #FunctionalProgramming #Haskell
- Personal website in org. ~ Thibault Marin. #Emacs #OrgMode
- The Theorem Prover Museum. #ATP #ITP #AutomatedReasoning
- Signature-based Gröbner basis algorithms. ~ A. Maletzky. #ITP #IsabelleHOL #Math
- Safe low-level code generation in Coq using monomorphization and monadification. ~ A. Tanaka, R. Affeldt, and J. Garrigue. #ITP #Coq
- What makes functional programming a viable choice for artificial intelligence projects? ~ Prasad Ramesh. #FunctionalProgramming #AI
- Univalent foundations and the UniMath library (The architecture of mathematics). ~ A. Bordg. #Logic #Math #HoTT #ITP #Coq
- Simple reflection of expressions. ~ Twan van Laarhoven #FunctionalProgramming #Haskell
- The prime number theorem. ~ M. Eberl and L.C. Paulson. #ITP #IsabelleHOL #Math
- Agda tips. ~ Donnacha Oisín Kidney (@oisdk) #ITP #Agda
- The Thoralf plugin: for your fancy type needs. ~ D. Otwani, R.A. Eisenberg. #FunctionalProgramming #Haskell #ATP #SMT #Z3
- the-thoralf-plugin: a type-checker plugin to rule all type checker plugins involving type-equality reasoning using SMT solvers. ~ Divesh Otwani. #FunctionalProgramming #Haskell #ATP #SMT #Z3
- What the heck is Typeable!?. ~ Sandeep.C.R #FunctionalProgramming #Haskell
- Alga: a library for algebraic construction and manipulation of graphs in Haskell. ~ Andrey Mokhov. #Haskell
- Simple Web Routing with Spock!. ~ James Bowen (@james_OWA) #FunctionalProgramming #Haskell
- Functional pearls: Even higher-order functions for parsing or why would anyone ever want to use a sixth-order function?. ~ Chris Okasaki. #FunctionalProgramming #SML via @Iceland_jack
- Programming metamorphic algorithms in Agda (Functional pearl). ~ Hsiang-Shang Ko. #FunctionalProgramming #ITP #Agda
- Generic programming of all kinds. ~ A. Serrano, V.C. Miraldo. #FunctionalProgramming #Haskell
- From algebra to abstract machine: a verified generic construction. ~ C. Tomé Cortiñas, W. Swierstra. #FunctionalProgramming #ITP #Agda
- Deriving via (or, how to turn hand-written instances into an anti-pattern). ~ B. Blöndal, A. Löh, R. Scott. #FunctionalProgramming #Haskell
- Garnishing Parsec with Parsley. ~ J. Willis, N. Wu. #FunctionalProgramming #Scala
- Formalising mathematics: a mathematician’s personal viewpoint. ~ Kevin Buzzard #ITP #Lean #Math
- HELIX: a case study of a formal verification of high performance program generation. ~ V. Zaliva, F. Franchetti. #ITP #Coq
- Machine-assisted proofs (ICM 2018 Panel). ~ J. Davenport et als. #ITP #Math
- Coherent explicit dictionary application for Haskell. ~ T. Winant, D. Devriese. #FunctionalProgramming #Haskell
- The strong law of small numbers. ~ R.K. Guy. #Math
- Freer than free. ~ David Smith. #FunctionalProgramming #Haskell
- assoc-list: An association list conceptually signifies a mapping, but is represented as a list (of key-value pairs). ~ Chris Martin (@chris__martin). #FunctionalProgramming #Haskell
- Certified algorithms for program slicing. J.C. Léchenet. #PhD_Thesis #ITP #Coq #Why3
- onlineSPARC: a programming environment for Answer Set Programming. ~ E. Marcopoulos, Y. Zhang. #LogicProgramming #ASP
- “Turing machines”, The Stanford Encyclopedia of Philosophy. ~ Liesbeth De Mol. #CompSci
- A verified certificate checker for finite-precision error bounds in Coq and HOL4. ~ H. Becker et als. #ITP #Coq #HOL4
- co-log: Composable contravariant combinatorial comonadic configurable convenient logging. ~ Dmitrii Kovanikov #FunctionalProgramming #Haskell
- A revised and verified proof of the Scalable Commutativity Rule. ~ L. Tsai, E. Kohler, M.F. Kaashoek, N. Zeldovich. #ITP #Coq
- Course: Building verification tools with Isabelle. ~ Georg Struth. #ITP #IsabelleHOL
- Symmetric polynomials in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
- The Type Tetris Toolbox. ~ J.J. Koullas (@jjoekoullas) #FunctionalProgramming #Haskell
- Reading into Atiyah’s proof. ~ R.J. Lipton, K.W. Regan. #Math
- Formalizing the translation method in Agda. ~ Bjarki Ágúst Guðmundsson. #ITP #Agda
- Translate: An Agda library for turning equations into bijections using the translation method. ~ Bjarki Ágúst Guðmundsson. #ITP #Agda
- AlgoWiki: a wiki dedicated to competitive programming. ~ Bjarki Ágúst Guðmundsson. #Programming #Algorithms
- Rewrite combinators. ~ Stephen Diehl (@smdiehl). #FunctionalProgramming #Haskell
- A list of foundational Haskell papers. ~ Emily Pillmore (@emi1ypi) #FunctionalProgramming #Haskell
- Haskell in production: A GHC upgrade success story. ~ Trevis Elser (@telser). #FunctionalProgramming #Haskell
- Komposition: The video editor built for screencasters. ~ Oskar Wickström (@owickstrom). #Haskell
- T-414-ÁFLV: A competitive programming course. ~ Bjarki Ágúst Guðmundsson. #Programming #Algorithms
- Atiyah Riemann Hypothesis proof: final thoughts. ~ K. Steckles, C. Lawson-Perfect. #Math
- Formalization of first-order syntactic unification. ~ K.F. Brandt, A. Schlichtkrull, J. Villadsen. #ITP #IsabelleHOL
- Mocking effects using constraints and phantom data kinds. ~ Chris Penner (@chrislpenner). #FunctionalProgramming #Haskell
- Overloaded type families. ~ Xia Li-yao #FunctionalProgramming #Haskell
- Metaheurísticas de búsquedas y optimización (Parte 1). ~ F. Sancho (@sanchocaparrini). #Algoritmos #IA
- Metaheurísticas de búsquedas y optimización (Parte 2). ~ F. Sancho (@sanchocaparrini). #Algoritmos #IA
- Formally verified software in the real world. ~ G. Klein et als. #FormalVerification #ITP #IsabelleHOL
- 90 Years of AI in the movies: what’s changed (and what hasn’t). #AI
- AI goes to the movies: A history of Artificial Intelligence in film. #AI
- Essential Math for Data Science: ’Why’ and ‘How’. ~ Tirthajyoti Sarkar #DataScience