Lecturas del Grupo de Lógica Computacional durante el año 2017

Este repositorio es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el año 2017. La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

Contenido

Enero 2017
Febrero 2017
Marzo 2017
Abril 2017
Mayo 2017
Julio 2017
Agosto 2017
Septiembre 2017
Octubre 2017
Noviembre 2017
Diciembre de 2017

Enero 2017

Advances in connection-based automated theorem proving. ~ J. Otten & W. Bibel #Logic #ATP #Prolog
Best practices for scientific computing. ~ G. Wilson et als. #Programming
Ten simple rules for the open development of scientific software. ~ A. Prlić & J.B. Procter #Programming
2017 is not just another prime number. ~ T.J. Wei #Matemáticas
Lecturas sobre lógica computacional, programación funcional y razonamiento automático del 2016. ~ J.A. Alonso #GLC
The Twelvefold Way. ~ Lukas Bulwahn #IsabelleHOL #Math #AFP
Lazy vs strict state monad. ~ Kwang Yul Seo. #Haskell
Write you an interpreter. ~ Kwang Yul Seo. #Haskell
Basic category theory. ~ Tom Leinster #Math #eBook
(R)creational Common Lisp. ~ Marco Antoniotti #Lisp #Rstats
foldl vs foldl’. ~ Kwang Yul Seo. #Haskell
Verification for ASP denotational semantics: a case study using the PVS theorem prover. ~ F. Aguado et als. #PVS #ASP
Functors, applicatives, and monads. ~ M. Snoyman. #Haskell
Nix and Haskell in production. ~ G. Gonzalez. #Haskell #Nix
SICP (Structure and Interpretation of Computer Programs) in Python. ~ GitBook #eBook #Python
Why recursive data structures?. ~ Reginald Braithwaite #Algorithms #JavaScript
CertiCoq: A verified compiler for Coq. ~ A.W. Appel et als. #Coq
Typeclassopedia. ~ Brent Yorgey #Haskell
Combinatorial algorithms (for computers and calculators). ~ A. Nijenhuis & H.S. Wilf #eBook #Math
EasyTest: a Haskell simple testing toolkit. ~ Paul Chiusano. #Haskell
First-order logic according to Harrison. ~ A.B. Jensen, A. Schlichtkrull & J. Villadsen #IsabelleHOL #Logic #AFP
GHC optimization and fusion. ~ Mark Karpov #Haskell
5 big predictions for Artificial Intelligence in 2017. ~ Will Knight #AI
Writing an interpreter using fold. ~ Kwang Yul Seo. #Haskell
Opaleye’s sugar on top. ~ Renzo Carbonara #Haskell
GHC (STG,Cmm,asm) illustrated for hardware persons (exploring some mental models and implementations). ~ Takenobu Tani #Haskell
Formalizing eventsourcing. ~ @yoeight #Haskell
Concurrent refinement algebra and rely quotients in Isabelle/HOL. ~ J. Fell, I. Hayes, A. Velykis #IsabelleHOL
Recopilación de pensamientos.
Verification of a Diffie-Hellman password-based authentication protocol. ~ P. Noce #IsabelleHOL
Intro to Parsing with Parsec in Haskell. ~ Jake Wheat #Haskell
Modular construction of Bayesian inference algorithms. ~ A Scibior, Z Ghahramani #Haskell
Goodbye, Object Oriented Programming. ~ Charles Scalfani. #Programming
So you want to be a functional programmer. ~ Charles Scalfani. #Programming #FP
Type defaulting in Haskell. ~ Kwang Yul Seo. #Haskell
Implementing a call-by-value interpreter in Haskell. ~ Kwang Yul Seo. #Haskell
Haskell pitfalls. ~ Chris Allen, Mark Wotton #Haskell
P =? NP: A survey. ~ Scott Aaronson #Math #CompSci #History
3.000 millones de archivos: así es la mayor biblioteca de código abierto del mundo. ~ José Manuel Blanco. #Programación
The Software Heritage archive.
Visible type application in GHC 8. ~ Kwang Yul Seo. #Haskell
Polymorphism for dummies. ~ G. Gonzalez. #Haskell
Continuation passing style interpreter. ~ Kwang Yul Seo. #Haskell
Learn you a Haskell - In a nutshell. ~ Michael Härtl #Haskell
Integrating Computer Science in Math: The potential is great, but so are the risks. ~ E. Schanzer #Math #CompSci
Call for interest: Haskell in middle school math education. ~ Chris Smith #Haskell #Math
Formal network models and their application to firewall policies. ~ A.D. Brucker, L. Brügger & B. Wolff #IsabelleHOL
Simple RNA folding in 130 lines of Haskell. ~ Michael J. Flynn #Haskell
How the strengths of Lisp-family languages facilitate building complex and flexible bioinformatics applications. ~ B.B. Khomtchouk et als. #Lisp
GRAKN.AI and Haskell: Data processing using Haskell and the Grakn knowledge graph. ~ Felix Chapman #Haskell
Cheat sheet: Python for Data Science. ~ Martijn #Python #DataScience
Glance, a visual Haskell. ~ Robbie Gleichman #Haskell
Linearity, uniqueness, and Haskell. ~ Edsko de Vries. #Haskell
Eta: a pure, lazy, strongly typed functional programming language on the JVM. #Haskell #Eta
The essence of the iterator pattern. ~ J Gibbons, BCS Oliveira #Haskell
Why Traversable is the real deal. ~ @yoeight #Haskell
Fast Haskell: Competing with C at parsing XML. ~ Chris Done. #Haskell
An introduction to Liquid Haskell. ~ Ricardo Peña #Haskell
Refactoring with Applicatives in Haskell. ~ Brendan Benson #Haskell
The Great Programming Jargon Bake-off (Imperative vs. Declarative. Pure vs. Impure. Static vs. Dynamic). ~ Preethi Kasireddy #Programming
How lazy evaluation works in Haskell. ~ Heinrich Apfelmus #Haskell
Should you get started in Data Science? ~ John F. McGowan #DataScience
The rise and fall and rise of logic. ~ C. Dutilh Novaes. #Logic
Safe primes, Sylow theorems, and Cryptography. ~ J.D. Cook. #Math #CompSci
The transcendence of e in Isabelle/HOL. ~ Manuel Eberl #IsabelleHOL #Math
Automated theorem proving. ~ J.D. Cook. #Math #CompSci
Prácticas de Matemáticas con Maxima: Matemáticas usando Software Libre. ~ A.J. Arriaza et als. #Libro #Matemáticas #Maxima
Equational reasoning about formal languages in coalgebraic style. ~ Andreas Abel #Agda
Monads made difficult: A short, fast and analogy-free introduction to Haskell monads derived from a categorical perspective. ~ S. Diehl. #Haskell
Leibniz’s characteristica universalis and calculus ratiocinator today. ~ Bruno Woltzenlogel Paleo #Logic
Computer-assisted theoretical philosophy (computer-assisted formalizations of ontological proofs). #Coq #IsabelleHOL
The essence of functional structures. ~ Adil Akhter. #Scala
Applicative programming with effects. ~ Conor McBride & Ross Paterson. #Haskell
Course: Programming languages (Fall 2016). ~ Brent Yorgey #Haskell
The design and use of QuickCheck. ~ Joe Nelson #Haskell #QuickCheck
Formalization of Birth-Death and IID Processes in Higher-order Logic. ~ L. Liu, O. Hasan & S. Tahar #HOL4
Memoization in Haskell. ~ Kwang Yul Seo. #Haskell
LiquidHaskell: a static verifier for Haskell, based on Liquid Types. #Haskell
Automatic verification and interactive theorem proving. ~ Andrea Asperti #ATP #ITP
Formalization of the pumping lemma for context-free languages. ~ M.V M. Ramos et als. #ITP #Coq
A simple Publicly Verifiable Secret Sharing Scheme and its application to electronic voting. ~ Berry Schoenmakers
Haskell implementation of the Public Verifiable Secret Scheme based on Berry Schoenmakers’s paper. ~ Carlos D’Agostino #Haskell
Lazy I/O and graphs (Finding the shortest path in a lazily loaded infinite graph). ~ Jasper Van der Jeugt. #Haskell
Rextester: A nice online IDE that supports multiple prog lang #Fsharp #Haskell #erlang #Scala #OCaml #Swift #elixirlang #Go …
A tutorial on using Dafny to construct verified software. ~ Paqui Lucio #Dafny
Zipped finger tree (o porqué los `ArrayList` son ineficientes). ~ @__josejuan__ #Haskell
Bertrand’s postulate in Isabelle/HOL. ~ J. Biendarra & M. Eberl #IsabelleHOL #Math
Speeding up a distributed computation in Haskell. ~ Francesco Mazzoli #Haskell
Haskell Pad: Run your Haskell on the browser. ~ Kwang Yul Seo. #Haskell
Introduction to Haskell. ~ Kwang Yul Seo. #Haskell
Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. ~ R. Affeldt, J. Garrigue, T. Saikawa #Coq
Building inference algorithms from monad transformers. ~ Adam Ścibior et als. #Haskell
What is monad? ~ Kwang Yul Seo. #Haskell
Número de descomposiciones en diferencia de cuadrados. ~ Antonio Roldán. #Matemáticas #Programación
Selecting a platform (JavaScript vs Elm vs PureScript vs GHCjs vs Scalajs). ~ Isaac Shapira
A practical introduction to Functional Programming for Python coders. ~ Sachin Joglekar #FP #Python
Putting the science back in data science (Best practices and scalable workflows for reproducible data science). ~ D. Whitenack #DataScience
Invasion of the physicists. ~ John F. McGowan
Los 10 algoritmos más frecuentes que surgen en entrevistas de trabajo de programación. ~ @Alvy #Programación
Fun with hint. ~ Kwang Yul Seo. #Haskell
Characterology of programmers. ~ Konrad Kokosa #Programming
Writer monad. ~ Kwang Yul Seo. #Haskell
A verified decision procedure for pseudo-boolean formulas. ~ T Philipp, A Tigunova #Coq #Haskell #Logic
Functional programming is not what you (probably) think. ~ Sean Toner #FunctionalProgramming
Stackage design choices: making Haskell curated package sets. ~ Michael Snoyman. #Haskell
¿Se puede liberar la programación del estilo de von Neumann? ~ F. Sancho #Programación
La otra cara del Big Data. ~ David Gómez-Ullate #BigData
Review: Weapons of Math Destruction. ~ Evelyn Lamb #BigData
Princeton Web Transparency & Accountability Project.
Looking for Haskell companies outside USA. #Haskell
Formal specification by Coq of Date and Darwen’s object/relational model. ~ A. Benabbou, S.N. Bahloul #Coq
Software inteligente que aprende a escribir software inteligente. ~ @Alvy #Programación #IA
AI software learns to make AI software. ~ Tom Simonite #Programming #IA
QuickCheck and magic of testing. ~ A. Kuleshevich #Haskell
Bernoulli numbers in Isabelle/HOL. ~ L. Bulwahn #IsabelleHOL #Math
Course: Functional systems in Haskell. ~ S. Kurtz #Haskell
An alpha-beta heuristic implementation of tic-tac-toe in Haskell. ~ S.G. Korenewych #Haskell
Graph algorithms in Prolog. ~ A.C. Volk #Prolog #Math
Interactive proof presentations with Cobra. ~ M. Ring, C. Lüth #Cobra #IsabelleHOL #Haskell #Scala
Haskell Weekly 39: News from the Haskell community (January 26 2017). #Haskell
Enumeration of words in context-free languages using Haskell. ~ W. Wieczorek #Haskell
Verifying a simple compiler using property-based random testing. ~ Pedro Vasconcelos #Haskell
The Monad Fear. ~ @xtendo_org #Haskell
Lux: New functional language for JVM builds on Haskell, Clojure, ML. ~ @syegulalp #Lux
The Lux Programming Language. #eBook #Lux
How AI is changing software development. ~ Esther Shein #Programming #AI
Formalization of polynomially bounded and negligible functions using the computer-aided proof-checking system Mizar. ~ H. Okazaki, Y. Futa #Mizar
Advent of code #16 solution: an algebra of bitstrings. ~ Brent Yorgey #Haskell
Monads for functional programming. ~ Philip Wadler #Haskell
How I learned Haskell. ~ Kwang Yul Seo. #Haskell
24 days of GHC extensions. #Haskell
Ethical considerations in Artificial Intelligence courses. ~ E. Burton et als.#AI
Tarski’s geometry and the euclidean plane in Mizar. ~ A. Grabowski, R. Coghetto. #Mizar
A tutorial on the universality and expressiveness of fold. ~ Graham Hutton #Haskell
Build your Haskell project continuously. ~ Kwang Yul Seo. #Haskell
Twin prime conjecture and the Pentium division bug. ~ J.D. Cook. #Math #CompSci
Rigor of TP (computer theorem proving) in educational engineering software. ~ W. Neuper #ATP
Monadic parsing in Haskell. ~ G. Hutton, E. Meijer #Haskell
A practical theory of programming. ~ E.C.R. Hehner #eBook #Programming
Functional programming per tutti. ~ Giancarlo Valente #FuncionalProgramming
Solutions to various Haskell problems on HackerRank For Work. ~ Chris Mckinlay. #Haskell
Haskell and Docker: Down the rabbit hole and back. ~ Deni Bertovic. #Haskell
Initial experiments with statistical conjecturing over large formal corpora. ~ T. Gauthier, C. Kaliszyk, J. Urban #ML #ATP
Monad transformers and modular interpreters. ~ S. Liang, P. Hudak, M. Jones #Haskell

Febrero 2017

Formal foundations of 3d geometry to model robot manipulators. ~ R. Affeldt, C. Cohen #Coq
Data types à la carte. ~ W. Swierstra #Haskell
GeeksforGeeks Practice: Platform to practice programming problems. #Programming
Haskell maxims and arrows. #Haskell
Intuition for time complexity of algorithms. #Algorithms
An introduction into philosophy of science for software engineers. ~ Daniel Méndez.
Meaning, truth, and physics. ~ László E. Szabó
Tarski’s geometry and the euclidean plane in Mizar. ~ A. Grabowski, R. Coghetto #ITP #Mizar #Math
The Zipper. ~ G. Huet #OCaml
What’s functional programming all about? ~ Li Haoyi. #FuncionalProgramming
Type-level insertion sort. ~ Kwang Yul Seo. #Haskell
A linear algebra formulation for boolean satisfiability testing. ~ C. Fang, J. Liu #Logic
How to read “Pearls of functional algorithm design”. ~ Kim-Ee Yeoh #FunctionalProgramming #Haskell
What is category theory anyway? ~ Tai-Danae Bradley. #Math
What is a category? Definition and examples. ~ Tai-Danae Bradley #Math
What is a functor? Definitions and examples, part 1. ~ Tai-Danae Bradley. #Math
What is a functor? Definitions and examples, part 2. ~ Tai-Danae Bradley. #Math
Haskell Weekly 40: News from the Haskell community (February 2 2017). #Haskell
Easing Haskell’s intimidating glare. ~ James Bowen #Haskell
The easiest Haskell idiom. ~ James Bowen #Haskell
Haskell Bits #1: Randomness. ~ Ben Kovach. #Haskell
El mapa de las matemáticas. ~ @Alvy #Matemáticas
Map of Mathematics poster (All of mathematics summarised in one poster). ~ Dominic Walliman #Math
Context reduction. ~ Kwang Yul Seo. #Haskell
Refining authenticated key agreement with strong adversaries. ~ J. Lallemand & C. Sprenger #IsabelleHOL
Software verification/validation methods and tools … or practical formal methods. ~ John Rushby
Haskell bits #2: Application beginnings. ~ Ben Kovach. #Haskell
Unsolved problems in AI. ~ Simon Andersson #AI
Démontrer sans donner la preuve! ~ Fabrice Benhamouda #Math #CompSci
Req: Easy-to-use, type-safe, expandable, high-level HTTP library. ~ Mark Karpov #Haskell
Stream fusion: From lists to streams to nothing at all. ~ D. Coutts, R. Leshchinskiy, D. Stewart #Haskell
Miscomputation in software: Learning to live with errors. ~ Tomas Petricek #Programming
Categories in theory and in Haskell. ~ Ben Kovach. #Haskell
Monoids in theory and in Haskell. ~ Ben Kovach. #Haskell
Posting to Twitter via HTTP in Haskell. ~ Ben Kovach. #Haskell
Applicative functors. ~ Bartosz Milewski. #Haskell
Applicatives: One step further. ~ James Bowen #Haskell
Code your own QuickCheck. #Haskell
A practical guide to formalised mathematics in Isabelle. ~ A. Hicks, J. Siqueira #IsabelleHOL #Math
Why prove programs equivalent when your compiler can do that for you? ~ Joachim Breitner. #Haskell
Famous problems in the history of Mathematics. ~ Isaac Reed #Math
Reified dictionaries. ~ Kwang Yul Seo. #Haskell
Reluplex: An efficient SMT solver for verifying deep neural networks. ~ G. Kat et als. #SMT
Modeling and simulating Markov chain evolution. ~ Ben Kovach. #Haskell
The TAO of monad. ~ Bartosz Milewski. #Haskell
Computer proof assistants (the future of mathematics). ~ Vladimir Voevodsky #ITP #Math
The factorization algorithm of Berlekamp and Zassenhaus. ~ J. Divasón et als. #IsabelleHOL #Math
Tidying up trivial details (the value of abstract mathematics). ~ J.D. Cook. #Math
Functional pearl: Compiling a fifty year journey. ~ G. Hutton, P. Bahr #Haskell
Haskell Weekly 41: News from the Haskell community (February 9 2017). #Haskell
Monads in category theory for laymen. ~ AndyShiue #Haskell
Haskell on Bash/WSL. ~ Rich Turner #Haskell
Stone relation algebras in Isabelle/HOL. ~ W. Guttmann #ITP #IsabelleHOL #Math
Code your own QuickCheck (HOF). Part 2 #Haskell
Supercomputers for quantum computers.
GHC generics explained. ~ M. Karpov #Haskell
Haskell implementation of the Abelian sandpile model using Gloss. #Haskell #Gloss
Haskell implementation of the Abelian sandpile model using CodeWorld. ~ C. Smith #Haskell #CodeWorld
Computational logic for computer science. ~ M. Ayala-Rincón & F.L.C. de Moura #Logic
Lecture notes on Haskell programming. ~ L. Padovani #Haskell
Unbounded spigot algorithms for the digits of pi. ~ J. Gibbons #Haskell #Math #Pi
Computing the digits in π. ~ C.D. Offner #Math #Algorithms #Pi
A formal study of boolean games with random formulas as pay functions. ~ E. Martin-Dorel & S. Soloviev #ITP #Coq
Stricter JSON parsing with Haskell and Aeson. ~ A. Raghavan #Haskell
Arithmetical theorems with Lambda Calculus. ~ Shubham Jain #Haskell
Bootstrapping Haskell. ~ rekado #Haskell
Code your own QuickCheck (Shrink). ~ DeQue #Haskell
El cerebro artificial que piensa por ti. ~ Joseba Elola #IA
Cuando políticos de EE UU decidieron que el número pi era 3,2. ~ M. Ansede #Matemáticas
Using functional programming in Python like a boss: generators, iterators and decorators. #Python
Programación funcional en Python. ~ D. Sánchez #Python
Soundness and completeness proofs by coinductive methods. ~ J. C. Blanchette, A. Popescu, D. Traytel #IsabelleHOL #Logic
Abstract soundness in Isabelle/HOL.~ J. C. Blanchette, A. Popescu, D. Traytel #IsabelleHOL #Logic
The Haskell programmer’s guide to the IO Monad (don’t panic). ~ S. Klinger #Haskell #Math
Differential dynamic logic. ~ B. Bohrer #IsabelleHOL #Logic
Haskell bits #3: Connecting to databases. ~ Ben Kovach. #Haskell
Mastering time-to-market with Haskell. ~ Chris Done. #Haskell
Playing with QuickCheck on an arithmetic DSL. ~ DeQue #Haskell
VMDV: A 3D visualization tool for modeling, demonstration, and verification. ~ Jian Liu et als. #ATP #ITP
How to sell excellence. ~ Michael O. Church #Haskell
Thought experiments in mathematics. ~ I. Starikova & M. Giaquinto #Math
Replacing GHCi’s pretty-printer. ~ Tim Humphries #Haskell
Quasiquoters for XML and HTML documents in Haskell. ~ Dennis Gosnell. #Haskell
Trees that grow. ~ S. Najd & Simon Peyton Jones #Haskell
Better exception messages. ~ Michael Snoyman. #Haskell
QuickCheck is fun, deal with it. ~ DeQue #Haskell
Local lexing. ~ S. Obua, P. Scott & J. Fleuriot #IsabelleHOL
Creación de ficheros LaTeX con GNU Emacs. ~ Joaquín Ataz López #LaTeX #Emacs
y-cruncher: A multi-threaded pi-program. ~ Alexander J. Yee #Math #Programming #Pi
Theorem proving based on semantics of DNA strand graph. ~ K.S. Ray & M. Mondal #ATP
Euterpea: A Haskell library for music creation. #Haskell #Music
Ten example uses of Monads. ~ Philipp Schuster #Haskell
Entrenamiento de redes neuronales: mejorando el gradiente descendiente. ~ F. Sancho #IA
The Curry-Howard correspondence between programs and proofs. ~ G. Gonzalez #Haskell #Logic
From math to machine: translating a function to machine code. ~ Brian Steffens. #Haskell #Math
El isomorfismo de Curry-Howard y una introducción a Coq. ~ M. Román #Lógica #Coq
La tiranía de las publicaciones. ~ F. Sancho. #Investigación
How to read and write (with monads!) ~ James Bowen._OWA #Haskell
Development and verification of a proof assistant. ~ A.B. Jensen. #Thesis #Logic #IsabelleHOL
To be or not to be constructive (that is not the question). ~ Sam Sanders #Math #Logic
Synthesizing imperative programs for introductory programming assignments. ~ Sunbeom So, Hakjoo Oh #Programming
Optimal Emacs settings for org-mode for literate programming. ~ F. Giasson #Emacs #Programming
Emacs magical syntax highlighting for LaTeX-mode buffers. #LaTeX #Emacs
Mathematical notation in Emacs. ~ Eric Kaschalk #Emacs
Effective array computation in Haskell (Because we all want highly performant and beautiful code). ~ Samuel Schlesinger #Haskell #Math
All hail geometric algebra! ~ Ben Lynn #Haskell #Math
From Atbash to Enigma: 2500 years of cryptography in a few lines of Haskell. ~ Ben Lynn #Haskell #Cryptography
Hello Elm and Haskell! ~ Mark Bucciarelli. #Elm #Haskell
Maxima was elected as the Sourceforge February 2017 Community Project of the Month. #Maxima #Math
Haskell sorcery. ~ Ben Lynn #Haskell
Making money using math: Modern applications are increasingly using probabilistic machine-learned models. ~ E. Meijer
Inteligencia artificial que programa robando código de otros programas. ~ Nacho Palou. #IA
AI learns to write its own code by stealing from other programs. ~ Matt Reynolds #AI
The notion of software language. ~ Ralf Lämmel
Haskell Bits #4: Environment variables. ~ Ben Kovach. #Haskell
Relational convolution, generalised modalities and incidence algebras. ~ B. Dongol, I.J. Hayes, G. Struth #IsabelleHOL
Signed sets and ballots, part 2. ~ Brent Yorgey #Haskell
Brute force for beginners. ~ Ben Lynn #Haskell
Browser games in Haskell. ~ Ben Lynn #Haskell #Games
A problem with I/O. ~ Ben Lynn #Haskell
Basics of R. ~ Charles J. Geyer #Rstats
Model checking: an introduction to bisimulation. ~ Hans-Dieter Hiep #Haskell
Introducción a generar sitios web estáticos con Hakyll. ~ Anler Hernández Peral #Haskell Código
Fun and games in Emacs. ~ Mickey Petersen #Emacs
DeepCoder: learning to write programs. ~ M. Balog et als. #DeepLearning
Menger’s theorem in Isabelle/HOL. ~ C. Dittmann #IsabelleHOL
Bug-free code. ~ Ben Lynn #Haskell #Math
Aplicative programming with naperian functors. ~ J. Gibbons #Haskell
Dimensional: a library providing data types for performing arithmetic with physical quantities and units. #Haskell
Haskell type constraints unleashed. ~ D. Orchard, T. Schrijvers #Haskell
Refining authenticated key agreement with strong adversaries. ~ J. Lallemand, C. Sprenge #IsabelleHOL
Parser combinators. ~ Ben Lynn #Haskell

Marzo 2017

Computer-aided methods for social choice theory. ~ C. Geist, D. Peters #ATP
GHCi in the browser. ~ @replit #Haskell
Code that counts: Combinatorial calculations with combinator calculus. ~ Ben Lynn #Haskell #Math
Computability theory, nonstandard analysis, and their connections. ~ D. Normann, S. Sanders #Math #CompSci
Awesome Haskell: some of the most popular and actively developed packages. #Haskell
How we secretly introduced Haskell and got away with it. ~ Arian van Putten & Ruud van Asseldonk #Haskell
Autosubst: Automation for de Bruijn syntax and substitution in Coq. #Coq
The monadic state of mind. ~ James Bowen. #Haskell
Laziness in action. ~ Ben Lynn #Haskell
Haskell, Redis, Mailgun and Heroku Scheduler. ~ Ecky Putrady. #Haskel
Proofs of functor laws in Haskell. ~ Siva Somayyajula #Haskell
How to sell FP? ~ Denis Redozubov. #FuncionalProgramming #Haskell
Homogeneous geometric algebra. ~ Ben Lynn #Haskell #Math
The group law for elliptic curves in Isabelle/HOL. ~ S. Berghofer #IsabelleHOL #Math #CompSci
Conformal geometric algebra. ~ Ben Lynn #Haskell #Math
Proof refinement basics. ~ Darryl #Haskell #Logic
In depth overview of Elm and Purescript. Lessons learned porting a game from Purescript to Elm. ~ Marco Sampellegrini. #Haskell #Elm #Purescript
The typed-process library. ~ Michael Snoyman. #Haskell
The Lisp approach to AI (Part 1). ~ S. Valencia #Lisp #IA
Notes on Coursera’s functional programming principles in Scala. ~ G. Kunigami. #FunctionalProgramming #Scala
Seeing theory: a visual introduction to probability and statistics. ~ Daniel Kunin #Math #Statistics.
Au pays des illuminés du nombre Pi. ~Jean-Paul Delahaye #Math
Le nombre Pi est partout. ~ Jean-Paul Delahaye #Math
The reasonable effectiveness of the Multiplicative Weights Update Algorithm. ~ Jeremy Kun | Math ∩ Programming #Algorithms
Parity games, separations, and the modal μ-calculus. ~ C. Dittmann #PhD_Thesis #IsabelleHOL
Get a brain (neural network in Haskell). ~ Ben Lynn #Haskell #Math
A minimalistic, elegant and powerful approach to working with graphs in a functional programming language. #Haskell
A library for algebraic construction and manipulation of graphs in Haskell. #Haskell
A “proof by contradiction” is not a proof that ends with a contradiction. ~ R. Harper #Logic
Una introducción al pensamiento crítico en 32 cómodos vídeos y un MOOC. ~ @Wicho
First hint of how DNA calculators could supercharge computing. ~ M. Reynolds #Computing #DNA
Microsoft’s AI is learning to write code by itself, not steal it. #Programming #AI
Proof checker for forall x: Cambridge and Calgary. ~ R. Zach. #Logic
El boom de la Inteligencia Artificial. #IA
Codifican una película en ADN y la vuelven a recuperar. | Principia Marsupia #Computación
DNA Fountain enables a robust and efficient storage architecture. ~ Y. Erlich, D. Zielinski #CompSci
Computer-aided mathematical proof, Cambridge (England), 10-14 July 2017. #ITP #Logic #Math #CompSci
Analysis of an ontological proof proposed by Leibniz. ~ M. Bentert et als. #IsabelleHOL
Five years with Kattis: using an automated assessment system in teaching. ~ E. Enström et als. #Teaching #Programming
Dependency grammars as Haskell programs. ~ T. Obrebski #Haskell
First-order logic according to Harrison. ~ AB Jensen, A Schlichtkrull, J Villadsen #IsabelleHOL #Logic
Highly automated formal verification of arithmetic circuits. ~ A Sayed-Ahmed #PhD_thesis
NASA Software Catalog 2017-2018.
Is computer security possible? ~ RJ Lipton, KW Regan #CompSci
Structure-aware version control (A generic approach using Agda). ~ V. Cacciari, W. Swierstra #Agda #Haskell
Rewarding Disobedience. ~ MIT Media Lab
Partial patterns in do blocks: let vs return. ~ M. Snoyman. #Haskell
Emacs and Org mode resources. ~ Ben Elijah. #Emacs #OrgMode
Abstract algebra: theory and applications. ~ T.W. Judson & R.A. Beezer #Math #Sage #eBook
Profunctors, arrows, & static analysis. ~ Will Fancher #Haskell
Reading is a profoundly creative act. ~ E. Wallingford #Teaching #Learning
Inteligencia artificial: algoritmos genéticos. ~ Daniel Riera #IA
When you should use lists in Haskell (mostly, you should not). ~ J. Waldmann #Haskell
What’s in a fold: The basic catamorphism in recursion-schemes. ~ Duplode #Haskell
A monadic framework for relational verification (Functional pearl). ~ N. Grimm et als. #Fstar
Isotope: a chemistry library for calculating masses of elements and molecules. ~ M. Thomas #Haskell
Mathematical balance of trade. ~ J.D. Cook. #Math
How areas of math are connected. ~ J.D. Cook. #Math
Will democracy survive big data and artificial intelligence? ~ Dirk Helbing et als. #AI
Introduction to formal concept analysis and its applications in information retrieval and related fields. ~ D.I. Ignatov #AFC
Making a simple parametric Parser which is both a Functor and Applicative in Haskell!. ~ @sam2code #Haskell
Formalizing restriction categories. ~ J. Chapman, T. Uustalu & N. Veltri #ITP #Agda
Haskell programming tips. ~ HaskellWiki #Haskell
Why types matter. ~ Slavomir Kaslev. #Haskell #Logic #CompSci
Intro to Haskell syntax. ~ Andrew Gibiansky #Haskell
Your first Haskell application (with Gloss). ~ Andrew Gibiansky #Haskell
Typeclasses: Polymorphism in Haskell. ~ Andrew Gibiansky #Haskell
Abstraction in Haskell (Monoids, Functors, Monads). ~ Andrew Gibiansky #Haskell
Algebras for Monads. ~ Bartosz Milewski. #Haskell
The Haskell Performance Resource: the collected wisdom on how to make your Haskell programs go faster. ~ HaskellWiki #Haskell
The Euler–MacLaurin formula in Isabelle/HOL. ~ Manuel Eberl #ITP #IsabelleHOL #Math
Fundamentos matemáticos del aprendizaje (I). ~ F. Sancho. #IA
Minimal Cabal files. ~ J.P. Villa. #Haskell
Haskell from C: Where are the for Loops? ~ C. Scherrer #Haskell
My first Idris proof. ~ A. Kaygun. #Idris
Papers We Love: John Reynolds, Definitional interpreters for Higher-Order Languages, now in Haskell. #Haskell
An efficient proof-producing framework for formula processing. ~ H. Barbosa, J.C. Blanchette, P. Fontaine #IsabelleHOL
Solving a game book, as blog post series about modelling and optimization. ~ @bartavelle #Haskell
Children of the miracle: from Algol to Prolog. ~ Maarten van Emden #Programming #History
Amortization and persistence via lazy evaluation. ~ G. Kunigami. #DataStructures #OCaml
Fully mechanized proofs of Dilworths theorem and Mirskys theorem. ~ Abhishek Kr Singh #ITP #Coq #Math
Interactive theorem proving in Coq and the Curry-Howard isomorphism. ~ Abhishek Kr Singh #ITP #Coq #Math
IsarMathLib (a library of formalized mathematics) updated to Isabelle2016-1. #ITP #Isabelle #Math
A specification for dependently-typed Haskell. ~ S. Weirich et als. #Haskell #Coq
Formalization of the arithmetization of euclidean plane geometry and applications. ~ P Boutry, G Braun, J Narboux #ITP #Coq #Math
Parallel postulates and continuity axioms: a mechanized study in intuitionistic logic using Coq. ~ P. Boutry et als, #Coq
Inlining and specialisation. ~ Matthew Pickering #Haskell
Applicative sorting. ~ Will Fancher. #Haskell
Obey the (type) laws! ~ James Bowen #Haskell
CYP (short for “Check Your Proof”) verifies proofs about Haskell-like programs. ~ L. Noschinski #Haskell #Logic
Analysing privacy analyses. ~ G Bella, D Butin, H Jonker #IsabelleHOL
Type-level insertion sort. ~ Kwang Yul Seo. #Haskell
Haskell concepts in one sentence. ~ Joseph Cieslik #Haskell
How Aristotle created the computer. ~ Chris Dixon #History #CompSci #Logic
Do you know how much your computer can do in a second? ~ @kamalmarhubi @b0rk #Programming
Category theory for the sciences. ~ David I. Spivak #eBook #Math #CompSci
Thinking functionally with Clojure. ~ J. Stevenson. #FP #Clojure
Logic Production Systems (LPS): A new mixed logic/imperative programming language. ~ Bob Kowalski and Fariba Sadri. #Logic #Programming
Towards an implementation of a functional interpretation for nonstandard arithmetic. ~ C. Xu #ITP #Agda #Math
Learning to learn Haskell. ~ James Bowen. #Haskell
Category theory made easy with (ugly) pictures. ~ Ashwin Rao #Haskell #Math
22 trucos para ser un ninja de Ubuntu.
An axiomatic formalisation of trigonometric functions in Isabelle. ~ I.I. Morris #ITP #IsabelleHOL #Math
Certifying a file system using Crash Hoare Logic: correctness in the presence of crashes. ~ T. Chajed et als. #Coq
Mathematical reasoning. Writing and proof. ~ T. Sundstrom #eBook #Math

Abril 2017

ProofScript: Proof scripting for the masses. ~ S. Obua, P. Scott, J. Fleuriot #ProofScript
ProofPeer: Collaborative theorem proving. ~ S. Obua, J. Fleuriot, P. Scott, D. Aspinall #ITP #ProofPeer
ProofScript: the language component of ProofPeer.
Universal reasoning, rational argumentation and human-machine interaction. ~ C. Benzmüller #ITP
Principles of probabilistic programming. ~ J.P. Katoen
Correct safety critical hardware descriptions via static analysis and theorem proving. ~ N. Moore, M. Lawford #ITP #PVS
Verify your typeclass instances in Haskell today! ~ Justin Le #Haskell
Formalization of some central theorems in combinatorics of finite sets. ~ A.K. Singh #ITP #Coq #Math
Lazy priority heap. @__josejuan__ #Haskell
Introduction to functional programming. ~ Fraser Tweedale. #Haskell #OCaml #Scala
Implementing Goodstein. ~ Ken T Takusagawa #Haskell
Expected shape of random binary search trees in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #Algorithms
La carrera por el ordenador cuántico. ~ D. Manzano #Computación
The race to quantum technologies and quantum computers (useful links). ~ Gil Kalai #CompSci
The power of Prolog. ~ Markus Triska #eBook #Prolog
When is UndecidableInstances safe? ~ Dennis Gosnell. #Haskell
2 + 2 = 5… !? and why compiler warnings are good. ~ @jezenthomas #Haskell
A beginner-friendly step by step tutorial for Reflex-Dom. #Haskell
Accelerate: High-performance parallel arrays for Haskell. #Haskell
Neural networks, types, and functional programming. ~ C. Olah. #Haskell
The theory of subresultants and the subresultant polynomial remainder sequence in Isabelle/HOL. ~ S. Joosten et als. #IsabelleHOL
Speaking Logic (propositional, modal, equational, first-order, and higher-order logic). ~ N. Shankar #Logic
Type theory (in “Sixth Summer School on Formal Techniques”). ~ Stéphane Graham-Lengrand #Logic #CompSci
Automated deduction for verification. ~ N. Shankar #ATP #ITP #Logic #CompSci
Satisfiability Modulo Theories. ~ Clark Barrett #Logic #CompSci
Eleven reasons to use Haskell as a mathematician. ~ Dan Piponi. #Haskell #Math
Evolution and adoption of programming languages. ~ A. Jain, M. Gupta #Programming
ediprolog: Emacs does interactive Prolog. ~ Markus Triska #Emacs #Prolog
Variations on noetherianness. ~ D. Firsov, T. Uustalu, N. Veltri #ITP #Agda #Math
Natural numbers with addition form a monoid. ~ James Chapman #Tutorial #Agda
MIU (puzzle from Douglas Hofstadter’s book “Gödel, Escher, Bach”) in Haskell. ~ Wolfgang Jeltsch #Haskell #Logic
Generic programming in Haskell. ~ Wolfgang Jeltsch #Haskell
An introduction to category theory and categorical logic. ~ Wolfgang Jeltsch #Logic
Dependently typed programming and theorem proving in Haskell.~ Wolfgang Jeltsch #Logic #Haskell #Agda
BayHac (the Bay Area Haskell Hackathon) 2017 summary! ~ James Bowen #Haskell
CodeWorld and Summer of Haskell 2017. ~ Chris Smith #Haskell
Summer of Haskell 2017. #Haskell
Profunctor optics (modular data accessors). ~ M Pickering, J Gibbons, N Wu #Haskell
AutoDraw: Fast drawing for everyone. #AI #ML
Cómo convertirte en un artista con Autodraw de Google. ~ M. Marcaletti #IA #AutoDraw
Introduction to type theory. ~ Herman Geuvers #Math #Logic
On recursion, continuations and trampolines. ~ Eli Bendersky. #Python #Clojure
A programmer’s guide To R: The vector, vector expressions & attributes. ~ Mike James #RStats
Data science, Python and the functional programming revolution. ~ Holger Peters #DataScience #Python #FuncionalProgramming
Functional programming in R: Advanced statistical programming for data science, analysis and finance. ~ Thomas Mailund #RStats
All about Applicative. ~ Adelbert Chang #Haskell
Lazy dynamic programming. ~ Tikhon Jelvis #Haskell
NStack: Composable, typed streams and microservices for data analytics. #Haskell #DataScience
Dante: Emacs mode for Interactive Haskell. ~ Jean-Philippe Bernardy #Haskell #Emacs
Modern functional programming. ~ R. Eisenberg #Haskell #Course
Dependent types in Haskell: theory and practice. ~ R.A. Eisenberg #PhD_Thesis #Haskell
CodeWorld: The why, what, and how of teaching Haskell to children. ~ Chris Smith #Haskell
CID project: Computing with Infinite Data. #CompSci #Logic #Math
Dependent types in GHC. ~ J. Leo #Haskell
TensorFlow Haskell API. ~ J. Jacobson, F. Mayle, G. Steuck #Haskell
Adjunctions in everyday life (Or: what we talk about when we talk about monads). ~ Rúnar Bjarnason #Haskell
Don’t eff it up: freer monads in action. ~ Sandy Maguire #Haskell
Elsa: a lambda calculus evaluator. ~ R. Jhala #Haskell #Logic
Testing a saturation-based theorem prover: Experiences and challenges. ~ G. Reger, M. Suda, A. Voronkov #ATP #Logic
Symbolic computation and automated reasoning for program analysis. ~ L. Kovacs #ATP
Category theory applied to functional programming [PDF]. ~ J.P. Villa #Haskell #Agda #Math #eBook
Category theory applied to functional programming [Code]. ~ J.P. Villa #Haskell #Agda #Math #eBook
What pure functional programming is all about: Part 1. ~ Chris Done #Haskell #FP
Competitive programmer’s Handbook. ~ A. Laaksonen #Programming
Programming in the point-free style. ~ Eirik Tsarpalis #PF #Fsharp
These, Align, and Crosswalk. ~ Tim Humphries #Haskell
Hedgehog: a modern property-based testing system, in the spirit of QuickCheck. #Haskell
Computer aided formal reasoning. ~ T. Altenkirch #ITP #Agda
Formalizing mathematical knowledge as a biform theory graph: a case study. ~ J. Carette, W.M. Farmer #ITP #Agda
Verification of sampled-data systems using Coq. ~ D. Ricketts #PhD_Thesis #Coq
Haskell and deliberate practice. ~ James Bowen #Haskell
Descending sort in Haskell. ~ R. Cheplyaka #Haskell
There is no Haskell topology. ~ Semantic Dreams #Haskell #Math
A Coq tactic for equality learning in linear arithmetic. ~ S. Boulmé, A. Maréchal #ITP #Coq #Math
Submitting Haskell functions to Z3. ~ John Wiegley #Haskell
SAS para aprendizaje automático y Haskell para ciencia de datos. #Haskell #DataScience
Trouble with Tribbles. ~ Dominic Steinitz #Haskell
Computación cuántica (I): el fin de los ordenadores clásicos. ~ Robert Clarisó #Computación
Modern software development with Haskell. ~ Runar Bjarnason #Haskell
Some good “Statistics for programmers” resources. ~ Julia Evans #Statistics #Programming
Introducción a Elm a través de sistemas de tipos. ~ @anler #Elm #FunctionalProgramming
EPTL: A temporal logic for weakly consistent systems. ~ M Weber, A Bieniusa, A Poetzsch-Heffter #IsabelleHOL #Logic
HOPS: a DSL for power series and integer sequences. ~ Anders Claesson #Haskell #Math
CodeWorld-API: Graphics library for CodeWorld. ~ Chris Smith #Haskell #CodeWorld
Refinement reflection on ADTs: Lists are Monoids. ~ Niki Vazou #Haskell #LiquidHaskell
The influence of dependent types. ~ Stephanie Weirich #Haskell
Applicatives and Alternatives. ~ @queertypes #Haskell
Solvers for type recovery and decompilation of binaries. ~ Ed Robbins #PhD_Thesis #SMT #CHR
Haskell is a great imperative language. ~ Chris Martin #Haskell
Lambda calculus in Haskell. ~ S. Diehl #Haskell #Logic
7 lines of code, 3 minutes: Implement a programming language from scratch. ~ Matthew Might #Racket
500 Data structures and algorithms interview questions and their solutions. ~ Vivek Srivastava #Programming
CodeWorld: Teaching Haskell to childre (Video). ~ Chris Smith #Haskell
How to create a new Haskell project (Video) ~ G. Gonzalez #Haskell
How to create a new Haskell project (Slides) ~ G. Gonzalez #Haskell
Verifying safety of functional programs with Rosette/Unbound. ~ D Mordvinov, G Fedyukovich #Verification #FuncionalProgramming
QuickCheck: a lightweight tool for random testing Haskell programs. ~ W. Swierstra #Haskell #QuickCheck
Computación cuántica (II): un nuevo paradigma. ~ Robert Clarisó #Computación
The pebbling comonad in finite model theory. ~ S Abramsky, A Dawar, P Wang #Logic #FunctionalProgramming
Why functional programming? (11 reasons to learn functional programming). #FunctionalProgramming
Naperian tensors. #Haskell
xmonad in Coq (experience report): Programming a window manager with a proof assistant. ~ W. Swierstra #Coq #Haskell
The water jug problem in Hedgehog. ~ E.A. Alvarez #Haskell
Functional programming made easy: Here comes Eta. #FunctionalProgramming
Improving Haskell types with SMT. I.S. Diatchki #Haskell #SMT
Embedding the refinement calculus in Coq. ~ J. Alpuim, W. Swierstra #Coq
Verifying data structures in Haskell. ~ D.O. Kidney #Haskell
Basic type level programming in Haskell. ~ @mattoflambda #Haskell
Structure-aware version control: A generic approach using Agda. ~ V. Cacciari, W. Swierstra #Agda #Haskell
hs-to-coq: Convert Haskell source code to Coq source code. ~ Antal Spector-Zabusky #Haskell #Coq
Counting objects up to isomorphism: groupoid cardinality. ~ T. Tao #Math
Programming as a way of thinking. ~ A. Downey #Programming #Python
AITP 2017: The Second Conference on Artificial Intelligence and Theorem Proving. (Abstracts of the talks). #AI #ATP #ITP
A basis for a mathematical theory of computation. ~ J. McCarthy #Math #CompSci
What has Artificial Intelligence ever done for us? (formalizers). ~ J. Harrison #AI #ATP #ITP
Deep reasoning: a vision for automated deduction. ~ S. Schulz #AI #ATP
Deep Prolog: End-to-end differentiable proving in knowledge bases. ~ T. Rocktäschel #DeepLearning #Prolog
Refinement: a reflection on proofs and computations. ~ C. Cohen & D. Rouhling #Coq
On the formalization of foundations of Tarski’s system of geometry. ~ P Boutry #Math #Coq
Lifts for free: making mtl typeclasses derivable. ~ Alexis King #Haskell
Learning Cryptography, math and programming with Cryptol. ~ Dylan McNamee #Math #Haskell #Cryptol
FindStat: The Combinatorial Statistic Finder. ~ M. Rubey, C. Stump, et als. #Programming #Math
LMFDB: an extensive database of mathematical objects arising in Number Theory. #Math
Tapping sources of Mathematical (Big) Data. ~ M. Kohlhase #MKM
Laziness, impatience, hubris Larry Wall (Programming Perl) #Quote #Programming
Logic tensor networks: Deep learning and logical reasoning from data and knowledge. ~ L. Serafini & A. d’Avila #Logic #DeepLearning
What can logic do for AI? ~ David McAllester #Logic #AI
An Isabelle formalization of the expressiveness of deep learning. ~ A. Bentkamp #MsC_Thesis #IsabelleHOL #DeepLearning
math.wikipedia.org: A vision for a collaborative semi-formal, language independent math(s) encyclopedia. ~ J. Corneli & M. Schubotz
Learning-assisted theorem proving and formalization. ~ J. Urban #AI #ATP #ITP
Towards AI methods for clause selection. ~ J. Jakubův, J. Urban & B. Veroff #AI #ATP #Logic

Mayo 2017

A formal proof of the expressiveness of deep learning. ~ A. Bentkamp, J.C. Blanchette & D. Klakow #IsabelleHOL #DeepLearning
A tutorial for using Emacs with Haskell projects. #Haskell #Emacs
Quotient inductive types & their dual. #Haskell
The programming language of mathematics. ~ Vladimir Kirillov #Math
DeepAlgebra: an outline of a program. ~ P. Chojecki #ITP #Coq #Math
April 2017 1HaskellADay problems and solutions. ~ @geophf | Typed Logic #Haskell #1HaskellADay
Open Sourcing our new Duckling (more Haskell at Facebook). ~ Team Wit #Haskell
A Python implementation of Douglas Hofstadter formal systems, from his book “Gödel, Escher, Bach”. #Logic #Python
Putting your Haskell to the test! ~ James Bowen #Haskell
Filopodia: open source projects, mostly related to data science, machine learning and statistics in Haskell. #Haskell #DataScience
Types, tableaus and Gödel’s God in Isabelle/HOL. ~ D. Fuenmayor & C. Benzmüller #IsabelleHOL #Logic
I tried Haskell for 5 years and here’s how it was. ~ L.P. Coelho #Haskell
Universal reasoning, rational argumentation and human-machine interaction. ~ C. Benzmüller #ITP #Logic
Functional programming and proving in Isabelle/HOL. ~ A. Lochbihler #FunctionalProgramming #IsabelleHOL
Using mathematical induction to design computer algorithms. ~ U. Manber #Algorithms
Duckling: Language, engine, and tooling for expressing, testing, and evaluating composable language rules on input strings. #Haskell
The graphviz library: Bindings Haskell to Graphviz for graph visualisation. ~ M. Sackman & I.L. Miljenovic #Haskell #Graphviz
Haphviz: Graphviz code generation with Haskell. #Haskell #Graphviz
The Cayley-Dickson construction in ACL2. ~ J. Cowles & R. Gamboa #ACL2 #ITP #Math
Técnicas de diseño de algoritmos. ~ R. Guerequeta y A. Vallecillo #Libro #Algorítmica
Course “Data structures and functional programming”: Lecture notes. ~ R.L. Constable #FunctionalProgramming #OCaml
Homotopy Type Theory in Lean. ~ U. Buchholtz, F. van Doorn & J. von Raumer #ITP #Lean #HoTT
Monads are monoid objects. ~ J. Wiegley #ITP #Coq
Data analysis with Monoids. ~ Tim Docker #Haskell
What a Haskell study group is not. ~ Steven Syrek #Haskell
Some notes on Haskell pedagogy. ~ Steven Syrek #Haskell
Monoidal categories in Isabelle/HOL. ~ E.W. Stark #ITP #IsabelleHOL #Math
A puzzle about game review scoring in Haskell. ~ Vladimir Slepnev #Haskell
Formal verification of a floating-point expansion renormalization algorithm. ~ S. Boldo et als. #ITP #Coq #Math
Proving stuff with Idris. ~ Neil Mitchell #Idris #Haskell
A formally verified compiler for Lustre. ~ T. Bourke et als. #Coq
Let Idris take care of you: variable binding. | Crunchy Type #Idris #Haskell
New release of SBV (a library for seamlessly integrating SMT solvers with Haskell), now with optimization. ~ L. Erkok #Haskell #SMT
The Floyd-Warshall algorithm for shortest paths in Isabelle/HOL. ~ S. Wimmer & P. Lammich #IsabelleHOL
Nested multisets, hereditary multisets, and syntactic ordinals in Isabelle/HOL. ~ J.C. Blanchette et als. #IsabelleHOL
Teaching new tricks to old programs. ~ Conal Elliott #Haskell
Dynamic dispatch in Haskell, or: how can I make my code extendable? #Haskell
Learning of human-like algebraic reasoning using deep feedforward neural networks. ~ C.H. Cai et als. #ATP #ML
On the history of the minimum spanning tree problem. ~ R.L. Graham & P. Hell #Algorithms
Trees: a mathematical tool for all seasons. ~ Joe Malkevitch #Algorithms
CryptHOL: a framework for formalising cryptographic arguments in Isabelle/HOL. ~ A. Lochbihler #IsabelleHOL
Game-based cryptography in HOL. ~ A. Lochbihler, S. Reza & B. Bhatt #IsabelleHOL
The most unreliable technique in the world to compute pi. ~ J. Karczmarczuk #Haskell #Math
Experience report: Haskell and mathematics. ~ H. Thielemann #Haskell #Math
Lazy processing and optimization of discrete sequences. ~ J. Karczmarczuk #Haskell #Math
Programming with bananas and barbed wire. Part 1. ~ Michał Kawalec #Haskell
A persistent union-find data structure. ~ S. Conchon & J.C. Filliâtre #Coq
Tarjan’s Union-Find algorithm using Conchon & Filliâtre’s persistent arrays. #Haskell
Haskell library containing common graph search algorithms (depth-first, breadth-first, Dijkstra, and A*). #Haskell
A computationally surveyable proof of the group properties of an elliptic curve. ~ D.M. Russinoff #ACL2 #Math
De Pitágoras a la conjetura del millón de dólares. ~ Pedro Alegría #Matemáticas
Beal’s conjecture revisited. ~ Peter Norvig #Math #Python
El teorema de los cuatro colores (1): una historia que comienza en 1852. ~ Marta Macho Stadler #Matemáticas
El teorema de los cuatro colores (2): el error de Kempe y la clave de la prueba. ~ Marta Macho Stadler #Matemáticas
El mayor número primo conocido. ~ Miguel Ángel Morales #Matemáticas #Computación
¿Es posible usar Haskell más allá del mundo académico? ~ Ramiro Pastor #Haskell
Technology of deduction for “Systems that explain themselves”. ~ W. Neuper #ATP #ITP
Prototyping “Systems that explain themselves” for education. ~ W. Neuper #ITP #IsabelleHOL
Untangling Haskell’s strings. ~ James Bowen #Haskell
Summer school on satisfiability checking and symbolic computation.
Tree oriented programming in Haskell. ~ J.D. Fokker #Haskell
An introduction & supplement to Knuth’s introduction to addition chains. ~ B. Smith #Haskell
Proving fib equivalence. ~ Neil Mitchell #Haskell #Idris
AI and the origins of the functional programming language style. ~ M. Priestley #AI #FunctionalProgramming
A formalization of the process algebra CCS in HOL4. ~ Chun Tian #ITP #HOL4
Extendable data in Haskell (part 2). #Haskell
¿P=NP?: El problema que los informáticos no han podido resolver en 45 años. ~ R. Peña
Largest sets of subsequences in OCaml. ~ G. Kunigami #OCaml
Haskell, vectors and simple mechanics (part 2). ~ GitCommit #Haskell
The simplest Haskell priority queue implementation I know of. ~ Alfredo di Napoli #Haskell
Proof mining with dependent types. ~ E. Komendantskaya & J. Heras #Coq
Purely functional data structures. ~ Franz Thoma #Haskell
Deforestation and program fusion: applying equational transforms to automatically simplify programs. ~ R. Orendorff #Haskell
Grenade: Practical Deep Learning in Haskell. ~ Huw Campbell #Haskell #DeepLearning
Developing security protocols by refinement in Isabelle/HOL. ~ C. Sprenger & I. Somaini #ITP #IsabelleHOL
Curvas que separan: fácil de entender, difícil de demostrar. ~ Miguel Ángel Morales #Matemáticas
An illustrated book of bad arguments. ~ Ali Almossawi #Logic
El teorema de los cuatro colores (3): ¿un ordenador resuelve el problema? ~ Marta Macho #Matemáticas #Computación
Automating the proofs of strengthening Lemmas in the Abella proof assistant. ~ D. Michaelson #ITP #Abella
Blunt converts Haskell expressions between the pointfree and pointful styles. #Haskell
Write more understandable Haskell with Flow. ~ Taylor Fausak #Haskell
Realizing Hackett, a metaprogrammable Haskell. ~ Alexis King #Haskell #Racket #Hackett
An opinionated survey of functional Web development. ~ Yoran Heling #Haskell #OCaml
Formalized Lambek calculus in Higher Order Logic (HOL4). ~ Chun Tian #ITP #HOL4
Lock-step simulation is child’s play. ~ J. Breitner & C. Smith #Haskell #CodeWorld
The lambda calculus. (Stanford Encyclopedia of Philosophy) #Logic
Simulate physics on generalized coordinate systems using Hamiltonian Mechanics and automatic differentiation. #Haskell #Physics
Optics in Isabelle. ~ S. Foster & F. Zeyda #ITP #IsabelleHOL
Imperative Haskell. ~ Vaibhav Sagar #Haskell
End-to-end differentiable proving. ~ T. Rocktäschel & S. Riedel
Gröbner bases in Haskell: Part I. ~ Oleksandr Manzyuk #Haskell
Gröbner bases in Haskell: Part II. ~ Oleksandr Manzyuk #Haskell
Flow networks and the min-cut-max-flow theorem in Isabelle/HOL. ~ P. Lammich & S. Reza Sefidgar #IsabelleHOL
Haskell for numerics? ~ Dominic Steinitz #Haskell
Can’t see the four-est for the trees. ~ Peter Seibel #Haskell #Math
Bézier curves in Haskell. ~ Harold Cooper #Haskell #Gloss #Math
Automatic differentiation using constraint handling rules in Prolog. ~ S. Abdallah #Prolog #CHR #Math
Compiling to categories (extended version). ~ Conal Elliott #Haskell
A simple Haskell implementation of the algebra of pictures outlined in Peter Henderson’s “Functional Geometry”. ~ Micah Hahn #Haskell
Cosette: an automated prover for checking equivalences of SQL queries. #Coq
Formalization of transform methods using HOL Light. ~ A. Rashid & O. Hasan #ITP #HOL_Light
The MINERVA software development process. ~ A. Narkawicz, C.A. Muñoz & A.M. Dutle #PVS #Formal_verification
Constraint Handling Rules. ~ T. Frühwirth #Book #CHR
Augmented Backus-Naur Form (ABNF) in ACL2. ~ A. Coglio #ITP #ACL2
Formal reasoning about programs. ~ A. Chlipala #Coq
Incompleteness and computability (an open logic text). ~ R. Zach #Logic
Buffon’s needle problem in Isabelle/HOL. ~ M. Eberl #IsabelleHOL
Word vs Int. ~ R. Cheplyaka #Haskell
Pyfi : PYthon Function Interface for Haskell. ~ Russell Stewart #Python #Haskell
eBooks gratuitos de la NASA sobre historia, ciencia, aeronáutica e investigación. #Libros #Ciencia
Verified perceptron convergence theorem. ~ C. Murphy, P. Gray & G. Stewart #ITP #Coq
A relaxation technique. ~ Dan Piponi #Haskell
El arte de Escher recreado matemáticamente mediante programación y geometría. ~ @Alvy #Programación
Programming with Escher. ~ Massimo Santini #Python
Haskell and the Curry-Howard isomorphism (Part 1). ~ Ben Sherman #Haskell #Logic
A tutorial on hybrid Answer Set Solving with clingo. ~ R. Kaminski, T. Schaub & P. Wanko #ASP #clingo #Python
An introduction to the Prolog programming language. ~ J.L. Watkin #Prolog
An introduction to the CLIPS programming language. ~ J.L. Watkin #CLIPS
Automated cryptographic analysis of the Pedersen commitment scheme. ~ R. Metere & C. Dong #ITP #Coq
The Typeclassopedia is now up-to-date. ~ Brent Yorgey #Haskell
Intro to functional programming with Haskell. ~ Quinn Wilson #Haskell
All Liouville numbers are transcendental in Mizar. ~ A. Korniłowicz, A. Naumowicz & A. Grabowski #ITP #Mizar #Math
A verified algorithm enumerating event structures in Isabelle/HOL. ~ J. Bowles & M.B. Caminati #ITP #IsabelleHOL
Verified correctness and security of mbedTLS HMAC-DRBG. K.Q. Ye et als. #ITP #Coq
Teaching Haskell for understanding. ~ J. Moronuki #Haskell
Translating a C++ parser to Haskell. ~ G. Gonzalez #Haskell
Lazy interactions – back to the future. ~ Simon Thompson #Haskell
Small minimal examples of modern cryptographic techniques in Haskell. ~ Stephen Diehl #Haskell
Data structures are antithetical to functional programming. ~ John A De Goes #Haskell
Problem solving might attract women to computer science. #CompSci
One practical application of functional programming. ~ J.D. Cook #FuncionalProgramming
A framework for validating session protocols. ~ K.S. Tse & P.C. Johnson #Haskell
Categoricity results for second-order ZF in dependent type theory. ~ D. Kirst & G. Smolka #ITP #Coq
A formally verified proof of the Central Limit Theorem in Isabelle/HOL. ~ J. Avigad, J, Hölzl & L. Serafin #ITP #IsabelleHOL #Math
A single-page quick reference for the markup used in GHC’s Haddock documentation format. ~ G.D. Ritter #Haskell
servant: a type-level web DSL. #Haskell
Partial semigroups and convolution algebras. ~ B. Dongol et als. #IsabelleHOL
Hedgehog: a modern property-based testing system, in the spirit of QuickCheck. ~ Jacob Stanley #Haskell
10 things Idris improved over Haskell. ~ DeQue #Haskell #Idris
Un problema que vale un millón de dólares. ~ Miguel Ángel Morales #Matemáticas
Efficient, verified checking of propositional proofs. ~ M Heule, W Hunt Jr, M Kaufmann, N Wetzler #ITP #ACL2 #SAT
Deep learning: The future of AI. ~ Damian Borth #AI
Reading for programmers. ~ Piotr Limanowski #Emacs #OrgMode
How to read papers efficiently. ~ Irreal #Emacs #OrgMode
La gran novela de las matemáticas.
A beginner’s look at lambda calculus. ~ Prateek Joshi #Logic #CompSci
Backtracking with cut via a distributive law and left-zero monoids. ~ M. Piróg & S. Staton #Haskell
Speculate: discovering conditional equations and inequalities about Haskell functions. ~ R. Braquehais & C. Runciman #Haskell
Introduction to property-based testing (with LeanCheck). ~ Rudy Matela #Haskell
BackProp: Heterogeneous, type-safe automatic backpropagation in Haskell. ~ Justin Le #Haskell
Practical dependent types: type-safe neural networks. ~ Justin Le #Haskell
Some random thoughts of an advanced haskeller. ~ Russell O’Connor #Haskell
Why do monads matter? ~ C. Smith #Haskell
Test automáticos con QuickCheck ¿Cómo analizar nuestro código en busca de bugs? ~ Jose Juan #Programación #QuickCheck
Drive-by Haskell contributions. ~ Neil Mitchell #Haskell
Peut-on faire des Mathématiques avec un ordinateur? ~ René David #Math #Logic #CompSci
Peut-on avoir confiance en l’informatique? ~ René David et Christophe Raffalli #CompSci
A set theory formalization in Agda. ~ A. Calle #ITP #Agda #Math #Logic
Subtyping: overview and implementation. ~ C. Jingwen #Haskell
Dhall is now a template engine. ~ G. Gonzalez #Haskell
Estimating the maximum element of a large list. ~ A. Kaygun #Algorithm #Lisp
Generic unification. ~ R. Cheplyaka #Haskell
A Coq-based synthesis of Scala programs which are correct-by-construction. ~ Y. El Bakouny, T. Crolard, D. Mezher #Coq #Scala
kinder-functor: An alternate definition of Haskell’s Functor typeclass. #Haskell
How well does it work? Profiling in Haskell. ~ James Bowen #Haskell
El futuro de la inteligencia artificial. ~ Geoffrey Hinton #IA
Understanding ResourceT. ~ M. Snoyman #Haskell
Programación. ¿Ciencia o Ingeniería? ~ Chema Cortés #Programación
On competing with C using Haskell. ~ Two Wrongs #Haskell
The Haskell learning curve. #Haskell #Humor
Generating random regular graphs. ~ Atabey Kaygun #Common_Lisp #Math
Calculating the diameter and the radius of a graph using tropic linear algebra. ~ Atabey Kaygun #Common_Lisp #Math
Large-scale formal proof for the working mathematician (ALEXANDRIA). ~ L.C. Paulson #ITP #Math
Course: Functional data structures. ~ P. Lammich & T. Nipkow #FunctionalProgramming #IsabelleHOL #Algorithms
brick: A declarative terminal UI programming library written in Haskell. ~ Jonathan Daugherty #Haskell
Love, monoids, and linguistic determinism. ~ J. Moronuki #Haskell
Propositional proof systems in Isabelle/HOL. ~ J. Michaelis & T. Nipkow #IsabelleHOL #Logic
Interfaces and typeclasses: Number APIs in C# and Haskell. ~ Marcelo Zabani #Haskell
Haskell Weekly 60: News from the Haskell community (June 22 2017). #Haskell
Configurable data types. ~ Francesco Mazzoli #Haskell
The linearity monad. ~ J. Paykin & S. Zdancewic #Haskell
A terminal interface for Tetris. #Haskell
Formalizing push-relabel algorithms for computing the maximum flow in a network. ~ P. Lammich & S.R. Sefidgar #IsabelleHOL
Just enough R: Learn data analysis with R in a day. ~ S. Raman #eBook #RStats
A formal proof of the Kepler conjecture. Thomas Hales et als. #ITP #IsabelleHOL #HOL_Light #Math
Haxl: Making concurrency unreasonably easy. ~ Simon Marlow #Haskell #Haxl
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. ~ S. Bernard et als. #Coq
Noether: Highly polymorphic algebraic structures with custom deriving strategies. ~ Soham Chowdhury #Haskell #Math
Hay que empezar a enseñar historia de la programación. ~ Jordi Cabot
Set theory: from Cantor to Cohen. ~ A. Kanamori #Logic
The Air Force and IBM are building an AI supercomputer. ~ A. Tarantola
Lisp as the Maxwell’s equations of software. ~ M. Nielsen #Lisp #CompSci
Applied category theory. ~ J.D. Cook
Free delivery (functional pearl). ~ J. Gibbons #Haskell
How to twist pointers without breaking them. ~ S. Chauhan, P.P. Kurur & B.A. Yorgey #Haskell
Verified functional algorithms. ~ A.W. Appel #Coq #Algorithms
Five stages of accepting constructive mathematics. ~ A. Bauer #Math #Logic
Matemáticas en Emacs. ~ M. Román #Emacs
Matemáticas vs. física o viceversa (y quizá no tan «versus»). ~@Alvy
Ten signs a claimed mathematical breakthrough is wrong. ~ Scott Aaronson #Math
(Dicen que) han demostrado la conjetura de Goldbach. Otra vez. ~ A. Córdoba #Matemáticas
Geometry, topology and physics. ~ M. Nakahara #Math
Algebraic graphs with class (Functional pearl). ~ A. Mokhov #Haskell
A minimalistic, elegant and powerful approach to working with graphs in Haskell. ~ A. Mokhov #Haskell
The theory of algebraic graphs formalised in Agda. ~ A. Mokhov #Agda
The Common Lisp cookbook #eBook #CommonLisp
Lists and why they are useful - M. V. Wilkes #Lisp

Julio 2017

Developing bug-free machine learning systems with formal mathematics. ~ D. Selsam, P. Liang, D.L. Dill #LeanTP
Functional programming for deep learning. ~ Joyce Xu #FuncionalProgramming #DeepLearning
Haskell on Android and iOS. ~ Keera Studios #Haskell
Maxima & GnuPlot (Logiciel de calcul formel & logiciel de tracé de courbes). ~ T. Castanet #Maxima #GnuPlot #Math
Utiliser Maxima pour préparer le travail en classe. ~ T. Castanet #Maxima #GnuPlot #Math
An overview of the PureScript type system. ~ Phil Freeman #PureScript #Haskell
Idris dependent typing challenge: Bowling Kata. ~ Quentin Duval #Haskell #Idris
Tutorial on Ivy, Counsel, and Swiper. ~ Irreal #Emacs
Notes on fusion. ~ Tim Humphries #Haskell
Continuations, all the way down. ~ Tim Humphries #Haskell
Generating mazes with inductive graphs. ~ T. Jelvis #Haskell
Probability monad. ~ T. Jelvis #Haskell
Typesafe modular arithmetic in Haskell. ~ R. Muthukrishnan #Haskell
Automatic functional correctness proofs for functional search trees. ~ T. Nipkow #IsabelleHOL #Algorithms
SAT-MICRO: petit mais costaud! ~ S. Conchon, J. Kanig, S. Lescuyer #Logic #OCaml
Haskell implementation of the minimal OCaml solver described in the paper “SAT-MICRO: petit mais costaud!” ~ D. Bueno #Logic #Haskell
Advanced Python features. #Python
OPLSS2017: The Oregon Programming Languages Summer School. [Videos] #Programming
A minimax AI for deterministic games, in 47 lines of Haskell. #Haskell #AI #Games
Notes and files from HaskellerZ meetups. #Haskell
Can ILP be applied to large dataset? ~ H. Watanabe, S. Muggleton #ILP #BigData
Functional programming and proving in Isabelle/HOL. ~ Andreas Lochbihler [Video] #IsabelleHOL
Graphing it Out. ~ James Bowen #Haskell #FGL
De monos, melanesios y desarrollo de software. ~ Juan María Hernández
The implementation of functional programming languages. ~ Simon Peyton Jones #eBook
Functional baby talk: Analysis of code fragments from novice Haskell programmers. ~ J. Singer, B. Archibald #Haskell
Vector programming using structural recursion (an introduction to vectors for beginners). ~ M.T. Morazán #Racket
Using Elm to introduce algebraic thinking to K-8 students. ~ C. d’Alves et als. #Elm
Overcoming non distributivity: A case study in functional programming. ~ J.C. Saenz, M. Stannett #Haskell
Teaching Functional Programming should start earlier! ~ J. Sharrad #Teaching #Haskell
Crafting certified elliptic curve cryptography implementations in Coq. ~ A. Erbsen #MsC_Thesis #Coq #Math
Kaprekar sequence. ~ Atabey Kaygun #Common_Lisp #Math
Lattice of Dyck Words. ~ Atabey Kaygun #Common_Lisp #Math
Logic programming for an introductory computer science course for high school students. ~ T. Yuen, M. Reyes, Y. Zhang #Teaching #Logic_Programming
Haskell, WhatsApp and romance. ~ Akshay Zade #Haskell
Formalisation of ground inference systems in a proof assistant. ~ M. Fleury #Msc_Thesis #IsabelleHOL #Logic
Industrial use of a mechanical theorem prover. ~ JS. Moore #ATP #ITP #ACL2
The Big Proof agenda for mechanizing mathematical discourse. ~ N. Shankar #Logic #Math #ITP
Generic approach to certified static checking of module-like constructs. ~ J. Belyakova #Coq
The resurgence of functional programming. ~ Wesharethis #Haskell #Erlang #Elixir #Scala #Clojure #Fsharp
Verifying a simple compiler using property-based random testing. ~ P. Vasconcelos Code #Haskell
A formalized general theory of syntax with bindings. ~ L. Gheri, A. Popescu #IsabelleHOL
The Lean theorem prover. ~ Jeremy Avigad #ITP #LeanTP #Math #Logic
Validating the meta-theory of programming languages. ~ G. Fachini, A. Momigliano #Haskell
Introducing Vaultenv: Keeping your secrets secure with Vault and Haskell. ~ L. Duijvesteijn #Haskell
El perfil de un data scientist. ~ Jordi Casas #DataScience
How do we use (typed) functional programming to minimize our flaws. ~ Steven Vandevelde #Haskell #Elm
Continuations from the ground up. ~ Isaac Elliott #Haskell
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes. ~ V.B.F. Gomes et als. #IsabelleHOL #AFP
Some Hasse diagrams. ~ @Atabey_Kaygun #CommonLisp #Math
Efficient verified (UN)SAT certificate checking. ~ P. Lammich #IsabelleHOL #Logic #SAT
An Oxford University artificial intelligence startup has raised £17 million to check code for errors. ~ Shona Ghosh
DiffBlue: a world leader in AI that understands code.
An Emacs tutorial series. ~ Irreal #Emacs
Towards a formal verification of Courcelle’s theorem. ~ E. Black #ITP #Agda
Prácticas de la asignatura “Criptografía y computación” ~ Marta Gómez #Haskell
RustBelt: Securing the foundations of the Rust programming language. ~ R. Jung et als. #Rust #Coq
Iterators and streams in Rust and Haskell. ~ M. Snoyman #Rust #Haskell
A tale of two provers (Verifying monoidal string matching in Liquid Haskell and Coq). ~ Niki Vazou #Haskell #Coq
Trace and stable failures semantics for CSP-Agda. ~ B. Igried & A: Setzer #Agda
Curso básico de Haskell en español. #Haskell
Instalación de Haskell-Platform. ~ Rayskell Vídeo #Haskell
Introducción y primeros pasos con Haskell. ~ Rayskell #Haskell
El cálculo lambda. ~ Rayskell #Haskell
Tipos y clases de tipos. ~ Rayskell #Haskell
Regresión lineal con Haskell. ~ Rayskell Vídeo #Haskell
What are some useful, but little-known, features of the tools used in professional mathematics? ~ Terence Tao #Math
Typesetting flow graphs with Tikz. ~ Greg Restall #LaTeX
A case-study in programming coinductive proofs: Howe’s method. ~ D. Thibodeau, A. Momigliano & B. Pientka #ITP #Beluga
Playing match maker. ~ James Bowen #Haskell
¿Por qué triunfa Sci-hub si es el mayor repositorio pirata de ciencia a nivel mundial? ~ Lydia Gil
Isabelle/HOL demo. ~ Sebastian Neubauer #IsabelleHOL
Local refinement typing. ~ B. Cosman, R. Jhala #Haskell #Verification #SMT #LiquidHaskell
AIMS Desktop: distro GNU/Linux para matemáticos. ~ MiradaDelReplicante #Linux #Matemáticas
Using the Coq theorem prover to verify complex data structure invariants. ~ K. Roe & S. Smith #ITP #Coq
Encoding objects. ~ F. Kinoshita #Haskell
Modelling the way mathematics is actually done. ~ J. Corneli & R. Puzio #AI #Math #MKM
sparse-linear-algebra: Numerical computation in native Haskell. ~ Marco Zocca #Haskell #Math
Use Hpack - e.xtendo.org #Haskell
Ordonner les ordres : un treillis sur les ordres partiels. ~ V. Pons
Cheatsheet: Rank 2 types with typeclasses. ~ Jeremy Mikkola #Haskell
Course: Mathematical logic and programming languages. ~ T. Sheard #Logic #Haskell
Logic via foundational algorithms. ~ J. Hook & T. Sheard #eBook #Logic #Haskell
Notes on the Finite Set module. ~ J. Hook & T. Sheard #Haskell #Logic
Course: Mathematical logic via foundational algorithms. ~ J. Hook & T. Sheard #Logic #Haskell
Formalization of the fundamental group in untyped set theory using auto2. ~ B. Zhan #ITP #IsabelleHOL #Logic #Math
The algebra (and calculus!) of algebraic data types. ~ J. Burget #Haskell
Haskell tutorials, a tutorial. ~ Yann Esposito #Haskell
Using doctest-discover with Stack. ~ Richard Cook #Haskell
Formalization of a large part of Haskell’s standard prelude in Isabelle/HOLCF. ~ J. Breitner et als. #IsabelleHOL #Haskell
VisPar: Visualising dataflow graphs from the Par monad. ~ M. Algehed & P. Jansson #Haskell
Verified metatheory and type inference for a name-carrying simply-typed lambda calculus. ~ M. Rawson #ITP #IsabelleHOL
Demystifying Haskell assignment. ~ G. Gonzalez #Haskell
The language(s) of first-order logic #1. ~ Peter Smith #Logic
Self-referential logic via self-referential circuits. ~ Dan Piponi
NASA PVS Library of Formal Developments. #PVS
Monad transformers step by step. ~ M. Grabmüller #Haskell
Minkowski’s theorem in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL #Math
Cleaning up our projects with Hpack! ~ James Bowen #Haskell
Biased algorithms are everywhere, and no one seems to care. ~ Will Knight
Further formalization of the process algebra CCS in HOL4. ~ Chun Tian #ITP #HOL4
R and Haskell: best of both worlds with HaskellR. ~ Sigrid Keydana #Haskell #RStats #HaskellIR
Tamarin prover: a powerful tool for the symbolic modeling and analysis of security protocols. #Haskell #Tamarin
Formal verification of the WireGuard protocol. ~ J.A. Donenfeld & K. Milner #Haskell #Tamarin #Formal_verification
Using Coq to write fast and correct Haskell. ~ J. Wiegley & B. Delaware #Haskell #Coq
Pascal’s triangle in Haskell and JavaScript: or, more fun with recursion! ~ T. Cothran #Haskell #JavaScript
Verifying strong eventual consistency in distributed systems. ~ V.B.F. Gomes et als. #ITP #IsabelleHOL
Categories and Haskell (An introduction to the mathematics behind modern functional programming). ~ Jan-Willem Buurlage #Haskell #Math
Formalizing Cartan geometry in modal homotopy type theory. ~ F. Wellen #ITP #Agda #Math #HoTT
A formalization of convex polyhedra based on the simplex method. ~ X. Allamigeon & R.D. Katz #ITP #Coq #Math
Get started with sending SMS in Haskell. ~ Lizzie Siegle #Haskell
State machine testing with Hedgehog. ~ Tim Humphries #Haskell
Simple exercises in Haskell, using HSpec. ~ Attila Domokos #Haskell
Compiling GHC with Stack for Stack. ~ Vincent Hanquez #Haskell
Functional programming Babelfish. ~ Håkon Rossebø #Purescript #Haskell #Elm #Fsharp
Industrial use of ACL2: applications, achievements, challenges, and directions. ~ J S. Moore & M.J.H. Heule #ACL2
Mikrokosmos: an untyped lambda calculus interpreter. ~ Mario Román #Haskell #Logic
A formal proof in Coq of LaSalle’s invariance principle. ~ C. Cohen & D. Rouhling (Code) #ITP #Coq
Simple verification of Rust programs via functional purification. ~ S. Ullrich #ITP #LeanTP #Rust
Course: Automated reasoning (2016-17). ~ J. Fleuriot #AR #Logic #ITP #IsabelleHOL
How to believe a machine-checked proof. ~ R. Pollack (1997). #ATP #ITP
Logitext: an educational proof assistant for first-order classical logic using the sequent calculus. #Logic #Coq #Haskell
What happens when you mix three research programming languages together. ~ E.Z. Yang #Coq #Haskell
Equivalences for free! (Univalent parametricity for effective transport). ~ N. Tabareau et als. #ITP #Coq
Simplicitly (Foundations and applications of implicit function types). ~ M. Odersky et als. #Scala
The RIO monad. ~ M. Snoyman #Haskell
New fast.ai course: Computational linear algebra. ~ Rachel Thomas #Python #Math
Steenrod-Milnor and tournament sequences. ~ @Atabey_Kaygun #CommonLisp #Math
Declarative semantics for functional languages in Isabelle/HOL. ~ Jeremy Siek #IsabelleHOL
Declarative semantics for functional languages: compositional, extensional, and elementary. ~ Jeremy G. Siek
Course: The formal verification of compilers. ~ Xavier Leroy #Coq #DSSS17
Boolean logic in polynomials. ~ Jeremy Kun | Math ∩ Programming #Logic #Math
A verified certificate checker for floating-point error bounds. ~ H Becker, E Darulova, MO Myreen #ITP #Coq #HOL4
Vellvm: Verifying the LLVM. ~ Steve Zdancewic #Coq #DSSS17
List of companies that use Haskell. #Haskell
Hacker-proof coding. ~ Esther Shein | Communications of the ACM
Data science: challenges and directions. ~ Longbing Cao | Communications of the ACM #DataScience
«La ciencia nunca se pensó para el mercado, pero hoy es una mercancía» ~ Andrea Saltelli
A proof strategy language and proof script generation for Isabelle/HOL. ~ Y. Nagashima, R. Kumar #IsabelleHOL
Existential types in Haskell. ~ Roger Qiu #Haskell
Course: Program synthesis for everyone. ~ R. Bodik, E. Torlak
Cantor, el Aleph y los distintos infinitos. ~ M.A. Morales | El Aleph #Matemáticas
DeepSpec Summer School videos. #DSSS17 #Coq
Lecture material for DeepSpec Summer School 2017. #DSSS17 #Coq
Toward certification for free!: correct-by-construction ML oracles with polymorphic LCF style. ~ S. Boulmé, A. Maréchal #Coq
Formalizing abstract computability: Turing categories in Coq. ~ P. Vinogradova #PhD_Thesis #Coq
Formal proof of the Lindemann-Weierstrass theorem. ~ S. Bernard. #Coq #Math
Formalizing basic quaternionic analysis. ~ A. Gabrielli, M. Maggesi #HOL_Light #Math
Streaming programs without lazyness: a short primer. ~ F. Domínguez & M. Boespflug #Haskell
Logic Explorer: interactive proof assistant for sequent calculi. ~ Ben Selfridge #Haskell #Logic
Proof checker for propositional logic. ~ Ben Selfridge #Haskell #Logic
Lens tutorial - SimpleLens. ~ mchaver #Haskell
Effect polymorphism in higher-order logic (proof pearl). ~ A. Lochbihler #IsabelleHOL
GHC warnings you should use in addition to -Wall. ~ Dennis Gosnell #Haskell
How is coinduction the dual of induction? ~ J. Breitner #Haskell
Port of Software Foundations to Agda. ~ Wen Kokke & Philip Wadler #Agda
Coinduction in Coq and Isabelle. ~ J. Breitner #Coq #IsabelleHOL
Formalization of the functional pearl “Enumerating the rationals” by Gibbons, Lester and Bird in Coq. ~ Wen Kokke #Coq #Math
Intermediate abstraction. ~ Reid McKenzie #Programming #Clojure
Homotopy Type Theory in Lean. ~ U. Buchholtz, F. van Doorn, J. von Raumer #HoTT #LeanTP
Qwire practice: Formal verification of quantum circuits in Coq. ~ R. Rand, J. Paykin, S. Zdancewic #Coq
Faster command line tools with Haskell. ~ Cody Goodman #Haskell
La demostración matemática más larga. ~ F.R. Villatoro #Matemáticas #Computación
To Void or to void. ~ M. Snoyman #Haskell
The riddle of the number chain. ~ Michael Lugo #Math
DeepSpec Summer School 2017: a summary. ~ Jan Stolarek #Formal_verification #DSSS17

Agosto 2017

Dynamic architectures in Isabelle/HOL. ~ Diego Marmsoler #IsabelleHOL #AFP
July 2017 1HaskellADay problems and solutions. ~ @geophf | Typed Logic #Haskell #Haskell #1HaskellADay
200 terabyte proof demonstrates the potential of brute-force math. ~ M. Byrne #Math #CompSci
Table-of-contents sidebar for Emacs. ~ Austin Bingham #Emacs
Stewart’s theorem and Apollonius’ theorem in Isabelle/HOL. ~ Lukas Bulwahn #IsabelleHOL #Math #AFP
Owl: A general-purpose numerical library in OCaml. ~ L. Wang #OCaml #Math
The DeepSpec Summer School on Verified Systems (Schedule). #DSSS17 #Coq
A vision for automated deduction rooted in the connection method. ~ Wolfgang Bibel #ATP
A library for competitive programming in Haskell. #Haskell
Transitive closure of a directed graph or a relation. ~ @Atabey_Kaygun #CommonLisp #Clojure #Math
Thinking functionally with Haskell: A deep dive into the functional pool. ~ Paul Callaghan #Haskell
A formally verified proof of Kruskal’s tree theorem in Lean. ~ M. Wu #MsC_Thesis #ITP #LeanTP
Thinking functionally with Haskell: Types? tests? We need a new word. ~ Paul Callaghan #Haskell
Logic and proof. ~ J. Avigad, R.Y. Lewis, F. van Doorn #Logic #ITP #LeanTP
Computer-assisted proof. ~ Wikipedia #Math #CompSci
Mathematics in the age of the Turing machine: a survey of mathematical proofs that rely on computer calculations and formal proofs. ~ T. Hales
Formal methods in mathematics and the Lean theorem prover. ~ J. Avigad #Logic #Math #ITP #LeanTP
Appropriate steps (A theory of motivated proofs). ~ R. Morris #PhD_Thesis #Math #Logic
Counting zeros over finite fields using Gröbner bases. ~ S. Gao #MS_Thesis #Math
Org mode syntax reference card. ~ Fabrice Niessen #Emacs
wish: A trivial web browser written in Haskell. ~ Chris Done #Haskell
Implementación de un algoritmo de búsqueda aleatoria en programación lógica. ~ I. Blázquez #TFG #Prolog
Property-based testing via proof reconstruction: work-in-progress. ~ R Blanco, D Miller, A Momigliano #Prolog
The science of brute force (Mathematics solves problems by pen and paper. CS helps us to go far beyond that) ~ MJH Heule, O. Kullmann
Lógica de primer orden en Haskell. ~ E. Paluzo #TFG #Haskell #Lógica
Matemática discreta en Haskell. ~ M.D. Valverde #TFG #Haskell #Matemáticas
Formalización de cáculos lógicos en Isabelle/HOL. ~ M.D. Mateo #TFM #IsabelleHOL #Lógica
Formalising monotone frameworks: a dependently typed implementation in Agda. ~ J.J. van Wijk #MSc_Thesis #Agda
Finding functional pearls: Detecting recursion schemes in Haskell functions via anti-unification. ~ AD Barwell, C Brown, K Hammond #Haskell
Lazy rebuilding. ~ G. Kunigami #OCaml
A simple, concise implementation of Huet’s algorithm in Haskell. ~ Danny Gratzer #Haskell
Free: You can now read classic books by MIT Press on archive.org.
A metaprogramming framework for formal verification. ~ G. Ebner et als. #LeanTP
Thinking functionally with Haskell: Playing with Haskell. ~ Paul Callaghan #Haskell
Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. ~ A. Rizaldi et als. #IsabelleHOL
Ode on a random urn (Functional pearl). ~ L Lampropoulos, A Spector-Zabusky, K Foner #Haskell
The future is functional: Haskell and the AI-native. ~ James Bowen. #Haskell #AI
Robust computer algebra, theorem proving, and oracle AI. ~ G.P. Sarma, N.J. Hay #ATP #CAS #AI
Thinking functionally with Haskell: Is there anything left to say about monads? ~ Paul Callaghan #Haskell #Haskell
Mechanizing linear logic in Coq. ~ B. Xavier et als. #ITP #Coq #Logic
Declarative statistics. ~ R. Rossi et als. #Constraint_programming #Statistics
Unified media programming: an algebraic approach. ~ S. Archipoff & D. Janin #Haskell
Functional baby talk: analysis of code fragments from novice Haskell programmers. ~ J Singer, B Archibald #Haskell
Overcoming non distributivity: a case study in functional programming. ~ J.C. Saenz, M. Stannett #Haskell
Vector programming using structural recursion (an introduction to vectors for beginners). ~ M.T. Morazán #Racket
Using Elm to introduce algebraic thinking to K-8 students. ~ C. d’Alves et als. #Elm
QueryArrow: semantically unified query and update of heterogeneous data stores. ~ Hao Xu et als. #Haskell
QueryArrow: A semantically unified SQL and NoSQL query and update system. ~ Hao Xu #Haskell
Why you should use PureScript. ~ Phil Freeman #PureScript
Functional programming for & fun profit (or: how I learned to stop worrying and love shipping Haskell code). ~ D. Gasienica #Haskell
Program design by calculation (DRAFT / Last update: April 2017). ~ J.N. Oliveira #eBook #Haskell
Array programming in Haskell. ~ Manuel Chakravarty | Tweag I/O #Haskell
Writing performant Haskell (1 of 6): Intro. ~ Jason Shipman #Haskell
How can humans keep control of AI? #AI #DeepLearning
Using a set constraint solver for program verification. ~ M. Cristiá, G. Rossi & C. Frydman #ConstraintProgramming
Writing performant Haskell (2 of 6): Strings. ~ Jason Shipman #Haskell
Magit tutorial - Rebase (Part I). ~ Guowei Lv #Emacs
Magit tutorial - Rebase (Part II). ~ Guowei Lv #Emacs
Functional programming cheat sheet. ~ Tony Morris #Haskell
Reasoning with representable functors. ~ Adelbert Chang #Haskell
A computational logic approach to human syllogistic reasoning. ~ A.O. da Costa et als. #Logic
Writing performant Haskell (3 of 6): SPECIALIZE. ~ Jason Shipman #Haskell
Declarative algorithms for term generation, counting. ~ P. Tarau #Prolog
El modelo M4 de la máquina Enigma. ~ M. García #Haskell
Implementation of Enigma versions in Haskell. ~ M. García #Haskell
Experimental implementation of Cubical Type Theory. ~ Anders Mörtberg #Haskell
tdiff: Simply print the time difference between lines from stdin. ~ Chris Done #Haskell
Writing performant Haskell (4 of 6): builder revisited. ~ Jason Shipman #Haskell
agsyHOL: a theorem prover for higher-order logic. ~ Fredrik Lindblad #Haskell #Logic
How to read a book: 3 strategies & questions for critical reading. ~ Terry Heick
Announcing Hasky Stack. ~ Mark Karpov #Haskell #Emacs
Magit tutorial: Bisect. ~ Guowei Lv #Emacs
Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. ~ W Li, GO Passmore, LC Paulson #IsabelleHOL
Deriving law-abiding instances. ~ R. Scott et als. #Haskell #LiquidHaskell
On the quest for an acyclic graph. ~ M Janota, R Grigore, V Manquinho #SAT #Logic
Mathematics as a creative art. ~ Paul Halmos #Math
Static analysis of programs using semirings. ~ L. North #Haskell
Writing performant Haskell (5 of 6): dive into text. ~ Jason Shipman #Haskell
Starting out with Haskell Tensor Flow. ~ James Bowen. #Haskell #TensorFlow
An introduction to quantum computing, without the physics. ~ G. Nannicini #QuantumComputing
apecs: a fast, type driven, extensible ECS (Entity Component System) in pure Haskell. ~ Jonas Carpay #Haskell
Effect polymorphism in higher-order logic (Proof Pearl). ~ A. Lochbihler #IsabelleHOL
A foray into number theory with Haskell. ~ Fred Akalin #Haskell #Math
Challenges in the verification of reinforcement learning algorithms. ~ P. van Wesel, A.E. Goodloe #FormalVerification #ML
Proof editor for natural deduction in first-order logic. ~ E. Björnsson et als. #Logic #Teaching
Hacia la formalización del razonamiento ecuacional sobre mónadas. ~ E. Lobo #Agda
From sets to bits in Coq. ~ A. Blot, P.É. Dagand & J. Lawall #Coq
Problem sets for MIT 6.887 “Formal reasoning about programs”, Spring 2017. #Coq
Coq math problems (interesting, challenging, or fun math problems formalized in Coq). #Coq #Math
Exercises on generalizing the induction hypothesis. ~ James Wilcox #Coq
Making automatic theorem provers more versatile. ~ S. Cruanes #ATP
Writing a ZX Spectrum game in Haskell (introducing the z80 and zxspectrum packages). ~ Daniel P. Wright #Haskell
El lenguaje de la naturaleza. ~ A. Cordoba #Matemáticas
Proof assistants as smart programming languages. ~ A. Popescu #Programming #IsabelleHOL
Adaptive lock-free data structures in Haskell: a general method for concurrent implementation swapping. ~ C.H. Chen et als. #Haskell
Science fiction at the far side of technology: Vernor Vinge’s singularity thesis versus the limits of AI-research. ~ M.W. Johansen #AI #ATP
24 challenges in deductive software verification. ~ R. Hähnle & M. Huisman #Verification
Towards strong higher-order automation for fast interactive verification. ~ J.C. Blanchette #ATP
Duet: an educational dialect of Haskell aimed at interactivity. ~ Chris Done #Haskell
La IA que se explica: «Esto es un gato porque tiene pelo, bigotes, garras y orejas de gato como estas» ~ @Alvy #IA
What does the “we don’t understand how artificial intelligence takes decisions” statement mean? ~ Julián Estévez #AI #DeepLearning #CompSci
Inside Darpa’s push to make artificial intelligence explain itself. ~ S. Castellanos & S. Norton #AI
OrgStat: Statistics visualizer for org-mode. ~ Mikhail Volkhov #Haskell #Emacs #OrgMode
Backpack for deep learning. ~ Kaixi Ruan #Haskell #DeepLearning
Automated reasoning for explainable artificial intelligence. ~ M.P. Bonacina #ATP #AI
Yampa: Domain-specific language embedded in Haskell for programming hybrid (mixed discrete-time and continuous-time) systems. ~ Ivan Perez #Haskell
Back to the future: time travel in FRP. ~ Ivan Perez #Haskell #FRP
Cryptographic protocols specification and verification tools: a survey. ~ A.H. Shinde, A.J. Umbarkar & N.R. Pillai #Haskell #Isabelle #Coq
Generalized graph pattern matching. ~ P. Almagro & F. Sancho
Theorem provers as a learning tool in theory of computation. ~ M. Knobelsdorf et als. #ITP #Coq #Learning
The three gap theorem (Steinhauss conjecture). ~ M. Mayero #Coq #Math
GRAT: Efficient formally verified SAT solver certification toolchain. ~ P. Lammich #SAT #IsabelleHOL
Discrete mathematics. ~ M. Fiore #Math
SC2 challenges: when Satisfiability Checking and Symbolic Computation join forces. ~ E. Ábrahám et als. #ATP
Understanding asymmetric numeral systems. ~ Roman Cheplyaka #Haskell #Math
Recognizing when two arithmetic expressions are essentially the same. ~ Mark Dominus #Math #Puzzle
MGL: Common Lisp machine learning library. ~ Gábor Melis #CommonLisp #ML
The most beautiful program ever written: a Lisp interpreter written in Lisp. ~ Guowei Lv #Lisp
Information effects. ~ R.P. James & A. Sabry #Haskell
Review: Information effects. #Haskell #ReversibleComputing
Nix and Haskell in production. ~ G. Gonzalez #Haskell #Nix
Haskell merkle trees. #Haskell
Ser matemático es la profesión del futuro. ~ Cedric Villani #Matemáticas
The potential of interference-based proof systems. ~ M.J.H. Heule & B. Kiesl #ATP
Digging in deep: solving a real problem with Haskell Tensor Flow. ~ James Bowen. #Haskell #TensorFlow
Pirámides de números primos capicúa. ~ @Wicho #Matemáticas
Palindromic prime pyramids. ~ G.L. Honaker & C.K. Caldwell #Math
Supplement to “Palindromic prime pyramids”. ~ C.K. Caldwell #Math
Functional Pearl: a pretty but not greedy printer. ~ J.P. Bernardy #Haskell
Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results. ~ R. Braquehais & C. Runciman #Haskell
Notions of computation as monoids. ~ E. Rivas & M. Jaskelioff #Haskell
Industrial use of ACL2: applications, achievements, challenges, and directions. ~ JS. Moore & M.J.H. Heule #ACL2
Generic functional parallel algorithms: Scan and FFT. ~ Conal Elliott #Haskell
Universities are broke. So let’s cut the pointless admin and get back to teaching. ~ A. Spicer
Checkable proofs for first-order theorem proving. ~ G. Reger & M. Suda #ATP
A framework for adaptive differential privacy. ~ D. Winograd-Cort, A. Haeberlen, A. Roth & B.C. Pierce #OCaml
Induction for point-free equational reasoning. ~ Ruben Pieters #Haskell #Math
Vigorous public debates in academic computer science. ~ John Regehr #CompSci
A tour of Eta (Learn functional programming the easy way). #Eta #Haskell
Simply safe lattice cryptography. ~ E. Crockett #PhD_Thesis #Haskell #Math #Cryptography
Verified tail bounds for randomized programs. ~ J. Tassarotti & R. Harper #Coq
Faster coroutine pipelines. ~ Mike Spivey #Haskell
Abusing Haskell dependent types to make Redis queues safer. ~ Tebello M. Thejane #Haskell
A concise introduction to logic. ~ Craig DeLancey #eBook #Logic #OpenLibra
The evolution of Lisp. ~ G.L. Steele & R.P. Gabriel #Lisp
How to design programs (second edition). ~ M. Felleisen et als. #eBook #Programming #Scheme
Kami: a platform for high-level parametric hardware specification and its modular verification. ~ J. Choi et als. #Coq
Writing a formally-verified porn browser in Coq and Haskell. ~ Michael Burge #Coq #Haskell
The Ntha programming language. ~ JHZheng #Haskell
Shrink fast correctly! ~ O. Savary Bélanger & A.W. Appel #Coq
Type Tac Toe: advanced type safety. ~ Chris Penner #Haskell #Game
Monad transformer commutativity. ~ Jason Shipman #Haskell
Verified correctness and security of mbedTLS HMAC-DRBG. ~ K.Q. Ye et als. #Coq
Conway’s game of life using representable and comonads. ~ Chris Penner #Haskell
The engine for Haskell IDE-integration. #Haskell
A certified decision procedure for tree shares. ~ X.B. Le et als. #Coq
Putting the flow in Tensor Flow! ~ James Bowen #Haskell #TensorFlow
Radix sort, trie trees, and maps from representable functors. ~ Chris Penner #Haskell
Formalisations using two-level type theory. ~ D. Annenkov, P. Capriotti & N. Kraus #ITP #LeanTP #HoTT
Verification by reduction to functional programs. ~ R.W. Blanc #PhD_Thesis #ITP #Leon #Scala
Verified root-balanced trees. ~ T. Nipkow #ITP #IsabelleHOL #AFP
Certified soundness of simplest known formulation of first-order logic. ~ John Bruntse Larsen #IsabelleHOL #Logic
Free and forgetful functors. ~ Chris Penner #Haskell
Algoritmos para Big Data: Grafos y PageRank. ~ S. Garcı́a #TFG #BigData #Python
The GRAT tool chain: efficient (UN)SAT certificate checking with formal correctness guarantees. ~ P. Lammich #IsabelleHOL #SAT
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. ~ M. Hamana #Haskell
Adjunctions and Battleship. ~ Chris Penner #Haskell
FuncShell: Improve your shell by making it functional through Haskell! (An update to Awkward). ~ Rahul Ramteke #Haskell
Herbarium Racketensis: a stroll through the woods (functional pearl). ~ V. St-Amour et als. #FP #Racket
El gran salto entre creer y demostrar. ~ M.A. Morales | El Aleph #Matemáticas
Learning number theory and Haskell: the division algorithm. ~ Chris Smith #Haskell #Math

Septiembre 2017

Orbit-stabiliser theorem with application to rotational symmetries in Isabelle/HOL. ~ J. Rädle #ITP #IsabelleHOL #Math #AFP
Orbit-stabilizer theorem. ~ Proofwiki #Math
Category theory for programmers. ~ Bartosz Milewski #Haskell #Math
From concurrent programs to simulating sequential programs: correctness of a transformation. ~ A. Blanchard et als. #Coq
Zippers using Representable and Cofree. ~ Chris Penner #Haskell
Computational category theory. ~ D.E. Rydeheard & R.M. Burstall #eBook #FP #SML #Math
Enter the matrix, Haskell style. ~ Manuel Chakravarty | Tweag I/O #FP #Haskell #Math
7 lenguajes que se utilizan en inteligencia artificial. ~ E. Goette #Programación #IA
7 best Artificial Intelligence programming language in 2017. #AI #Programming #Haskell #JavaScript #Prolog #Java #Lisp #Cpp #Python
regex-fsm: Convert regular expressions into layered finite-state machines. ~ David Johnson #Haskell
AlgebraicPrelude: Remaking a basis for Haskell that is well grounded in Group theory. #Haskell #Math
Fixed-length vector types in Haskell (an update for 2017) ~ Justin Le #Haskell
The λμ-calculus in Isabelle/HOL. ~ C. Matache, V.B.F. Gomes & D.P. Mulligan #ITP #IsabelleHOL #Logic #AFP
Constrained type families. ~ J. Garrett Morris & R.A. Eisenberg #Haskell
Let’s make a GTK Video Player with Haskell. ~ David Lettier #Haskell
Hilbert R-tree in Haskell. ~ David Johnson #Haskell
Algebraic principles for program correctness tools in Isabelle/HOL. ~ V.B.F. Gomes #PhD_Thesis #IsabelleHOL
Serokell Haskell style guide. #Haskell
August 2017 1HaskellADay problems and solutions. ~ Douglas M. #Haskell #Haskell #1HaskellADay
SuperRecord: anonymous records for Haskell. ~ Alexander Thiemann #Haskell
Type level merge sort (Haskell). ~ Alexander Thiemann #Haskell
Exploration of primes, factorization and number theory through Haskell. ~ Mamy Ratsimbazafy #Haskell #Math
Explainable Artificial Intelligence (XAI). ~ David Gunning #AI #XAI
A proof strategy language and proof script generation for Isabelle/HOL. ~ Y. Nagashima, R. Kumar #IsabelleHOL
PSL: Proof Strategy Language for Isabelle/HOL. ~ Yutaka Nagashima #IsabelleHOL
Study and implementations of F-Algebras and Bird-Meertens formalism in Haskell. #Haskell #Math
Visualizing graphs in Haskell. ~ Michael Burge #Haskell #Graphviz
IfElse: Anaphoric and miscellaneous useful control-flow. ~ J.R. Heard & W. Thornton #Haskell
¿Qué demonios es el Deep Learning y por qué debería aprenderlo en este artículo? ~ A. Palomo #IA #DeepLearning
DeepL, un traductor superior. ~ @Alvy #IA
Programas, funciones y dibujos con CodeWorld/Haskell. #CodeWorld #Haskell
Roll your own bitcoin exchange in Haskell. Michael Burge #Haskell
Emulating finite state machines, non-deterministic finite state machines, push-down automata, and Turing machines in Haskell. #Haskell
Linear logic programming for narrative generation. ~ C. Martens, A.G. Bosser, J.F. Ferreira & M. Cavazza
Testing and debugging functional reactive programming. ~ I. Perez & H. Nilsson #Haskell
Lock-step simulation is child’s play (experience report). ~ J. Breitner & C. Smith #Haskell #CodeWorld #ICFP2017
Scaling up functional programming education: under the hood of the OCaml MOOC. ~ B. Canou, R. Di Cosmo & G. Henry #OCaml #ICFP2017
Verifying efficient function calls in CakeML. ~ S. Owens et als. #ITP #HOL4 #ICFP2017
Deeper still: convolutional neural networks. ~ James Bowen #Haskell
Cuando el algoritmo se convierte en artista: ¿reemplazará al humano? ~ Jose A. Luna
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation. ~ M. Hamana #Haskell
Kami: a platform for high-level parametric hardware specification and its modular verification. ~ J. Choi et als. #Coq #ICFP2017
SpaceSearch: a library for building and verifying solver-aided tools. ~ K. Weitz et als. #Coq #ICFP2017
Local refinement typing. ~ B. Cosman & R. Jhala #Haskell #SMT #LiquidHaskell #ICFP2017
Compiling to categories. ~ C. Elliott #Haskell #ICFP2017
Q*cert: Q*cert: A query compiler and a platform for implementing and verifying query compilers. #ITP #Coq
Mathematical components. ~ A. Mahboubi & E. Tassi #eBook #ITP #Coq #Math
99 ways to say ‘(I love you). ~ Matt Might #FP #Racket
A formal proof of the Kepler conjecture. ~ S. Kober #ITP #IsabelleHOL #HOL_Light #Math
GALE: A functional graphic adventure library and engine. ~ Ivan Perez #Haskell #Game
Tracking performance over the entire software lifecyle. ~ Nicolas Mattia #Haskell
ICFP / FSCD day 3 – rough notes. ~ Dominic Orchard #icfp2017
Bringing order to the separation logic jungle. ~ Q. Cao, S. Cuellar & A.W. Appel #Coq
Modeling music in Haskell. ~ Sandy Maguire #Haskell
Hyperion: a DSL for writing benchmarks to measure and analyze software performance. #Haskell
Highly cited theorems. ~ J.D. Cook #Math
Clojure numerics, part 2: General linear systems and LU factorization. ~ Dragan Djuric #Clojure #Math
Generalized refocusing: from hybrid strategies to abstract machines. ~ M. Biernacka, W. Charatonik & K. Zielińska #Coq
Combining Brick and Haskeline. ~ Gustav Behm #Haskell
How the List Monad helped me better understand Non-deterministic Polynomial time complexity. ~ Quentin Duval #Haskell
Haskell Study Startup: Launch your own Haskell study group. ~ Steven Syrek #Haskell
On dependent types and intuitionism in programming mathematics. ~ S.D. Meshveliani #Haskell #Agda #Math
An existence theorem of Nash equilibrium in Coq and Isabelle. ~ S. Le Roux, É. Martin & J.G. Smaus #Coq #IsabelleHOL
Signature inference for functional property discovery. ~ Tom Sydney Kerckhove #MSc_Thesis #Haskell
EasySpec: Signature inference for functional property discovery in Haskell. ~ Tom Sydney Kerckhove #Haskell
Elaboration on functional dependencies. ~ G. Karachalias & T. Schrijvers #Haskell
Reading EPUBs in Emacs. ~ Irreal #Emacs #EPub
Distant decimals of pi. ~ Y. Bertot, L. Rideau & L. Théry #Coq #Math
From logic programming to human reasoning: how to be artificially human. ~ EAD Saldanha #PhD_Thesis #LogicProgramming #AI #Logic
A reasoning system for a first-order logic of limited belief. ~ C. Schwering #Logic #AI #ATP
Swift logic for Big Data and knowledge graphs. ~ L. Bellomarini et als. #Logic #Big_Data #AI
Prolog loves graphs (How to use Prolog to implement graph traversal). #Prolog
Prácticas de cálculo numérico con Maxima. ~ A. Vigueras #Maxima #Matemáticas #OpenLibra
Anselm’s God in Isabelle/HOL. ~ Ben Blumson #ITP #IsabelleHOL #AFP
Deep Learning and Deep Types: Tensor Flow and Dependent Types. ~ James Bowen #Haskell #TensorFlow
From textbooks to knowledge: a case study in harvesting axiomatic knowledge from textbooks to solve geometry problems. ~ M. Sachan et als.
All about strictness. ~ M. Snoyman #Haskell
GeoS: an end-to-end system that solves high school geometry questions. #Math
The shape of a benedictine monastery: the SaintGall ontology. ~ C. Cantale et als. #OWL2
TiML: a functional language for practical complexity analysis with invariants. ~ P. Wang, D. Wang & A. Chlipala #FP #ML #SMT
Functional programming for mortals with Scalaz. ~ Sam Halliday #eBook #FP #Scala
Introduction to Homotopy Type Theory. ~ T. Altenkirch #HoTT
Functional programming and modern DevOps. ~ Aaron Contorer #FP #Haskell
ML for the working programmer, 2nd Edition. ~ L. Paulson #eBook #FP #ML
¿Puede la retroinformática darnos mejores programadores en el futuro? Este estudio cree que sí. #Programación
Obverse versus reverse: benchmarking in Haskell with criterion. ~ J.P. Villa #Haskell
Verified cryptography for Firefox 57. ~ B. Beurdouche, F. Kiefer, T. Taubert
Monoids: what they are, why they are useful, and what they teach us about software. ~ Quentin Duval #Haskell
Basic Haskell functional programming. ~ H. Conrad Cunningham #Haskell
A propositional theorem prover in Haskell, using Wang’s algorithm. ~ #Haskell #Logic
Trace and stable failures semantics for CSP-Agda. ~ B. Igried & A. Setzer #Agda
Theorem prover for intuitionistic propositional logic in Haskell. #Haskell #Logic
Differentiating functional programs. ~ Darryl McAdams #Haskell
Prime numbers in Haskell. #Haskell #Math
Certified password quality: a case study using Coq and Linux pluggable authentication modules. ~ J.F. Ferreira et als. #Coq
Java from Haskell: a tutorial. ~ F. Domínguez | Tweag I/O #Haskell #Java
A certified reference validation mechanism for the permission model of Android. ~ G. Betarte et als. #Coq #Haskell
Simply logical (intelligent reasoning by example) in Swish. ~ P. Flach #Prolog #Logic #AI
Encode state transitions in types using linear types. ~ A. Spiwack | Tweag I/O #Haskell
Building Haskell projects with GHC. ~ Emil Axelsson #Haskell
Free me: Exploring the Free data type. ~ Fintan Halpenny #Haskell
Making Google tasks better (Part 2). ~ Martin Capodici #Haskell
Dots and Boxes. ~ Wikipedia #Game
Dots and Boxes game in Haskell. ~ Martin Capodici #Haskell
IMP compiler implemented in Haskell. ~ Eugeniy Meshcheryakov #Haskell
Introducción a la programación funcional. #I1M2017 #Haskell #CodeWorld
How to script with Stack. ~ M. Snoyman #Haskell
Langages de programmation. ~ Sylvie Boldo
Visualizing lazy evaluation. ~ Edsko de Vries #Haskell
Cryptographic hashing in Haskell. ~ M. Snoyman #Haskell
Checking it’s all in place: placeholders and dependent types. ~ James Bowen #Haskell #TensorFlow
SafeD. ~ Bartosz Milewski #Programming #SafeD #Cpp #Dlang
Representation and partial automation of the Principia Logico-Metaphysica in Isabelle/HOL. ~ D. Kirchner #ITP #IsabelleHOL #AFP
Scrap your reprinter (a datatype generic algorithm for layout-preserving refactoring). ~ H. Clarke & D. Orchard #Haskell
Transforming data structures into types: an introduction to dependent typing and its benefits. ~ Quentin Duval #Idris
Verifying properties of binarized deep neural networks. ~ N. Narodytska et als. #DeepLearning #Logic #SAT
Reluplex: an efficient SMT solver for verifying deep neural networks. ~ G. Katz et als. #DeepLearning #SMT
Introducción a la programación funcional con Haskell. #I1M2017 #Haskell
Practical concurrent Haskell: with Big Data applications. ~ S.L. Nita & M. Mihailescu #Haskell #BigData
Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL. ~ T. Nipkow et als. #IsabelleHOL
GHC compiler plugins in the wild: typing Java. ~ F. Domínguez & M. Boespflug #Haskell #Java
Basic category theory for (Scala) programmers (part I). ~ Gabriel Claramunt #Scala #Math
An introduction to functional programming. ~ Lucas Dicioccio #FP
Extrapolate: generalizing counter-examples of functional test properties. ~ R. Braquehais & C. Runciman #Haskell
Secure automotive software (the next steps). ~ L. Pike, J. Sharp, M. Tullsen, P.C. Hickey & J. Bielman
Certified bit-coded regular expression parsing. ~ R. Ribeiro & A. Du Bois #ITP #Agda
Alternatives to typed holes for talking to your compiler. ~ Christopher Allen #Haskell
Approximation algorithms using allegories and Coq. ~ D. Chowdhury #MSc_Thesis #Coq #Math
Representación del conocimiento. ~ F. Sancho #IA
What is a knowledge representation? ~ R. Davis, H. Shrobe & P. Szolovits. #AI
Beautiful aggregations with Haskell. ~ Evan Borden #Haskell
Grenade! Dependently typed neural networks. ~ James Bowen #Haskell #NeuralNetworks
Immutability and unboxing in array programming. ~ Manuel Chakravarty #Haskell
Introducción al razonamiento automático con Prover9 y Mace4. ~ F. Sancho #Prover9 #Mace4
The state of being stuck. ~ Ben Orlin #Math
The real risks of Artificial Intelligence. ~ David Lorge Parnas #AI
Analyzing individual proofs as the basis of interoperability between proof systems. ~ G. Dowek #Logic #ITP
The time ontology of Allen’s interval algebra. ~ M. Grüninger & Z. Li #Prover9
Machine learning and algorithmic model theory. ~ M. Grohe #ML #Logic
Category theory for programmers. ~ Bartosz Milewski (unofficial PDF and LaTeX source) #Haskell #Math
Una Lambda aventura en Haskell. ~ Francisco José Cháves #Haskell #Lógica #Matemáticas
Expected value of the diameter of a tree. ~ Atabey Kaygun #CommonLisp #Math
Premise selection for theorem proving by deep graph embedding. ~ M. Wang er als. #ATP #DeepLearning

Octubre 2017

Profunctors for encoding and decoding. ~ Kari Pahula #Haskell
Making your brain tingle: Functions as functors. ~ Sascha Wilde #Haskell
Codex: a web application for setting programming exercises in a learning environment. ~ Pedro Vasconcelos #Haskell
Codex-QuickcCheck: QuickCheck customizations for the Codex learning environment. ~ Pedro Vasconcelos #Haskell
Trouble with databases? Persevere with Persistent! ~ James Bowen #Haskell
Proof-checking Euclid. ~ M. Beeson, J. Narboux & F. Wiedijk #ITP #Coq #HOL_Light #Math
Org mode as an Exocortex. ~ Irreal #Emacs
What does explainable AI really mean? A new conceptualization of perspectives. ~ D. Doran, S. Schulz & T.R. Besold #XAI
CMSC-16100 Lecture 1: Introduction to Haskell. ~ R. Chugh & S.A. Kurtz #Haskell #I1M2017
A Quarter of Haskell (Supplementary notes for UChicago CMSC 16100). ~ R. Chugh & S.A. Kurtz #Haskell #I1M2017
A Quarter of Haskell: Introduction to Haskell. ~ R. Chugh & S.A. Kurtz #Haskell #I1M2017
A verified messaging system. ~ W. Mansky, A.W. Appel & A. Nogin #Coq
Domain Specific Languages of Mathematics: Lecture Notes. ~ P. Jansson & C. Ionescu #Haskell #Math #I1M2017
Metamorphisms. ~ Jeremy Gibbons #Haskell
Les méthodes formelles: l’autre arme de la cybersécurité. ~ Jean Goubault-Larrecq #Formal_verification
Which languages are bug prone. ~ Janet Swift #Programming
Ten things you should know about Haskell syntax. ~ Bartosz Milewski #Haskell
Deduzione automatica. ~ M.P. Bonacina #ATP #Logic
Formalizing and proving a typing result for security protocols in Isabelle/HOL. ~ A.V. Hess & S. Mödersheim #ITP #IsabelleHOL
How to compose streaming programs. ~F. Domínguez #Haskell
Natural deduction on Liquid Haskell. ~ Niki Vazou #Haskell #LiquidHaskell #Logic
From design patterns to category theory. ~ Mark Seemann #Programming #Math
Lists as context: A deeper look at the Applicative Type Class. ~ Will Kurt #Haskell
Why do our programs need to read input and write output? ~ G. Gonzalez #Haskell
Exponential sums make pretty pictures. ~ J.D. Cook #Math #Programming
Haskell Weekly 75: News from the Haskell community (October 5 2017). #Haskell
scalendar: Haskell Library to deal with resource availability in a Calendar. ~ Sebastián Pulido #Haskell
A large-scale study of programming languages and code quality in GitHub. ~ B. Ray et als. #Programming
Semantic versioning checking in a declarative package manager. ~ M. Hanus #Curry
Functional Pearl: Compiling a fifty year journey. ~ G. Hutton & P. Bahr #Haskell
News in Isabelle2017 (October 2017). #IsabelleHOL
A verified compiler from Isabelle/HOL to CakeML. ~ L. Hupel & T. Nipkow #IsabelleHOL
Matemáticas conceptuales: Una primera introducción a categorı́as. ~ W. Lawvere & S. Schanuel #Matemáticas
Category theory and functional programming. ~ Mikael Vejdemo Johansson #Math #CompSci #FunctionalProgramming
Isabelle functions: Always total, sometimes undefined. ~ Joachim Breitner #IsabelleHOL
Computational geometry: set operations on polytopes. ~ Maksymilian Owsianny #Haskell #Math
A Monoid for all seasons. ~ Julie Moronuki #Haskell #Logic #Math
Making Kalman filtering correct with types. ~ Dominic Steinitz #Haskell #DataScience
Array fusion with vector. ~ Manuel M T Chakravarty #Haskell
Scrap your bounds checks with Liquid Haskell. ~ Gabriel Gonzalez #Haskell #LiquidHaskell
Recursion schemes, part IV: Time is of the essence. ~ Patrick Thomson #Haskell
A mechanized proof of Higman’s lemma by open induction. ~ Christian Sternagel #IsabelleHOL #Math
What are some scientific applications of Haskell? ~ Edward Kmett #Haskell
A tail we don’t need to wag. ~ Dan Piponi #Haskell
Composing declarations in Template Haskell. #Haskell
The CEO of GitHub, which caters to coders, thinks automation will bring an end to traditional software programming. ~ Becky Peterson #Programming
hs-to-coq: Convert Haskell source code to Coq source code. ~ Antal Spector-Zabusky #Haskell #Coq
MagicHaskeller based agent makes finalist in 1st round of general AI challenge! #Haskell #AI
Contando números primos: Análisis contra Combinatoria. ~ Juan Arias de Reyna #Matemáticas #Computación
The combinatorial algorithm for computing π(x). ~ Douglas B. Staple #Math #CompSci
Homogeneous linear diophantine equations in Isabelle/HOL. ~ Florian Meßner et als. #ITP #IsabelleHOL #Math
Computer-assisted reconstruction and assessment of E. J. Lowe’s modal ontological argument. ~ D. Fuenmayor & C. Benzmüller #IsabelleHOL
hs-init: Tool for creating completely configured production Haskell projects. ~ Veronika Romashkina #Haskell
Advice for Haskell beginners. ~ G. Gonzalez #Haskell
The Hurwitz and Riemann ζ functions in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #ITP #Math
Hotswapping Haskell. ~ Jon Coens #Haskell
A verified solver for linear recurrences in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #ITP #Math
Dirichlet series in Isabelle/HOL. ~ M. Eberl #IsabelleHOL #ITP #Math
AI algorithms are starting to teach AI algorithms. #AI #Programming
Homogeneous linear diophantine equations in Isabelle/HOL. ~ F. Messner et als. #IsabelleHOL #ITP #Math
Formal methods for Answer Set Programming. ~ Amelia J. Harrison #PhD_Thesis #ASP
Formalization of quantum protocols using Coq. ~ J. Boender, F. Kammüller & R. Nagarajan #ITP #Coq
forall x: Calgary Remix (An introduction to formal logic). ~ P.D. Magnus et als. #eBook #Logic
Count the number of complex roots in Isabelle/HOL. ~ Wenda Li #IsabelleHOL #ITP #Math
Empirically testing the Chowla conjecture. ~ J.D. Cook #Math #Programming
ELFE: An interactive theorem prover for undergraduate students. ~ Maximilian Doré #ITP #Logic #Haskell
ELFE: Interactive theorem proving for students (code). ~ Maximilian Doré #ITP #Logic #Haskell
Good proofs are proofs that make us wiser. ~ Yu.I.Manin #Math
Formal methods during the programming phase. ~ R.F. Paige et als. #Formal_methods
Towards complete specification and verification with SMT. ~ N. Vazou et als. #Haskell #LiquidHaskell #Logic #SMT
Handout on basics behind answer sets. ~ Yuliya Lierler #ASP #Logic #Programming
Evaluate winding numbers through Cauchy indices in Isabelle/HOL. ~ Wenda Li #IsabelleHOL #ITP #Math
Formalization of Pell’s equation in the Mizar system. ~ M. Acewicz & K. Pak #ITP #Mizar #Math
Tangled Webs: Testing an integrated system. ~ James Bowen #Haskell
Didáctica con R, menos cuentas y más pensamiento crítico. ~ A. Galindo #Matemáticas #Enseñanza
Progress in the independent certification of Mizar Mathematical Library in Isabelle. ~ C. Kaliszyk & K. Pak #ITP #IsabelleHOL #Mizar #Math
System Description: Russell (A logical framework for deductive systems). ~ Dmitry Vlasov #ITP #Logic
Transition systems and automata in Isabelle/HOL. ~ J. Brunner #IsabelleHOL
Motor: Finite-state machines in Haskell. ~ Oskar Wickström #Haskell
Linear Haskell: practical linearity in a higher-order polymorphic language. ~ Jean-Philippe Bernardy et als. #Haskell
Using Stackage for GHC regression testing. ~ Manuel Chakravarty #Haskell
The Kuratowski closure-complement theorem in Isabelle/HOL. ~ P. Gammie & G. Gioiosa. #ITP #IsabelleHOL #Math
What’s the future of programming? The answer lies in functional languages. ~ Nick Heath #Programming #Haskell
The refinement calculus of reactive systems toolset. ~ I. Dragomir, V. Preoteasa & S. Tripakis #IsabelleHOL
Comonads for optionality. ~ Phil Freeman #Haskell #PureScript
The game of pattern matching. ~ Phil Freeman #Haskell #PureScript
Constructive pedagogy. ~ Julie Moronuki #Haskell #Pedagogy
Modern library for working with URIs. ~ Mark Karpov #Haskell
Why Computer Science is a science. Emanuele D’Osualdo #CompSi
Cuatro décadas de Informática en España. ~ Ángel G. Perianes #Historia
Temporal Answer Set Programming. ~ M. Diéguez #ASP
Réminiscences d’un chercheur en informatique 1967-2000. ~ Gérard Huet #OCaml #Coq
Formal proof of Banach-Tarski paradox. ~ Daniel de Rauglaudre #ITP #Coq #Math
A pragmatic introduction to category theory. ~ Daniela Sfregola #Scala #Category_theory
Answer Set Programming in Proofdoku. ~ Adam M. Smith #ASP #Game
proofdoku: Game with ASP-backed mechanics. ~ By Nick Warren, Mason Reed & Adam Smith #ASP #Game
Answer Set Programming tutorial (AIIDE2017). ~ Adam M. Smith #ASP #AI #Game
Jean D’Alembert: cómo pasar de matemático a figura pública. ~ J. Ferreirós #Historia #Matemática
Poisson distribution and prime numbers. ~ J.D. Cook #Math #Programming #Python
View and annotate PDFs in Emacs with PDF-tools. #Emacs
Mathematics and computation. ~ Avi Wigderson #eBook #Math #CompSci
Büchi complementation in Isabelle/HOL. ~ J. Brunner #IsabelleHOL
Functional programming with bananas, lenses, envelopes and barbed wire. ~ E. Meijer, M. Fokkinga & R. Paterson #FunctionalProgramming
Generalized bananas, lenses and barbed wire. ~ Edward Kmett #Haskell
An Idris library for recursion schemes, with liberal examples. ~ Vanessa McHale #Idris
Peeling the banana: Recursion schemes from first principles. ~ Zainab Ali #Scala
Near future of programming languages. ~ Stephen Diehl #Programming
Mechanizing exploratory game design. ~ Adam M. Smith #eBook #ASP #Game #AI
Command Line Interface Tweeter in Haskell. ~ Vanessa McHale #Haskell
Temporal type theory (A topos-theoretic approach to systems and behavior). ~ P. Schultz, D.I. Spivak
Solving a crossword in answer set programming. ~ Alessandro Bruni #ASP

Noviembre 2017

Formal methods and the KRACK vulnerability. ~ Joey Dodds #Cryptography #Formal_methods
ASP with applications to mazes and levels. ~ Mark J. Nelson & Adam M. Smith #ASP #Game
Notes on Answer Set Programming. ~ Chris Martens #ASP #Logic Programming
The basics of Answer Set Programming. ~ Olaf Aviss #ASP
A first look at Answer Set Programming. ~ Hakan Kjellerstrand #ASP
Constraint solving and planning with Picat. ~ N.F. Zhou, H. Kjellerstrand, J. Fruhman #eBook #Logic #Programming #Picat
BioASP: Answer Set Programming for systems biology. #ASP
Lecturas de teorías de categorías y programación funcional. #Matemáticas #Programación
Improve SAT-solving with machine learning. ~ Haoze Wu #ATP #SAT #ML
TypedFlow: a typed, higher-order frontend to TensorFlow and a high-level library for deep-learning. ~ Jean-Philippe Bernardy #Haskell #DeepLearning
Academic research in the 21st century: maintaining scientific integrity in a climate of perverse incentives and hypercompetition. ~ M.A. Edwards, S. Roy
Understanding HLint rules. ~ Neil Mitchell #Haskell
Computing with impossible types. ~ @haskell_cat #Haskell
Sum of heights in a binary tree. ~ Brent Yorgey #Algorithmic
Aivika: computation-based modeling and simulation in Haskell. ~ David E. Sorokin et als. #eBook #Haskell #Simulation
Notes and thoughts from reading Milewski “Category theory for programmers” written in Haskell. ~ Robert Peszek #Haskell #Category_theory
Foundations of implementations for formal argumentation. ~ F. Cerutti et als. #Logic #AI #ASP
Simplicity: a new language for blockchains. ~ Russell O’Connor #Coq #Blockchain
Las matemáticas que puede esconder un dónut. ~ Alfonso J. Población #Matemáticas
Who gets to be called a mathematician? ~ Junaid Mubeen #Math
A set solver for finite relation algebra. ~ M. Cristiá, G. Rossi #CLP
Profunctor Optics. ~ Bartosz Milewski #Haskell
BiGUL: the bidirectional generic update language. #Haskell #Agda
An axiomatic basis for bidirectional programming. ~ H.S. Ko, Z. Hu #Agda
An axiomatic basis for bidirectional programming (Agda code). ~ H.S. Ko, Z. Hu #Agda
A logical relation for monadic encapsulation of state (Proving contextual equivalences in the presence of runST). ~ A. Timany #Haskell
AutoML, la máquina que crea otras máquinas inteligentes. ~ David Sarabia #IA #AA
AutoML for large scale image classification and object detection. ~ B. Zoph, V. Vasudevan, J. Shlens, Q. Le #AI #ML
Is mathematics a fine art? ~ Adrian Hindes #Math
Teaching A.I. systems to behave themselves. ~ Cade Metz #AI #ML
Mathematicians measure infinities and find they’re equal. ~ Kevin Hartnett #Math
Refinement reflection: complete verification with SMT. ~ Niki Vazou #Haskell #LiquidHaskell #Logic #SMT
Persistent red black trees in Haskell. ~ Abhiroop Sarkar #Haskell
Improving Haskell. ~ Martin A.T. Handley & Graham Hutton #Haskell
Unie: Inequational reasoning assistant for proofs relating to improvement theory. ~ Martin A.T. Handley #Haskell
Generating good generators for inductive relations. ~ L. Lampropoulos, Z. Paraskevopoulou, B.C. Pierce #Coq #QuickCheck
Encoding DCC (Dependency Core Calculus) in Haskell. ~ M. Algehed & A. Russo #Haskell
Cómo calcular áreas contando puntitos. ~ M.A. Morales | El Aleph #Matemáticas
An introduction to univalent foundations for mathematicians. ~ D.R. Grayson #Math #Logic #HoTT
Proof theory. ~ J. Avigad #Math #Logic #ATP
Small resolution proofs for QBF using dependency treewidth. ~ E. Eiben, R. Ganian & S. Ordyniak #Math #Logic #ATP
Capturing the future by replaying the past (Functional Pearl). ~ J. Koppel & A. Solar #SML
Finite state machines? (Your compiler wants in!) ~ Oskar Wickström #Haskell #Idris
Would aliens understand lambda calculus? ~ Tomas Petricek #Math #Logic #CompSci
Verifiable computing in Haskell. ~ Anthony Sheldon #Haskell #Math
Spatial reasoning about motorway traffic safety with Isabelle/HOL. ~ Sven Linker #IsabelleHOL
Hybrid multi-lane spatial logic in Isabelle/HOL. ~ Sven Linker #IsabelleHOL
The digits of pi. ~ Jeremy Gibbons #Haskell #Math
Haskell theory exploration scripts. ~ Chris Warburton #Haskell
The Has type class pattern. ~ Jonathan Fischoff #Haskell
Formalization of a Conflict-free Replicated Datatype for Internet Message Access Protocol commands in Isabelle/HOL. ~ T. Jungnickel, L. Oldenburg & M. Loibl #IsabelleHOL
Theory exploration on infinite structures. ~ S.H. Einarsdóttir #IsabelleHOL
Replicable parallel branch and bound search. ~ B. Archibald, P. Maier, C. McCreesh, R. Stewart & P. Trinder #Haskell
Purescript for Elm developers. ~ Marco Sampellegrini #PureScript #Elm
Answer Set Programming from a logical point of view. ~ P. Cabalar, D. Pearce & A. Valverde #ASP
Formalisms and formalizations: Glass Bead in conversation with Catarina Dutilh Novaes and Reviel Netz. #Logic #Math
To settle infinity question, a new law of Mathematics. ~ Natalie Wolchover #Math
Scientists in silico? ~ Carl McBride #CompSci
argmat-clpb: Solve argumentation problems using Constraint Logic Programming over boolean variables. ~ F. Pu, G. Luo & Y. Chen #CLP
Vigila tus primos. ~ Juan Arias de Reyna #Matemáticas #Computación #RSA
Millions of high-security crypto keys crippled by newly discovered flaw (Factorization weakness lets attackers impersonate key holders and decrypt their data). ~ Dan Goodin #RSA
The return of Coppersmith’s attack: Practical factorization of widely used RSA moduli. ~ M. Nemec, M. Sys, P. Svenda, D. Klinec, V. Matyas #Math #CompSci #RSA
Validating Brouwer’s continuity principle for numbers using named exceptions. ~ V. Rahli & M. Bickford #ITP #Nuprl #Coq
dblp2bibtex: Generates bibtex files for authors identified in the DBLP database. ~ Rob Stewart #Haskell #TeX
Rust as a gateway drug to Haskell. ~ Karol Kuczmarski #Rust #Haskell
MAC (A verified static information-flow control library). ~ M. Vassena & A. Russo #Haskell #Agda
In depth overview of Elm and PureScript. Lessons learned porting a game from PureScript to Elm. ~ Marco Sampellegrini #PureScript #Elm
Selecting a platform: JavaScript vs Elm vs PureScript vs GHCjs vs Scalajs. ~ Isaac Shapira #JavaScript #Elm #PureScript #GHCjs #Scalajs
Is (some) mathematics poetry? ~ J. Henle #Math
Neural-symbolic learning and reasoning: a survey and interpretation. ~ T.R. Besold et als. #AI
Haskell communities and activities report (November 2017). #Haskell
Por qué deberías aprender programación funcional ya mismo (con una breve introducción a Haskell). ~ A. Marzal #PF #Haskell
Answer Set Programming and CLASP (A tutorial). ~ S. Hölldobler, L. Schweizer #ASP
Parallelising your array code. ~ Manuel Chakravarty #Haskell
Portraits of famous philosophers who were also famous mathematicians. ~ C.S. Keyser #eBook #Math #History
Recursion schemes (why, how and more). ~ Sergey Vinokurov #Haskell
Domain Specific Languages of Mathematics: lecture notes (November 8, 2017). ~ Patrik Jansson Cezar Ionescu. #Haskell #Math
Algorithmic resource verification. ~ R Kandhadai Madhavan #PhD_Thesis #ITP #Leon
Proceedings of the Third Workshop on Bridging the gap between human and automated Reasoning (Is logic and automated reasoning a foundation for human reasoning?) #Logic #AR
How type errors were fixed and what students did? ~ B. Wu, S. Chen #Haskell
Learning user friendly type-error messages. ~ B. Wu, J.P. Campora III, S. Chen #Haskell
Unifying parsing and prettyprinting. ~ Sergey Vinokurov #Haskell
Adjunctions in everyday life (What we talk about when we talk about monads). ~ Rúnar Bjarnason #Haskell
Jargon from the functional programming world in simple terms! #FuncionalProgramming
Scala code examples for functional programming jargon. ~ Ikhoon Eom #FuncionalProgramming #Scala
Mechanizing Principia Logico-Metaphysica in functional type theory. ~ D. Kirchner, C. Benzmüller, E.N. Zalta #IsabelleHOL #RA2017
Representation and partial automation of the Principia Logico-Metaphysica in Isabelle/HOL. ~ D. Kirchner #Msc_Thesis #IsabelleHOL #RA2017
Finite-state machines, part 2: Explicit typed state transitions. ~ Oskar Wickström #Haskell
Let’s play with Regular Expressions. ~ Sergey Vinokurov #Haskell
Python implementation and construction of finite abelian groups. ~ P. Bradley, J. Smethurst #Python #Math
A programming digression: Kaprekar numbers. ~ E. Wallingford #Programming #Math
Net puzzle game in Elm. ~ Julian Priestley #Elm #Puzzle
Verification of PCP-related computational reductions in Coq. ~ Y. Forster, E. Heiter, G. Smolka #Coq
Rewriting a shallow DSL using a GHC Compiler extension. ~ M. Grebe, D. Young, A. Gill #Haskell
A programming digression: Farey sequences. ~ E. Wallingford #Programming #Math
Emacs for humans: glossary. #Emacs
QuickCheck and magic of testing. ~ A. Kuleshevich #Haskell #QuickCheck
Learn Emacs in one video. ~ Derek Banas #Emacs #I1M2017
Type-directed code generation. ~ Sandy Maguire #Haskell
Anatomy of a Haskell-based application, revisited. ~ Zhouyu Qian #Haskell
LeanCheck: a simple enumerative property-based testing library. ~ Rudy Matela #Haskell
A programming digression: Generating excellent numbers. ~ E. Wallingford #Programming #Math
Joys & frustrations of putting 34,000 lines of Haskell into production (at Vacation Labs). ~ Saurabh Nanda #Haskell
Schur number five. ~ Marijn J.H. Heule #SAT #Logic #AI
Category theory for programmers. ~ Bartosz Milewski #eBook #CategoryTheory #Haskell #OpenLibra
Verified functional algorithms. ~ Andrew W. Appel #FuncionalProgramming #ITP #Coq
Eta Fibers (Towards better concurrency on the JVM). ~ Rahul Muttineni #Haskell
Resolviendo problemas de satisfacción de restricciones con hormigas. ~ F. Sancho #PSR #IA
MonadBaseControl in five minutes. ~ Matt Parsons #Haskell
Dependent types in Haskell. ~ Sasa Bogicevic #Haskell
A formally proved, complete algorithm for path resolution with symbolic links. ~ R. Chen, M. Clochard, C. Marché #ITP #Coq
Functional pearl: Nested Datacubes. ~ Tim Philip Williams #Haskell
Spheres and points. ~ Bassel Mabsout #Haskell
tzimtsum: A Presburger arithmetic proposition decider Haskell library. #Haskell #Logic #Math
Stochastic matrices and the Perron-Frobenius theorem in Isabelle/HOL. ~ R. Thiemann #IsabelleHOL #Math
An EDSL for KDB/Q (rationale, techniques and lessons learned). ~ Tim Williams #Haskell
Talk notes: Lazy evaluation in Haskell. ~ Kostiantyn Rybnikov #Haskell
HyperHaskell: a graphical interpreter for the programming language Haskell. ~ Heinrich Apfelmus #Haskell
IPS-like proof systems based on binary decision diagrams. ~ A. Knop #Logic #AR #IPS
Circuit complexity, proof complexity, and polynomial identity testing. ~ J.A. Grochow, T. Pitassi #AR #GröbnerBases
Type theory in 15min. ~ Niki Vazou #Programming
Una formalización del sistema de los números reales. ~ J.O. Acevedo y J.L. Echeverri #ITP #Agda
Exference: Haskell tool to generate expressions from types. ~ Lennart Spitzner #Haskell
Exference: Rubbing the Lamp once more. ~ Lennart Spitzner #Haskell
Programación funcional avanzada (2017). ~ Ernesto Hernández-Novich #Curso #Haskell
Can A.I. be taught to explain itself? ~ C. Kuang #XAI
Teoría de categorías en Scala: Tipos y funciones. ~ A. Alcalde #TeoríaCategorías #Scala
Carp: A statically typed Lisp, without a GC, for high performance applications. #Haskell #Lisp
¿Porqué usar programación funcional? ~ Marco Ordoñez #ProgramacionFuncional
Proving Peano arithmetic partially consistent? ~ R.J. Lipton & K.W. Regan #Logic
Stochastic matrices and the Perron–Frobenius theorem in Isabelle/HOL. ~ René Thiemann #ITP #IsabelleHOL #Math
Session types in Cloud Haskell. ~ Ferdinand van Walree #PhD_Thesis #Haskell
Hamiltonian dynamics in Haskell. ~ Justin Le #Haskell #Math #Physic
My unusual hobby. ~ Stephan Boyer #ITP #Coq
sparse-linear-algebra: Numerical computation in native Haskell. ~ Marco Zocca #Haskell #Math
Total Haskell is reasonable Coq. ~ A. Spector-Zabusky, J. Breitner, C. Rizkallah, S. Weirich #Haskell #Coq
Deciphering Haskell’s applicative and monadic parsers. ~ Eli Bendersky #Haskell
Reseña: “Apología de un matemático” de G. H. Hardy. ~ F.R. Villatoro #Matemáticas
Lecturas sobre teoría de categorías y programación funcional. #TeoriaDeCategorias #ProgramacionFuncional #Haskell
European Union regulations on algorithmic decision-making and a “right to explanation”. ~ B. Goodman, S. Flaxman #MachineLearning
Haskell-University: Portfolio-based approach to learning Haskell. #Haskell
Symmetric groups on finite sets in PureScript. #PureScript #Math

Diciembre de 2017

Teaching the formalization of mathematical theories and algorithms via the automatic checking of finite models. ~ W. Schreiner, A. Brunhuemer, C. Fürst #ITP #Math #RISCAL
Números piramidales de cuatro dimensiones. ~ Antonio Roldán #Matemáticas #Programación
From logic programming to machine ethics. ~ A. Saptawijaya, L.M. Pereira #LogicProgramming #KRR #AI
Tierless Web programming in ML. ~ G. Radanne #PhD_Thesis #FunctionalProgramming #OCaml
A domain specific language for drum beat programming. ~ A.R. Du Bois, R. Ribeiro #Haskell #DSL #Music
A formal proof in Coq of a control function for the inverted pendulum. ~ D. Rouhling #ITP #Coq #Math #Physics
Writing code like a mathematical proof. ~ Spiro Sideris #Math #Programming
Haskell for dummies. ~ M. Snoyman #Haskell
CompCert: Practical experience on integrating and qualifying a formally verified optimizing compiler. ~ D. Kästner et als. #ITP #Coq #CompCert
Reflecting on Haskell in 2017. ~ Stephen Diehl #Haskell
Slides and other materials for functional programming lectures ITMO university. ~ D. Kovanikov, A. Seroka #Haskell
Point-free or die: tacit programming in Haskell and beyond. ~ Amar Shah #Haskell
Voting with ties: Strong impossibilities via SAT solving. ~ F. Brandt, C. Saile, C. Stricker #SAT_solving
A constructive formalisation of semi-algebraic sets and functions. ~ B. Djalal #ITP #Coq #Math
Arithmetic coding. ~ Jeremy Gibbons #Haskell #Math
Finding bugs in Haskell code by proving it. ~ J. Breitner #Haskell
Using Haskell on the frontend. ~ Vanessa McHale #Haskell
La inteligencia artificial que caza noticias para Reuters en Twitter. ~ David Sarabia #IA
Reuters Tracer: toward automated news production using large scale social media data. ~ X. Liu et als. #AI #BigData
learn elm: discover why people are switching to Elm and how you can get started today! #elm
Un bestiario fractal de curvas para rellenar el espacio (y el cerebro). ~ @Alvy #Fractales
Brainfilling curves: a fractal bestiary. ~ Jeffrey Ventrella
A complete taxonomy of plane-filling curves. ~ Jeffrey Ventrella #Fractal
Analyzing individual proofs as the basis of interoperability between proof systems. ~ G. Dowek #ITP #Coq #IsabelleHOL
Functional pearl: integer partitions and QuickCheck. ~ Vanessa McHale #Haskell
Secret link uncovered between pure math and physics. ~ Kevin Hartnett #Math #Physics
Cómo compartir un secreto usando sistemas de ecuaciones lineales. ~ A. Cano, J.M. LunA, A. Rojas #Matemáticas
The mind as a computational system. ~ Christoph Adami #AI
Geometría axiomática. ~ Gerard Romo Garrido #Matemáticas
Variations on a theme: A set of curated examples meant to show Haskell’s expressiveness. ~ Vanessa McHale #Haskell
P = NP: Perhaps I change my mind. (An old result put a new way). ~ R.J. Lipton, K.W. Regan #Math #CompSci
Mathematicians crack the cursed curve. ~ Kevin Hartnett #Math
Notes on mathematical writing. ~ Clark Barwick #Math
Rings: an efficient Java/Scala library for polynomial rings. ~ S. Poslavsky #Scala #Math
Towards automatic resource bound analysis for OCaml. ~ J. Hoffmann, A. Das, S.C. Weng #OCaml
The role of theory in Deep Learning. ~ David McAllester #AI #DeepLearning
Computation in Logic and Logic in Computation. ~ S. Salehi #Logic #CompSci
All about strictness analysis (part 1). ~ Sebastian Graf #Haskell
Introduction to logic programming with Prolog. ~ Mathias Schilling #Prolog
Co finds a pairing. ~ Phil Freeman #Haskell
Streaming arithmetic coding. ~ Jeremy Gibbons #Haskell #Math
A framework for certified self-stabilization. ~ S. Devismes, P. Corbineau, K. Altisen #ITP #Coq
Getting things done in Haskell. ~ Jasper Van der Jeugt #Haskell
Dismal arithmetic. ~ D. Applegate, M. LeBrun, N.J.A. Sloane #Math
The Haskell pyramid. ~ Patrick Nielsen #Haskell
fugacious: An example Haskell Web application. ~ Jasper Van der Jeugt #Haskell
swMATH: An information service for mathematical software. #Math #CompSci
Computational Logic: its origins and applications. ~ L.C Paulson #Logic #ITP #IsabelleHOL
Monadification of functional programs. ~ M. Erwig, D. Ren #Haskell
An interactive introduction to quantum computing (or what do you mean they can be both zero and one at the same time!) ~ D. Kemp #CompSci
Efficiency is not associative for matrix multiplication. ~ J.D. Cook #Math #CompSci
A brief introduction to category theory. ~ D. Hofmann #CategoryTheory
Applications of automated reasoning. ~ J. Harrison #AutomatedReasoning
El Tao de la programación. #Programación
The Tao of programming. #Programming
Verified iptables firewall analysis & verification. ~ C. Diekmann, L. Hupel, J. Michaelis, M. Haslbeck, G. Carle #ITP #IsabelleHOL
A tour of Go in Haskell. ~ Osanai Kazuyoshi #Haskell
Reading simple Haskell. ~ Gil Mizrahi #Haskell
Continuation passing style Free Monads and direct style Free Monads. ~ Quentin Duval #Idris
Folding Christmas fractals. ~ Clarissa Grandi #Math
Online Turing machine simulator. ~ Martín Ugarte #CompSci #Turing
A logical relation for monadic encapsulation of state (proving contextual equivalences in the presence of runST). ~ A. Timany et als. #ITP #Coq #Haskell
What makes Haskell unique. ~ M. Snoyman #Haskell
safe-money: Money in the type system where it belongs. ~ Renzo Carbonara #Haskell
Emacs: Org mode, programing language code markup. ~ Xah Lee #Emacs #Programming #OrgMode
taskell: A command line task manager written in Haskell. ~ Mark Wales #Haskell
Logic books of the year? ~ Peter Smith #Logic
SLS: Songbird + Lemma Synthesis (a separation logic prover which can automatically synthesize inductive lemmas on-the-fly). #ATP #OCaml
An axiomatic basis for bidirectional programming. ~ H.S. Ko, Z. Hu #ITP #Agda
Bonsai: synthesis-based reasoning for type systems. ~ K. Chandra, R. Bodik #Racket
Collapsing towers of interpreters. ~ N. Amin, T. Rompf #Lisp #Scala
Debug: Haskell library for debugging. ~ Neil Mitchell #Haskell
Fast and fearless evolution of server-side Web applications. ~ Oskar Wickström #Haskell
A water-based solution of polynomial equations. ~ Mark Levi #Math
Safety and conservativity of definitions in HOL and Isabelle/HOL. ~ O. Kunčar, A. Popescu #ITP #IsabelleHOL
The string search algorithm by Knuth, Morris and Pratt in Isabelle/HOL. ~ F. Hellauer, P. Lammich #IsabelleHOL
Monadic “do” block, yet again (What should get into your “do” block?) ~ Arvind Devarajan #Haskell
Lambda calculus in Clojure (part 1). ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure
Haskell in production in a startup in 2017? Yup. ~ Frédéric Menou Clément Delafargue #Haskell
Functional programming with graphs. ~ @futtetennista #Haskell
Solving satisfiability using inclusion-exclusion. ~ A. Zaleski #Logic #Sat #Maple
The Haskell performance checklist. ~ Chris Done #Haskell
Benchmarks for numbers: ints, doubles, bignums, rationals, etc. ~ Chris Done #Haskell
Splitting and splicing intervals (part 1). ~ R. Jhala #Haskell #LiquidHaskell
De Lutero a Voevodsky, pasando por Brouwer: Reformas en matemáticas. ~ J. Ferreirós #Matemáticas
A library for algorithmic game theory in Ssreflect/Coq. ~ A. Bagnall, S. Merten, G. Stewart #ITP #Coq
Building Haskell apps with Docker. ~ D. Bertovic #Haskell
All about reflection: a tutorial. ~ A. Spiwack #Haskell
A Lisp REPL in your pocket. ~ Kvardek Du #Lisp #Android
Reasoning about program behavior algebraically. ~ Stephen Diehl #Haskell
Understanding simplicity: implementing a smart contract language in 30 lines of Haskell. ~ Dan Robinson #Haskell
Evolutionary programming converts darwinism into algorithms. ~ R. Colin Johnson #Programming #AI
The Mason–Stother’s theorem. ~ Manuel Eberl #ITP #IsabelleHOL
Some notes about how I write Haskell. ~ Getty Ritter #Haskell
Zipperposition: An automatic theorem prover in OCaml for typed logic with equality, datatypes and arithmetic. ~ Simon Cruanes #OCaml #ATP #Logic
Extending superposition with integer arithmetic, structural induction, and beyond. ~ Simon Cruanes #PhD_Thesis #OCaml #ATP #Logic
Programas artístico-matemáticos en menos de 280 caracteres. ~ @Alvy #Programación #Matemáticas
Introduction to singletons (Part 1). ~ Justin Le #Haskell
On possible use of quantifier elimination software in upper secondary mathematics education. ~ Y. Sato, R. Fukasaku #Math #Logic
The median-of-medians selection algorithm. ~ Manuel Eberl #ITP #IsabelleHOL
Integrated simulation and formal verification of a simple autonomous vehicle. ~ A_ Domenici, A. Fagiolini, M. Palmieri #Formal_verification #ITP #PVS
importify: manage Haskell imports quickly. ~ Dmitry Kovanikov et als. #Haskell
Beginning Computer Science with R. ~ H. White #CompSci #Rstats
Protolude: A sensible starting Prelude for building custom Preludes. ~ Stephen Diehl #Haskell
Scaling Isabelle proof document processing. ~ M. Wenzel #IsabelleHOL
Getting used to R, RStudio, and R Markdown. ~ C. Ismay #Rstats
Tiny art in less than 280 characters. ~ Antonio S. Chinchón #Rstats
Programar (en R) te da alas. ~ Antonio S. Chinchón #Rstats
Formal proof of polynomial-time complexity with quasi-interpretations. ~ H. Férée et als. #ITP #Coq
A library for algorithmic game theory in Ssreflect/Coq. ~ A- Bagnall, S. Merten, G. Stewart #ITP #Coq
Annotated multisemantics to prove Non-Interference analyses. ~ G. Cabon, A. Schmitt #ITP #Coq

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Lecturas del año 2017.org

Lecturas del año 2017.org

Lecturas del Grupo de Lógica Computacional durante el año 2017

Contenido

Enero 2017

Febrero 2017

Marzo 2017

Abril 2017

Mayo 2017

Julio 2017

Agosto 2017

Septiembre 2017

Octubre 2017

Noviembre 2017

Diciembre de 2017

Files

Lecturas del año 2017.org

Latest commit

History

Lecturas del año 2017.org

File metadata and controls

Lecturas del Grupo de Lógica Computacional durante el año 2017

Contenido

Enero 2017

Febrero 2017

Marzo 2017

Abril 2017

Mayo 2017

Julio 2017

Agosto 2017

Septiembre 2017

Octubre 2017

Noviembre 2017

Diciembre de 2017