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

Este repositorio es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el año 2019. 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 2019
Febrero 2019
Marzo 2019
Abril 2019
Mayo 2019
Junio 2019
Julio 2019
Agosto 2019
Septiembre de 2019
Octubre de 2019
Noviembre de 2019
Diciembre de 2019

Enero 2019

Evaluation of Isabelle with a proof of the perfect number theorem. ~ Mark IJbema. #ITP #IsabelleHOL #Math
Univalent categories (A formalization of category theory in Cubical Agda). ~ F.H. Iversen #Msc_Thesis #ITP #Agda
Fun with kinds and GADTS. ~ Simon Peyton Jones. #Haskell #FunctionalProgramming
A combinatorial testing framework for intuitionistic propositional theorem provers. ~ P. Tarau. #ATP #Logic #Prolog
Haskell Code Explorer: Web application for exploring and understanding Haskell libraries. ~ Alexey Kiryushin. #Haskell
Haskell with only one type family. ~ Xia Li-yao. #Haskell
3D-Rubik’s cube simulator written in Haskell using Gloss. ~ Mark W. Ruszczycky. #Haskell
A new way of blogging about Prolog. ~ Yehonathan Sharvit. #Prolog #Klipse #Clojure
Formalization of concurrent revisions in Isabelle/HOL. ~ R. Overbeek. #ITP #IsabelleHOL
A tale of servant clients. ~ C. Delafargue. #Haskell
All about strictness analysis (part 2). ~ Sebastian Graf. #Haskell
Lens into wrapped newtypes. ~ Jappie Klooster. #Haskell
Parsing infinite streams with attoparsec. ~ Wander Hillen. #Haskell
Type annotations vs partial type signatures vs visible type applications. ~ Alexey Radkov. #Haskell
Three chapters of measure theory in Isabelle/HOL. ~ J. Hölzl, A. Heller. #ITP #IsabelleHOL #Math
Typeable: A long journey to type-safe dynamic type representation. ~ Toan Nguyen. #Haskell
Formalization of logic in the Isabelle proof assistant. ~ A. Schlichtkrull. #PhD_Thesis #ITP #IsabelleHOL #Logic
Course: Logical verification (2018-2019). ~ J. Blanchette et als. #ITP #LeanProver
Liquid Haskell tutorial. ~ Andres Löh. #Haskell #LiquidHaskell
The QED Manifesto revisited. ~ Freek Wiedijk. #ITP
The challenge of computer mathematics. ~ H. Barendregt, F. Wiedijk. #ITP
Zsyntax: Automated theorem prover for a linear logic-based calculus for molecular biology. ~ Filippo Sestini. #ATP #Logic #Haskell
Zsyntax: A formal language for molecular biology with projected applications in text mining and biological prediction. ~ G. Boniolo, M. D’Agostino, P.P. di Fiore. #ATP #Logic #Haskell
A formal model of the Document Object Model (DOM) in Isabelle/HOL. ~ A.D. Brucker, M, Herzberg. #ITP #IsabelleHOL
(The Cartoon Guide to) Lob’s Theorem. ~ Eliezer Yudkowsky. #Logic
Cantor pairing. #Haskell #FunctionalProgramming #Math
Why Haskell I: Simple data types! ~ James Bowen. #Haskell #FunctionalProgramming
Short overview of Haskell concepts. ~ E. Pogrebnyak et als. #Haskell #FunctionalProgramming
Machine learning leads mathematicians to unsolvable problem. ~ D. Castelvecchi. #AI #Math #MachineLearnig
Unprovability comes to machine learning. ~ L. Reyzin #AI #Math #MachineLearnig
Answer Set Programming (A story of default negation, definitions and informal semantics) . ~ M. Truszczynski #ASP #Logic #Programming #KR
Hakyll + TikZ. ~ Taeer Bar-Yam. #Haskell
Purely functional GTK+, Part 1: Hello World. ~ Oskar Wickström. #Haskell
Validating form data via applicative functors. ~ Kostiantyn Rybnikov. #Haskell
A reduction theorem for store buffers. ~ E. Cohen, N. Schirmer. #ITP #IsabelleHOL
HaskellQuest: a game for teaching functional programming in Haskell. ~ R. Fu. #Teaching #Haskell
Teaching to read Haskell. ~ Joachim Breitner. #Haskell
Haskell for readers. ~ Joachim Breitner. #Haskell
Types of proof system. ~ Peter Smith. #Logic #ITP
Nombres premiers, Euclide et Coq. ~ A. Alvarez. #ITP #Coq #Math
Column addition. ~ Kevin Buzzard. #ITP #LeanProver #Math
The forgotten history of OOP. ~ Eric Elliott. #Programming #History
Building the verifiable Web. ~ Kevin Buzzard. #Blockchain
The compactness theorem and applications. ~ B. Call #Logic
Handbook of modal logic. ~ P. Blackburn, J. van Benthem, F. Wolter. #Logic
A comparison of functional and imperative programming techniques for mathematical software development. ~ S. Frame, J.W. Coffey. #Haskell #Cpp #Math
HaskellRank 11: Treating lists as monads. ~ @tsoding. #Haskell #HaskellRank
Why Haskell II: Sum types. ~ James Bowen. #Haskell #Java #Python
Correct by construction programming in Agda. ~ Jesper Cockx. #ITP #Agda
An algebra for higher-order terms in Isabelle/HOL. ~ Lars Hupel. #ITP #IsabelleHOL
Haskell, Nix and Vim: Getting started. ~ Tobias Pflug. #Haskell #Nix #Vim
The history and concept of computability. ~ Robert I. Soare. #CompSci
Ode on a random urn (Functional pearl). ~ L. Lampropoulos, A. Spector-Zabusky, K. Foner, #Haskell
Haskell Showroom: How to switch between multiple kubernetes clusters and namespaces. ~ Deni Bertovic #Haskell
A touch of topological quantum computation in Haskell Pt. II: Automating drudgery. ~ Philip Zucker. #Haskell
IMP2: Simple program verification in Isabelle/HOL. ~ Peter Lammich and Simon Wimmer. #ITP #IsabelleHOL
Verifiable certificates for predicate subtyping. ~ F. Gilbert. #ITP #PVS
Mechanization of separation in generic extensions. ~ E- Gunther, M. Pagano, P.S Terraf. #ITP #IsabelleHOL
Ltac2: Tactical warfare. ~ P.M. Pédrot. #ITP #Coq
A materialist dialectica. ~ P.M. Pédrot. #PhD_Thesis #Logic #CompSci
Löb and möb: strange loops in Haskell. ~ David Luposchainsky. #Haskell
Ignoring HLint (HLint now has more ways to ignore hints you don’t like). ~ Neil Mitchell. #Haskell
A binomial urn. ~ Donnacha Oisín Kidney. #Haskell
Dynamic graphs: A Haskell library for the dynamic connectivity problem. ~ Jasper Van der Jeugt. #Haskell
Hindsight on Advent of Code 2018. ~ Dimitri Sabadie. #Haskell
Lean Forward: Usable computer-checked proofs and computations for number theorists. #ITP #LeanProver #Math
mathlib: Lean mathematical components library. #ITP #LeanProver #Math
Using Lean with undergraduate mathematicians. ~ Kevin Buzzard. #ITP #LeanProver #Math
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. ~ F. Immler, B. Zhan. #ITP #IsabelleHOL #Math
Las mentes matemáticas mueven el mundo. ~ G. Abril. #Matemáticas
A new style of mathematical proof. ~ William Farmer. #Logic #Math #ITP
Resources for teaching with formal methods. ~ Jeremy Avigad. #Logic #Math #CompSci #ITP
Dynamic class initialization semantics: a Jinja extension. ~ S. Mansky, E.L. Gunter. #ITP #IsabelleHOL
Discrete Math in Coq. ~ B.C. Pierce et als. #ITP #Coq Math
Teaching discrete mathematics to early undergraduates with “Software Foundations”. ~ M. Greenberg, J.C. Osborn. #ITP #Coq #Math
Course: Discrete mathematics and functional programming. ~ M. Greenberg. #ITP #Coq #Math
Formally verified big step semantics out of x86-64 binaries. ~ I. Roessle, F. Verbeek, B. Ravindran. #ITP #IsabelleHOL
Pensando en programar. ~ Gonzalo García Braschi. #Programación
Data-category: a collection of categories, and some categorical constructions on them. ~ Sjoerd Visscher. #Haskell
Why Haskell III: Parametric types. ~ James Bowen. #Haskell #Java #Cpp #Python
Farkas’ lemma and Motzkin’s transposition theorem in Isabelle/HOL. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL #Math
A bridge too far: E.W. Dijkstra and logic. ~ Maarten van Emden. #Logic
Verifying imperative programs using auto2. ~ B. Zhan. #ITP #IsabelleHOL
Proof editor for natural deduction in first-order logic (The evaluation of an educational aiding tool for students learning logic). ~ E. Björnsson et als. #Logic #Teaching #RA2018
Tarski’s relevance logic. R. D. Maddux. #Logic
Towards interactive Data Science in Haskell: Haskell in JupyterLab. ~ Matthias Meschede, Juan Simões. #Haskell
An in-depth look at quickcheck-state-machine. ~ Edsko de Vries. #Haskell
Using Jape for “Introduction to formal proof”. ~ Bernard Sufrin. #ITP #Jape #Logic
Proving pointer programs in higher-order logic. ~ F. Mehta, T. Nipkow. #ITP #IsabelleHOL
La révolution de l’apprentissage profond. ~ Y. Bengio. #AI
A beginner’s guide to the ways Haskell helps us avoid errors. ~ Mitchell Vitez. #Haskell
Solving rings in Aga. ~ Donnacha Oisín Kidney. #ITP #Agda #Math
Experience implementing a performant category-theory library in Coq. ~ J. Gross, A. Chlipala, D.I. Spivak. #ITP #Coq #CategoryTheory
Domain modelling with Haskell. ~ Oskar Wickström. #Haskell
R, Python, Julia … and Polyglot. ~ Steve Miller. #Programming #Rstats #Python #Julia #Jupyter
Crash course on notation in programming language theory. ~ Jeremy G. Siek. #CompSci
Haskell and type theory: better together. ~ V. Bragilevsky. #Haskell #TypeTheory #LambdaCalculus
Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification. ~ A.D. Barwell, C. Brown, K. Hammond. #Haskell
Applicative bidirectional programming (Mixing lenses and semantic bidirectionalization). ~ K. Matsuda, M. Wang. #Haskell
Applicative bidirectional programming and automatic differentiation. ~ Philip Zucker. #Haskell
Haskell trainings at Google. #Haskell
Haskell trainings at Google: 101. #Haskell
Haskell trainings at Google: 102. #Haskell
El origen de los signos matemáticos. ~ Raúl Ibáñez. #Matemáticas
Why Haskell IV: Typeclasses vs. inheritance. ~ James Bowen. #Haskell
On the expressive power of programming languages. ~ M. Felleisen. #FunctionalProgramming
How technology has changed what it means to think mathematically. ~ K. Devlin. #Math
A correct compiler from Mini-ML to a big-step machine verified using natural semantics in Coq. ~ A. Zúniga, G. Bel-Enguix. #ITP #Coq
Defining exceptions in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
Combinatory logic: from philosophy and mathematics to computer science. ~ A. Farrugia. #Logic #Math #CompSci #FunctionalProgramming
Primes and polynomials. ~ R.J. Lipton, K.W. Regan. #Math
Metaprogramming lecture notes. ~ Nada Amin. #Programming #Scala #Lisp #Prolog
Fractals and monads in Haskell (Part 1). ~ Derek Wise. #Haskell
Fractals and monads in Haskell (Part 2). ~ Derek Wise. #Haskell

Febrero 2019

Inteligencia artificial en el aula con Scratch 3.0. #Enseñanza #InteligenciaArtificial #Scratch
A list of foundational Haskell papers. ~ Emily Pillmore. #Haskell #FunctionalProgramming
Robust notes with embedded code. #Emacs #OrgMode
Introduction to applied linear algebra. ~ S. Boyd, L. Vandenberghe. #Math
Introduction to applied linear algebra (Julia language companion). ~ S. Boyd, L. Vandenberghe. #Math #Programming #JuliaLang
Rust as a gateway drug to Haskell. ~ Karol Kuczmarski. #Programming #Rust #Haskell
Rust for functional programmers. ~ Raphael ‘kena’ Poss. #Rust #Haskell #OCaml #FunctionalProgramming
Visualizing prequel meme prefix tries with recursion schemes. ~ Justin Le. #Haskell #FunctionalProgramming
Categories with monadic effects and state machines. ~ Marcin Szamotulski. #Haskell #FunctionalProgramming
CLIPS-based execution for PDDL planners. ~ T. Niemueller, T. Hofmann, G. Lakemeyer. #CLIPS
Data Science with Julia. ~ P.D. McNicholas, P. Tait. #eBook #DataScience #JuliaLang
Rust in 2019: security, maturity, stability. ~ Tony Arcieri. #RustLang
Formalização de algoritmos de criptografia em um assistente de provas interativo. ~ Guilherme Gomes Felix da Silva. #ITP #LeanProver
A purely functional computer algebra system embedded in Haskell. ~ H. Ishii #Haskell #FunctionalProgramming #CAS #Math
Computational algebra system in Haskell. ~ H. Ishii #Haskell #FunctionalProgramming #CAS #Math
Introduction to Julia (the language of the future for AI and ML). ~ Zhuo Jia Dai. #JuliaLang
Programming paradigms for dummies: what every programmer should know. ~ Adrian Colyer. #Programming
Structure and interpretation of computer programs. (Interactive version). ~ Hal Abelson, Gerald Jay Sussman. ~ #CompSci
A primer on type systems. ~ Glenn G. Chappell. #Programming #Haskell #Cpp #Python #Lua
On the impact of programming languages on code quality (A reproduction study). ~ E.D. Berger et als. #Programming
Functional programming applied to computational algebra. ~ I.H. Kessler. #Msc_Thesis #Math #CategoryTheory #FunctionalProgramming #Scala
Answer Set Programming (Draft). ~ V. Lifschitz. #DeclarativeProgramming #ASP
Verified real asymptotics in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL
A Rosetta stone for Haskell abstractions. ~ Chas Leichner. #Haskell #FunctionalProgramming
Wise man’s Haskell. ~ Andre Popovitch. #Haskell #FunctionalProgramming
Learning Haskell (Miscellaneous enlightenments). ~ Sandeep C.R. #Haskell #FunctionalProgramming
2062: The World that AI made. ~ Toby Walsh. #eBook #AI
10 reasons why you should learn Julia. ~ Gabriel Gauci Maistre. #Programming #JuliaLang
The Julia express. ~ Bogumił Kamiński. #Programming #JuliaLang
esverify: Verifying dynamically-typed higher-order functional programs by SMT solving. ~ C. Schuster, S. Banerjea, C. Flanagan. #SMT #ITP #LeanProver
Formal analysis of language-based Android security using theorem proving approach. ~ W. Khan et als. #ITP #Coq
Why Haskell V: Type families. ~ James Bowen. #Haskell
“What is programming languages research?” The talk. ~ Michael Hicks. #PL
The significance of Philosophy to Mathematics. ~ Richard Zach. #Philosophy #Mathematics
Proof and other dilemmas: Mathematics and Philosophy. ~ B. Gold, R.A. Simons. #Mathematics #Philosophy
SAT/SMT by example. ~ Dennis Yurichev. #SAT #SMT
Getting started with Isabelle/jEdit in 2018. ~ C. Sternagel. #ITP #IsabelleHOL
Literate programming against REST APIs. ~ Justin Barclay. #Emacs #OrgMode
Compiling with dependent types. ~ W.J. Bowman. #PhD_Thesis
Isabelle/UTP: Mechanised theory engineering for unifying theories of programming. ~ S. Foster et als. #ITP #IsabelleHOL
Haskell style guide. ~ Kowainik. #Haskell
Running your life with Emacs. ~ Garrett Hopper #Emacs
Typeable: A long journey to type-safe dynamic type representation. ~ Toan Nguyen. #Haskell
Curry-Howard correspondence example. ~ Vladimir Ciobanu. #Haskell #Logic #Math #CategoryTheory
Calc tutorial. #Emacs
The Emacs calculator. ~ Chris Wellons. #Emacs
Calc: an advanced calculator and mathematical tool. #Emacs #Math
A series of tutorials about emacs-calc. ~ Andrew Hyatt #Emacs #Math
Signatures and induction principles for higher inductive-inductive types. ~ A. Kaposi, A. Kovács. #ITP #Agda #Haskell
Chemoinformatics and structural bioinformatics in OCaml. ~ F- Berenger, K.Y.J. Zhang, Y. Yamanishi. #OCaml #FunctionalProgramming
Evolution of Emacs Lisp. ~ S. Monnier, M. Sperber. #Emacs #Lisp
Comparing nub implementations. ~ A. Klebinger. #Haskell
EE.UU crea un algoritmo que predice golpes de estado y crisis financieras. ~ A. Barbieri #AI
Typed meta-interpretive learning of logic programs. ~ R: Morel, A. Cropper, L. Ong. #Prolog #ML
Exámenes de programación funcional con Haskell. Vol. 4 (Curso 2012-13). #Haskell #ProgramaciónFuncional
Lean in LaTeX. ~ Kevin Buzzard. #ITP #LeanProver
AI automation of software (Demystifying functional programming and monads). ~ @datacountry_ai. #FunctionalProgramming #CategoryTheory
Model checking applied to quantum physics. ~ J. Guan, Y. Feng, A. Turrini, M. Ying. #ModelChecking
Bisecting floating point numbers in Julia. #JuliaLang #Math
Having your cake and eating it. ~ Tim Spence. #Haskell
Formal proof and analysis of an incremental cycle detection algorithm. ~ Armaël Guéneau. #ITP #Coq
Refactoring Haskell: A case study. ~ Vaibhav Sagar. #Haskell
Universal Turing Machine in Isabelle/HOL. ~ Jian Xu et als. #ITP #IsabelleHOL
Bank kata in Haskell - dealing with state. ~ Liam Griffin. #Haskell #FunctionalProgramming
Freer monads, more better programs. #Haskell #FunctionalProgramming
The types got you. ~ Mark Karpov. #Haskell #FunctionalProgramming
AFSM: Arrowized Functional State Machines. ~ Hanzhong Xu. #Haskell #FunctionalProgramming
The bipolar Lisp programmer. ~ Mark Tarver. #Lisp #Programming
A proof that Unix utility sed is Turing complete. ~ Peter Krumins. #Programming
SAT solvers as smart search engines. ~ Mate Soos. #SAT #Logic
Hacking using SAT and SMT solvers. ~ Mate Soos. #SAT #SMT #Logic
Using SAT solvers for cryptographic problems. ~ Mate Soos. #SAT #SMT #Logic
BIRD: Engineering an efficient CNF-XOR SAT Solver and its applications to approximate model counting. ~ Mate Soos, Kuldeep S. Meel. #SAT
Finding roots of polynomials in Haskell? ~ Brent Yorgey. #Haskell
Probabilistic primality testing in Isabelle/HOL. ~ D. Stüwe, M. Eberl. #ITP #IsabelleHOL #Math
An opinionated guide to Haskell in 2018. ~ Alexis King. #Haskell
A three-stage program you definitely want to write. ~ Matthew Pickering. #Haskell
Translating Haskell to C++ metaprogramming. ~ Jos van den Oever. #Haskell #Cpp
Compiling an Haskell EDSL to C. ~ F. Dedden. #Haskell #Clang
An overview of common Racket data structures. ~ Alex Harsányi. #Racket
Theorem proving for classical logic with partial functions by reduction to Kleene logic. ~ H. de Nivelle. #Logic
A constructive version of Tarski’s geometry. ~ M. Beeson. #Logic #Math
Exámenes de programación funcional con Haskell. Vol. 5 (Curso 2013-14). #Haskell #ProgramaciónFuncional
Worstsort. ~ Brent Yorgey. #Haskell
Machines are not our masters – but the sinister side of AI demands a smart response. ~ Will Hutton. #AI
Heyting and boolean algebras in Haskell. ~ Marcin Szamotulski. #Haskell #Math
stdio: A simple and high-performance IO toolkit for Haskell. #Haskell
Implementing the Davis–Putnam method. ~ H. Zhang, M.E. Stickel. #Logic #ATP
Monads are monoid objects. #Haskell #CategoryTheory
Set theory: constructive and intuitionistic ZF. ~ Laura Crosilla. #Logic #Math
Kruskal’s algorithm for minimum spanning forest in Isabelle/HOL. ~ M.P.L. Haslbeck et als. #ITP #IsabelleHOL
Towards justifying computer algebra algorithms in Isabelle/HOL. ~ W. Li. #ITP #IsabelleHOL #Math
Freer monads: too fast, too free. #Haskell
A touch of topological quantum computation 3: Categorical interlude. ~ Philip Zucker. #Haskell #CategoryTheory
A brief introduction to the λ-calculus (part 1). ~ Laurence Emms. #LambdaCalculus
The AI that can write fake news stories from handful of words. #AI
The inversions of a list in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL
Quantifiers in Agda. ~ Vladimir Ciobanu. #ITP #Agda
A brief introduction to the λ-calculus (part 2). ~ Laurence Emms. #LambdaCalculus
Elementary facts about the distribution of primes in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL #Math
Adding bit vectors - Branchless Comparisons. ~ John Ky. #Haskell
Is Haskell really the language of geniuses and academia? #Haskell
Why monadic IO? ~ Marcin Szamotulski. #Haskell #FunctionalProgramming
Exámenes de programación funcional con Haskell. (Vol. 6: Curso 2014-15). #Haskell #ProgramaciónFuncional
Commutativity theorems in groups with power-like maps. ~ R. Padmanabhan, Y. Zhang. #ATP #Prover9 #Math
Reflected decision procedures in lean. ~ S. Baek. #PhD_Thesis #ITP #LeanProver #Logic #Math
What’s the right way to QuickCheck floating-point routines? ~ Brent Yorgey. #Haskell
How can basic arithmetic make a self-referential sentence? ~ Russell O’Connor. #Haskell #Logic #Math
Sums of products for mutually recursive datatypes (The appropriationist’s view on generic programming). ~ V.C. Miraldo, A. Serrano. #Haskell #FunctionalProgramming
Of Algebirds, monoids, monads, and other bestiary for large-scale data analytics. ~ Michael G. Noll. #Scala #FunctionalProgramming
Finger trees in Agda. ~ Donnacha Oisín Kidney. #Agda
Formalization of mathematics in type theory (Report from Dagstuhl Seminar 18341). #ITP #Math
Statistics with Julia: Fundamentals for Data Science, Machine Learning and Artificial Intelligence. ~ H. Klok, Y. Nazarathy. #eBook #JuliaLang #DataScience #MachineLearnig #AI
A complete axiomatisation of reversible Kleene lattices. ~ P. Brunet. #ITP #Coq #Logic #Math
Rock–paper–scissors game in less than 10 lines of code. ~ Mosè Giordano. #Programming #JuliaLang
Matplotlib guide for people in a hurry. ~ Julia Kho. #Python
QuickCheck, Hedgehog, Validity. ~ Syd Kerckhove. #Haskell
How to write mathematics. ~ Paul R. Halmos. #Math
Theorem and algorithm checking for courses on logic and formal methods. ~ W. Schreiner. #ITP #Logic #Teaching
JupyterWith: Declarative, reproducible notebook environments. ~ J. Simões, M. Meschede. #Programming #Jupyter

Marzo 2019

Monoidal and applicative functors. ~ Marcin Szamotulski. #Haskell #FunctionalProgramming
Property-based testing in a screencast editor: Introduction. ~ Oskar Wickström. #Haskell
Beeraffe: A silly game in PureScript. ~ Jasper Van der Jeugt. #PureScript
Recursion schemes, part VI: Comonads, composition, and generality. ~ Patrick Thomson. #Haskell
Beautiful Racket (an introduction to language oriented programming using Racket). ~ Matthew Butterick. #Racket #Programming
Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #OCaml #FunctionalProgramming
Lazy validation. ~ Roman Cheplyaka. #Haskell
The basics of game programming in Common Lisp. ~ Mauricio Fernandez. #CommonLisp
Using Julia for Data Science (Part 02). ~ Cleyton Farias. #JuliaLang #DataScience
Pourquoi créer des nouveaux langages de programmation? ~ Ludovic Henrio. #Programmation
Matplotlib guide for people in a hurry. ~ Julia Kho. #Python #Matplotlib
Selective applicative functors: declare your effects statically, select which to execute dynamically. ~ A. Mokhov. #Haskell
Isomorphic web apps in Haskell. ~ Julien Dehos. #Haskell
Programmation fonctionnelle pour le web. ~ Julien Dehos. #Haskell
Neural network in 42 lines of Haskell. ~ Julien Dehos. #Haskell
Shareable Haskell with Jupyter! ~ James Bowen. #Haskell #Jupyter
Infinite types, infinite data, infinite interaction. ~ P. Hyvernat. #ITP #Agda
Means compatible with semigroup laws. ~ R. Padmanabhan, A. Shukla. #ATP #Prover9 #Math
Introduction to theoretical computer science. ~ Boaz Barak. #eBook #CompSci
DimDraw: A novel tool for drawing concept lattices. ~ D. Dürrschnabel, T. Hanika, G. Stumme. #AFC
Type classes for mathematics in type theory. ~ B. Spitters, E. van der Weegen. #ITP #Coq #Math
A library of formalised undecidable problems in Coq. ~ Dominique Larchey-Wendling et als. #ITP #Coq
GRUNGE: A grand unified ATP challenge. ~ C.E. Brown, T. Gauthier, C. Kaliszyk, G. Sutcliffe, J. Urban. #ATP
The state of Haskell in Ethereum. ~ Martin Allen. #Haskell
Why I use Julia. (Come for the speed. Stay for the productivity). ~ Josh Day #LuliaLang
What exactly makes the Haskell type system so revered (vs say, Java)? #Haskell #FunctionalProgramming
Computer-assisted proving of combinatorial conjectures over finite domains: A case study of a chess conjecture. ~ P. Janičić, F. Marić, M. Maliković. #ITP #IsabelleHOL #ATP #SAT #SMT
Dijkstra monads for all. ~ K. Maillard et als. #ITP #Coq
Stack cookbook. #Haskell #Stack
Rust for linear algebra and neural networks. ~ J.P. Moresmau. #RustLang #AI #MachineLearnig #Math
On Lamport’s critique of compositional reasoning. ~ Ilya Sergey. #Programming
Why Jupyter is not my ideal notebook. ~ Clément Walter. #Jupyter
From free algebras to free monads. ~ Marcin Szamotulski. #Haskell #CategoryTheory
Category theory for computing science. ~ M. Barr, C. Wells. #eBook #CategoryTheory
What are the advantages/disadvantages of uLisp vs C/C++? #Programming #Lisp #Cpp
An example of state-based testing in Haskell. ~ Mark Seemann. #Haskell
33 can be written as the sum of three cubes. ~ Peter Rowlett. #Math #CompSci
Gödel without (too many) tears. ~ Peter Smith. #Logic
AI efforts at large companies may be hindered by poor quality data. #AI
Learning a SAT solver from single-bit supervision. ~ D. Selsam et als. #SAT #Logic #MachineLearnig
On constructive-deductive method for plane euclidean geometry. ~ E.V. Ivashkevich. #ITP #Coq #Math
Typeable and Data in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
From math to machine: translating a function to machine code. ~ Brian Steffens #Haskell #Math
Writing a simple evaluator and type-checker in Haskell. ~ Boro Sitnikovski. #Haskell
These years in Common Lisp: 2018. ~ Vince Zd #CommonLisp
Visible dependent quantification in Haskell. ~ Ryan Scott. #Haskell
Cooking a Haskell curry with applicative functors. ~ G. Érdi. #Haskell
Logipedia: a multi-system encyclopedia of formal proofs. ~ G. Dowek, F. Thiré. #ITP #Logic #Math #Dedukti #Coq #Matita #HOL_Light #PVS #LeanProver
A framework for defining computational higher-order logics. ~ A. Assaf. #PhD_Thesis #ITP #Logic #Math #Dedukti
Nine chapters of analytic number theory in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL #Math
Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ M. Handley, N. Vazou, G. Hutton. #Haskell
Machine learning and the Continuum Hypothesis. ~ K.P. Hart. #MachineLearnig #SetTheory
Extending Haskell’s syntax! ~ James Bowen. #Haskell #FunctionalProgramming
Compdata trees and catamorphisms. ~ Ben Blaxill. #Haskell #FunctionalProgramming
Pure maths in crisis? ~ M. Freiberger. #Math #ITP #IsabelleHOL #LeanProver
Writing a lambda calculus evaluator in Haskell. ~ B. Sitnikovski. #Haskell #FunctionalProgramming #LambdaCalculus
Map/Reduce operations for scientific computing in Julia. ~ X. Vasseur. #JuliaLang
Introduction to Univalent Foundations of Mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda #math #HoTT
What is a proof? What should it be? ~ C. Benzmüller. #Logic #Math #ITP #ATP
FMS: Functional programming as a modelling language. ~ I. Dasseville, G. Janssens. #FunctionalProgramming #ASP
FMS (Functional Modelling System) tutorial. ~ I. Dasseville. #FunctionalProgramming #ASP
Lazy binary numbers. ~ Donnacha Oisín Kidney. #Haskell #Agda
Fractals and monads (Part 3). ~ Derek Wise. #Haskell #Math
A small use case for Deriving Via. ~ Sam Tay. #Haskell
Okay, maybe proofs aren’t dying after all. ~ J. Horgan. #Math
An introduction to existential types. ~ S. Bly. #FunctionalProgramming
A constructive proof of dependent choice in classical arithmetic via memoization. ~ É. Miquey. #ITP #Coq
Algorithms for verifying deep neural networks. ~ C. Liu, T. Arnon, C. Lazarus, C. Barrett, M.J. Kochenderfer. #JuliaLang #NeuralNetworks
Introduction to Python for science and engineering. ~ D.J. Pine. #eBook #Programming #Python
Computer science and metaphysics: a cross-fertilization. ~ D. Kirchner, C. Benzmüller, E.N. Zalta. #ITP #IsabelleHOL
Permutations by sorting. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
Tagless final encoding in Haskell. ~ J.P. Royo. #Haskell #FunctionalProgramming
Quantum Hoare logic in Isabelle/HOL. ~ J. Liu et als. #ITP #IsabelleHOL
Using SMT solvers to validate models for AI problems. ~ A. Arusoaie, I. Pistol. #ATP #SMT #AI
Universal (meta-) logical reasoning: The wise men puzzle (Isabelle/HOL dataset). ~ C. Benzmüller. #ITP #IsabelleHOL #Logic
A verifiable search for projective planes of order ten. ~ C. Bright. #ATP #SAT #Math
The SAT+CAS method for combinatorial search with applications to best matrices. ~ C. Bright et als. #ATP #SAT #CAS #Math
Comonadic builders. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
The minimalist Prelude … or why can’t Haskell be more like Purescript? #Haskell #FunctionalProgramming
Finger trees in Agda. ~ Donnacha Oisín Kidney. #Agda
Promonads, arrows, and Einstein notation for profunctors. ~ Bartosz Milewski. #Haskel #CategoryTheory
The transcendence of certain infinite series in Isabelle/HOL. ~ A, Koutsoukou-Argyraki, W. Li. #ITP #IsabelleHOL #Math
A formal, classical proof of the Hahn-Banach theorem. ~ M. Kerjean, A. Mahboubi. #ITP #Coq #Math
Partial type constructors (extended version). ~ M.P. Jones et als. #Haskell #FunctionalProgramming
Towards a constructive formalization of Perfect Graph Theorems (Slides)]. ~ A.K. Singh. R. Natarajan. #ITP #Coq #Math
Towards a constructive formalization of Perfect Graph Theorems. ~ A.K. Singh. R. Natarajan. #ITP #Coq #Math

Abril 2019

Students’ Proof Assistant (SPA). ~ Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From. #Logic #IsabelleHOL
Towards ranking geometric automated theorem provers. ~ N. Baeta, P. Quaresma. #ATP #Math
Learning how to prove: From the Coq proof assistant to textbook style. ~ S. Böhne, C. Kreitz. #Teaching #Logic #ITP #Coq
Building a bigger World. James Bowen. #Haskell #FunctionalProgramming
A history of the theory of types. ~ J. Collins. #Logic #History
The pillars of functional programming (part 1). N. Mozgovoy. #FunctionalProgramming
Dynamic typing in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
Jupyter kernel for Coq. ~ Eugene Loy. #ITP #Coq #Jupyter
IFL2: Chapters on propositional natural deduction, again. ~ Peter Smith. #Logic
Theorem and algorithm checking for courses on logic and formal methods. ~ W. Schreiner. #Logic #RISCAL
Proof complexity. ~ Jan Krajicek. #Book #Logic
Verified code generation from Isabelle/HOL. ~ L. Hupel. #PhD_Thesis #ITP #IsabelleHOL
Proving soundness of extensional normal-form bisimilarities. ~ P. Polesiuk, S Lenglet, D. Biernacki. #ITP #Coq
Hammering Mizar by learning clause guidance. ~ J. Jakubův, J. Urban. #ITP #Mizar #MachineLearnig
The Open Problem Garden: a collection of unsolved problems in mathematics. #Math
Idempotent applicatives, parametricity, and a puzzle. ~ D. Mlot. #Haskell #FunctionalProgramming
Proving addition is commutative in Haskell using singletons. ~ Philip Zucker. #Haskell #FunctionalProgramming
Data Science in Haskell: An example using temperature data from Thailand and Myanmar. ~ Dominic Steinitz. #Haskell #FunctionalProgramming #DataScience
A tiny compiler for a typed higher order language. ~ Danny Gratzer. #Haskell #FunctionalProgramming
Imperative Haskell. ~ Vaibhav Sagar. #Haskell #FunctionalProgramming
Programación funcional para mortales con Scalaz. ~ S. Halliday, O. Vargas. #Scalaz #ProgramaciónFuncional
Analysing mathematical reasoning abilities of neural models. ~ D. Saxton, E. Grefenstette, F. Hill, P. Kohli. #MachineLearnig
Libro de soluciones de problemas de programación funcional con Haskell propuestos en Exercitum (versión del 6-abr-19). #Haskell #Exercitium
Isomorphism and embedding. ~ Marko Dimjašević. #ITP #Agda #Math
Six easy ways to run your Jupyter Notebook in the cloud. #Jupyter
Fun with functors. ~ Marco Perone. #FunctionalProgramming #CategoryTheory
Foundations of functional programming. ~ L.C Paulson. #FunctionalProgramming #LambdaCalculus
Set theory for Computer Science. ~ G. Winskel. #Logic #Math
Foundations of Data Science. ~ D. Wischik. #DataScience
Type systems. ~ N. Krishnaswami. #TypeTheory
Web engines in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
Vado: A demo web browser engine written in Haskell. ~ Chris Done. #Haskell #FunctionalProgramming
The nature of infinity and beyond (An introduction to Georg Cantor and his transfinite paradise). ~ Jørgen Veisdal. #Logic #Math
The Riemann Hypothesis, explained. ~ Jørgen Veisdal. #Math
Abstract completion, formalized. ~ N. Hirokawa, A. Middeldorp, C. Sternagel, S. Winkler. #ITP #IsabelleHOL
On initial categories with families (Formalization of unityped and simply typed CwFs in Agda). ~ K. Brilakis. #Msc_Thesis #ITP #Agda
Constructing inductive-inductive types in cubical type theory. ~ J. Hugunin. #ITP #Agda #Coq
What making a cup of tea taught me about functional programming. Sam Fare. #FunctionalProgramming
Programming prospect theory in Prolog. ~ I. Kenryo. #Prolog #LogicProgramming
Generating more difficult mazes! ~ James Bowen. #Haskell #FunctionalProgramming
Julia Data Science Tutorial: Working with DataFrames and CSV. #JuliaLang #DataScience
A general theory of syntax with bindings in Isabelle/HOL. ~ L. Gheri. #ITP #IsabelleHOL
HOList: An environment for machine learning of higher-order theorem proving (extended version). ~ K. Bansal et als. #ITP #HOL_Light #MachineLearnig
A gentle introduction to symbolic execution. ~ B. Schroeder, J. Burget. #Haskell #SMT
Logic, explainability and the future of understanding. ~ S. Wolfram. #Logic
Applicative regular expressions using the free alternative. ~ Justin Le. #Haskell #FunctionalProgramming
To kata haskellen evangelion (Learn Haskell the easy way). ~ Cosmia Fu. #eBook #Haskell #FunctionalProgramming
Short proof of Menger’s Theorem in Coq (Proof Pearl). ~ C. Doczkal. #ITP #Coq #Math
Hammering Mizar by learning clause guidance. ~ J. Jakubův, J. Urban. #ATP #Mizar #MachineLearnig
Quantitative continuity and computable analysis in Coq. ~ F. Steinberg, L. Thery, H. Thies. #ITP #Coq #Math
The Rubik’s cube group. ~ Jared Corduan. #Haskell #FunctionalProgramming #Math
Become a better haskeller by learning about inductive types. ~ Marko Dimjašević. #Haskell #FunctionalProgramming
A primer on scientific programming with Python. ~ Hans Petter Langtangen. #eBook #Python #Programming
Introduction to Python for computational science and engineering (A beginner’s guide). ~ Hans Fangohr. #eBook #Python #Programming
Lisp used to generate rhythms for a contemporary string trio. #Lisp #Programming #Music
Learning Haskell through Google Code Jam. ~ Ashwin Narayan. #Haskell #FunctionalProgramming
New in CodeWorld: Share a folder as a gallery. ~ Chris Smith. #CodeWorld #Haskell
A cheatsheet to regexes in Haskell. ~ William Yao. #Haskell
Learning heuristics for automated reasoning through deep reinforcement learning. ~ G. Lederman et als. #ATP #DeepLearning
Executable formal specification of programming languages with reusable components. ~ L.T. van Binsbergen. #PhD_Thesis #Haskell #FunctionalProgramming
A new foundational crisis in mathematics, is it really happening? ~ M. Džamonja. #Logic #Math #HoTT
Declaring victory! (and starting again!) ~ James Bowen. #Haskell #FunctionalProgramming
A graphical introduction to dynamic programming. ~ Avik Das. #Algorithms #Programming #Python
Modern SAT solvers: fast, neat and underused (part 3 of N). ~ M. Hořeňovský. #Logic #SAT
Basic Cheat Sheet for Python (PDF, Markdown and Jupyter Notebook). ~ Carlos Montecinos Geisse. #Python #Programming
Evolution of programming languages. #Programming
Cubical Agda and probability monads. ~ Donnacha Oisín Kidney. #Agda
Can you avoid functional programming as a policy? ~ Eric Elliott. #FunctionalProgramming
Every day recursion schemes. ~ David Smith. #Haskell #FunctionalProgramming
Towards evolutionary theorem proving for Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL #MachineLearning
Eisbach: A proof method language for Isabelle. ~ D. Matichuk, T. Murray, M. Wenzel. #ITP #IsabelleHOL
Automation for proof engineering (Machine-checked proofs at scale). ~ D. Matichuk. #PhD_Thesis #ITP #IsabelleHOL
Other classical reasoning methods in Isabelle: From tactics and tacticals to automated reasoning in Isabelle. ~ Stephan Scheele. #ITP #IsabelleHOL
Microsoft debuts Bosque – a new programming language with no loops, inspired by TypeScript. ~ T. Clarbun. #FunctionalProgramming
Regularized programming with the BOSQUE language (Moving beyond structured programming). ~ Mark Marron. #FunctionalProgramming
Towards machine learning induction. ~ Yutaka Nagashima. #ITP #IsabelleHOL #MachineLearning
Course: Interactive theorem proving using Isabelle/HOL. ~ Christian Sternagel. #ITP #IsabelleHOL
Automated proof synthesis for propositional logic with deep neural networks. ~ Taro Sekiyama, Kohei Suenaga. #ATP #MachineLearning
PSL: proof strategy language for Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL
A certificate-based approach to formally verified approximations. ~ F. Bréhard, A. Mahboubi, D. Pous. #ITP #Coq #Math
Did Functional Programming get it wrong? (Why do monads feel so clumsy?). ~ reinman. #FunctionalProgramming
From theory to systems: a grounded approach to programming language education. ~ W. Crichton. #Teaching #Programming
Soundness and completeness: with precision. ~ Bertrand Meyer. #CompSci
Just do it: Simple monadic equational reasoning. ~ Jeremy Gibbons and Ralf Hinze. #Haskell #FunctionalProgramming
Microsoft’s new programming language ‘Bosque’ keeps your code simple. ~ Manisha Priyadarshini #Programming #Bosque
A working mathematician’s guide to parsing. ~ Jeremy Kun | Math ∩ Programming #Programming #LaTeX
Serializing mazes! ~ James Bowen. #Haskell #FunctionalProgramming
P=NP proofs. ~ R.J. Lipton. #CompSci #Math
Rewriting functions with fold and reduce. ~ Max Strübing. #Programming #Haskell #JavaScript
The theorem prover museum (Conserving the system heritage of automated reasoning). ~ M. Kohlhase. #ATP #ITP
Competitive programming in Haskell: Basic setup. ~ Brent Yorgey. #Haskell
Declarative programming with Prolog. ~ Aaron Kraus. #Prolog #LogicProgramming
Why check a proof? ~ R.J. Lipton. #CompSci
Formalization of logical calculi in Isabelle/HOL. ~ M. Fleury. #PhD_Thesis #ITP #IsabelleHOL #Logic
A verified SAT solver framework including optimization and partial valuations. ~ M. Fleury, C. Weidenbach, D. Zimmer. #ITP #IsabelleHOL #Logic
Continuous improvement with hlint code smells. ~ Ben Weitzman. #Haskell
Demystifying folds with GHCi. ~ Ayman Nadeem. #Haskell
Thinking in types. ~ Pat Brisbin. #Haskell
Transitioning to Haskell from other languages. ~ @typeclasses #Haskell #Java #JavaScript #Python
Python iterators. ~ @typeclasses #Python #Haskell
Python function decorators. #Python #Haskell
Intro to Higher Kinded Types in Haskell. ~ Patxi Bocos. #Haskell
Exercises for understanding Lenses. ~ William Yao. #Haskell
Compile driven development in action: refactoring to arrays! ~ James Bowen. #Haskell
Logic for exact real arithmetic. ~ H. Schwichtenberg, F. Wiesnet. #Logic #Mayh #MinLog #Haskell

Mayo 2019

Ordinal notations via simultaneous definitions. ~ F.N. Forsberg, C. Xu. #ITP #Agda #Logic #Math
A formalization of forcing and the unprovability of the continuum hypothesis. ~ J.M. Han, F. van Doorn. #ITP #LeanProver #Logic #Math
Code style and moral absolutes. ~ Brent Yorgey. #Haskell
QKD (Quantum Key Distribution) algorithm in Isabelle: Bayesian calculation. ~ Florian Kammüller. #ITP #IsabelleHOL
Warshall’s algorithm (survey and applications). ~ Zoltán Kása. #Algorithms
Backprop as Functor: A compositional perspective on supervised learning. ~ B. Fong, D.I. Spivak, R. Tuyéras. #MachineLearning #CategoryTheory
MIP: Travelling Salesman. ~ Ole Kröger. #Algorithms #JuliaLang
MINLP: Travelling Salesman with Neighborhoods. ~ Ole Kröger. #Algorithms #JuliaLang
Currying and partial application. ~ M. Lopes. #Haskell #Scala
Formalization of Dubé’s degree bounds for Gröbner bases in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
Formatting tabular data. ~ Oleg Grenrus. #Haskell
Good symbolic differentiation requires multidimensional wobbliness. #Haskell #Math
Formalization of Reynolds’s parametricity theorem in Coq. ~ Li-yao Xia. #ITP #Coq
How to think about types: Insights from a personal journey. ~ F. Pfenning. #Logic #Programming #CompSci
Good symbolic differentiation requires multidimensional wobbliness. ~ @Aearnus. #Haskell #Math
Do we need effects to get abstraction? ~ Eric Torreborre. #Haskell
Object oriented programming in Haskell. ~ Edsko de Vries. #Haskell
Catamorphisms and F-Algebras. ~ Alex Avramenko. #Haskell
Higher kinded option parsing. ~ Chris Penner. #Haskell
The algebra of algebraic data types, part 1. ~ Chris Taylor #Haskell
Lens as a divisibility relation: Goofin’ off with the algebra of types. ~ Philip Zucker. #Haskell
PageRank y el surfista aleatorio. ~ F. Sancho. #Algoritmos #IA
Making arrays mutable! ~ James Bowen. #Haskell #FunctionalProgramming
Interaction with formal mathematical documents in Isabelle/PIDE. ~ M. Wenzel. #ITP #IsabelleHOL
M1F, Imperial undergraduates, and Lean. ~ Kevin Buzzard. #ITP #LeanProver #Math
Functional programming is on the rise. ~ Roman Elizarov. #FunctionalProgramming
An interactive network graph showing the connections of programming languages based on their influences relations. ~ Ramiro Gómez. #Programming
Exámenes de programación funcional con Haskell. Vol. 7 (Curso 2015-16). #Haskell #ProgramaciónFuncional
Can neural networks learn symbolic rewriting? ~ B. Piotrowski, C Brown, J. Urban, C. Kaliszyk. #ATP #MachineLearning
Tactic learning for Coq. ~ L. Blaauwbroek. #ITP #Coq #MachineLearnig
Making set theory great again: The Naproche-SAD project. ~ S. Frerix, P. Koepke. #ITP #Math
Experiments with connection method provers. ~ W. Bibel, J. Otten. #ATP
An introduction to categories with Haskell and databases. ~ R. Holbrook. #CategoryTheory #Haskell #Databases
The power of functional programming. ~ Arvind Kumar GS. #FunctionalProgramming
Exámenes de programación funcional con Haskell. Vol. 8 (Curso 2016-17). #Haskell #ProgramaciónFuncional
Complexity-theoretic aspects of interactive proof systems. ~ Lance Jeremy Fortnow. #PhD_Thesis #ITP #ComputationalComplexity
Neural guidance for SAT solving. ~ S. Jaszczur, M. Łuszczyk, H. Michalewski. #ATP #SAT #MachineLearning
Using Isabelle/UTP for the verification of sorting algorithms (A case study). ~ J.A. Bockenek, P. Lammich, Y. Nemouchi, B. Wolff. #ITP #IsabelleHOL
Algebraic type theory and the gluing construction. ~ J. Sterling. #CompSci #TypeTheory
The subtle art of the mathematical conjecture. ~ R. Dijkgraaf. #Math
API constraints a’la carte in Haskell & PureScript. ~ R. Andersson. #Haskell #PureScript
¿Qué es un coconut? ~ Chema Cortés. #Coconut #FunctionalProgramming #Python
Coconut - Primeros pasos. ~ Chema Cortés. #Coconut #FunctionalProgramming #Python
Monadas con coco. ~ Chema Cortés. #Coconut #FunctionalProgramming #Python
Functional Programming Cheat Sheet. ~ Tony Morris. #FunctionalProgramming #Haskell
Some tricks for list manipulation. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
Transition to Haskell from Python: Iterator slicing. ~ Chris Martin, Julie Moronuki. #Python #Haskell
Transition to Haskell from Python: Iteration to infinity. ~ Chris Martin, Julie Moronuki. #Python #Haskell
Inline-JS: Seamless JavaScript/Haskell interop. ~ Shao Cheng. #Haskell #JavaScript
Exámenes de programación funcional con Haskell. Vol. 9 (Curso 2017-18). #Haskell #ProgramaciónFuncional
Understanding logic programming. #LogicProgramming #Python
SMT-based constraint answer set solver EZSMT+. ~ D. Shen, Y. Lierler. #ASP #CASP
Constructing trees from a distance matrix. ~ Guilherme Kunigami. #Algorithms
Alan Turing Institute releases ML framework written in Julia. #MachineLearning #JuliaLang
Exámenes de programación funcional con Haskell. Vol. 10 (Curso 2018-19). #Haskell #ProgramaciónFuncional
Teoría de la probabilidad: Lo mínimo. ~ F. Sancho. #Matemáticas
Making elections safe (A new proof that MAJORITY is not in AC⁰). ~ R.J. Lipton. #CompSci
Java is confusing, Clojure is simple. ~ Yehonathan Sharvit. #Programming #Java #Clojure
Introduction to functional programming with Python examples. ~ Radoslaw Fabisiak. #FunctionalProgramming #Python
Timeline of mathematics. #Math
Category theory and lambda calculus. ~ Mario Román García. #LambdaCalculus #CategoryTheory #Haskell
Mikrokosmos: a educational λ-calculus interpreter. ~ Mario Román García. #LambdaCalculus #Haskell
Formalization of asymptotic notations in HOL4. ~ N. Iqbal et als. #ITP #HOL4
A denotational engineering of programming languages. ~ Andrzej Jacek Blikle. #eBook #Logic #CompSci
Concatenative programming; the free monoid of programming languages. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
Interpreters with non-determinism using a free monad. ~ Casper Bach Poulsen. #Agda #Haskell
Milestones from the pure lisp theorem prover to ACL2. ~ J Strother Moore. #ITP #ACL2
I/O logic in HOL. ~ C- Benzmüller, A. Farjami, P. Meder, X. Parent. #ITP #IsabelleHOL #Logic
Quicksort with Haskell! ~ James Bowen. #Haskell #FunctionalProgramming
Integrated versus manual shrinking. ~ Edsko de Vries. #Haskell #FunctionalProgramming
Functor-Of. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming
Unifying semantic foundations for automated verification tools in Isabelle/UTP. ~ S. Foster et als. #ITP #IsabelleHOL
Formalization of generic authenticated data structures in Isabelle/HOL. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL
Lightweight, efficiently sampleable enumerations in Haskell. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Implicit corecursive queues. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
holpy: Interactive theorem proving in Python. ~ Bohua Zhan. #ITP #Logic #Python
GHC language extensions. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
Laws! ~ George Wilson. #Haskell #FunctionalProgramming
Appetite for dysfunction. ~ Andrew McMiddlin #Haskell #FunctionalProgramming
Reflexive art. ~ Sean Chalmers. #Haskell #FunctionalProgramming
Comma police: The design and implementation of a CSV library. ~ George Wilson. #Haskell #FunctionalProgramming
State machine testing. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
Contravariant functors: The other side of the coin. ~ George Wilson. #Haskell #FunctionalProgramming
Notions of computation as monoids. ~ E. Rivas, M. Jaskelioff. #Haskell #CategoryTheory
Graph theory in Coq: Minors, treewidth, and isomorphisms. ~ C. Doczkal, D. Pous. #ITP #Coq #Math
Cargo culting lenses for fun & profit. ~ Sean Chalmers. #Haskell #FunctionalProgramming
Your first Haskell app. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
Type class: The ultimate ad-hoc. ~ George Wilson. #Haskell #FunctionalProgramming
A note on the connections between the Foldable methods. ~ Daniel Mlot. #Haskell #FunctionalProgramming
Data science for fundamental sciences. Atabey Kaygun #DataScience
An app proof. R.J. Lipton. #Math
Techniques for embedding postfix languages in Haskell. ~ Chris Okasaki. #Haskell #FunctionalProgramming
Isabelle technology for the Archive of Formal Proofs. ~ Makarius Wenzel. #ITP #IsabelleHOL
La Geometría se hizo Arte: las claves secretas de Escher. ~ Antonio Pérez Sanz. #Matemáticas #Escher
A consistent foundation for Isabelle/HOL. ~ O. Kunčar, A. Popescu. #ITP #IsabelleHOL
Mechanised assurance cases with integrated formal methods in Isabelle. ~ Y. Nemouchi et als. #ITP #IsabelleHOL
Guiding theorem proving by recurrent neural networks. ~ B. Piotrowski, J. Urban. #ATP #NeuralNetworks
Purely functional games (How I built a game in Haskell - pure functional style). ~ Gil Mizrahi. #Haskell #FunctionalProgramming #Game
For cybersecurity, Computer Science must rely on strongly-typed actors. ~ C. Hewitt. #Logic #CompSci
Running from enemies! ~ James Bowen. #Haskell #FunctionalProgramming
A correspondence between deep/shallow embeddings and CPS/first order evaluators. ~ Matthew Chan. #Haskell #FunctionalProgramming
Thoughts on code style. ~ Matthew Chan. #Haskell #FunctionalProgramming
Parsing with derivatives in Haskell. ~ Timo Maarse. #Haskell #FunctionalProgramming
Lessons in functional API development from Haskell’s servant and Http4s. ~ James Santucci. #Haskell #FunctionalProgramming
Formalization and certification of software for smart cities. ~ E.S. Grilo, B. Lopes. #ITP #Coq
EduBAI: An educational platform for logic-based reasoning. ~ D. Arampatzis et als. #Teaching #Logic #ASP
Program design by calculation. ~ J.N. Oliveira. #eBook #Haskell #FunctionalProgramming
Learning Haskell language eBook. #eBook #Haskell #FunctionalProgramming
Competitive programming in Haskell: Scanner. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Profiling in Haskell for a 10x speedup. ~ Jake Zimmerman. #Haskell #FunctionalProgramming
Maybe catamorphism. ~ Mark Seemann. #Haskell #FunctionalProgramming
A formalization of forcing and the consistency of the failure of the continuum hypothesis. ~ Jesse Michael Han and Floris van Doorn. #ITP #LeanProver #Logic
Flypitch: A formal proof of the independence of the continuum hypothesis. ~ Jesse Michael Han and Floris van Doorn. #ITP #LeanProver #Logic
Learning to prove theorems via interacting with proof assistants. ~ K. Yang, J. Deng. #ITP #Coq #MachineLearning
CoqGym: A learning environment for theorem proving with the Coq proof assistant. ~ K. Yang, J. Deng. #ITP #Coq #MachineLearning
ENIGMAWatch: ProofWatch meets ENIGMA. ~ Z. Goertzel, J. Jakubův, J. Urban. #ATP #MachineLearnig
Faking fundeps with typechecker plugins. #Haskell #FunctionalProgramming
Applied category theory. ~ John D. Cook. #CategoryTheory
Equality part 1: definitional equality. ~ Kevin Buzzard. #ITP #LeanProver
Equality part 2: syntactic equality. ~ Kevin Buzzard. #ITP #LeanProver
Codata in action, or how to connect Functional Programming and Object Oriented Programming. ~ J. Casas. #Haskell #FunctionalProgramming #CategoryTheory
Dimensions and Haskell: Introduction. ~ D. Rogozin. #Haskell #FunctionalProgramming #MachineLearnig #Math
Graph representations for Higher-Order Logic and theorem proving. ~ A. Paliwal et als. #ITP #ATP #MachineLearning
Pie-hs: an implementation of Pie, the language from “The little typer”, in Haskell. ~ D.T. Christiansen. #Haskell #FunctionalProgramming
Smarter enemies with BFS! ~ James Bowen. #Haskell #FunctionalProgramming
A formally verified abstract account of Gödel’s incompleteness theorems. ~ A. Popescu, D. Traytel. #ITP #IsabelleHOL #Logic #Math
Generic authenticated data structures, formally. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL
Learning to reason in large theories without imitation. ~ K. Bansal et als. #ATP #MachineLearning
Toychain: Formally verified blockchain consensus. ~ G. Pîrlea. #ITP #Coq #Blockchain
Programming with applicative-like expressions. ~ J. Malakhovski, S. Soloviev. #Haskell #FunctionalProgramming
Deriving a linear-time applicative traversal of a rose tree. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
CYP: Checker for “morally correct” induction proofs about Haskell programs. #ITP #Haskell #FunctionalProgramming
Naïve type theory. ~ T. Altenkirch. #Logic #Math #TypeTheory #HoTT
La théorie de la complexité algorithmique pour calculer efficacement. ~ G. Lagarde #Algorithmes
SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver. ~ P.W. Wang et als. #ATP #SAT #MachineLearning
Towards finding longer proofs. ~ Z. Zombori et als. #ATP #MachineLearning
Liquidate your assets (Reasoning about resource usage in Liquid Haskell). ~ M.A.T. Handley, N. Vazou, G. Hutton. #Haskell #LiquidHaskell
String interpolation and overlapping instances. ~ William Yao. #Haskell #FunctionalProgramming
Sobre cribas y matemáticas. ~ Juan Arias de Reyna. #Matemáticas

Junio 2019

Sheldon tenía razón: el mejor número es el 73. ~ M.A. Morales. #Matemáticas
A verified implementation of the Berlekamp–Zassenhaus factorization algorithm. ~ J. Divasón et als. #ITP #IsabelleHOL #Math
First semester in numerical analysis with Julia. ~ G. Ökten. #eBook #JuliaLang #Math
Why Haskell - why GitHub use Haskell for their newly released Semantic package. #Haskell #FunctionalProgramming
Multidimensional binary search trees in Isabelle/HOL. ~ Martin Rau. #ITP #IsabelleHOL
Towards automated reasoning in Herbrand structures. ~ L. Cohen, R. Rowe, Y. Zohar. #Logic #ATP
Generating random structurally rich algebraic data type values. ~ A. Mista, A. Russo. #Haskell #FunctionalProgramming
Monday Morning Haskell: Fighting Back! ~ James Bowen. #Haskell #FunctionalProgramming
Reference of basic commands to get comfortable with OCaml. ~ Musa Al-hassy. #OCaml
Translation from problem to code in seven steps. ~ A.D. Hilton, G.M. Lipp, S.H. Rodger. #Teaching #Programming
Refinement with time (Refining the run-time of algorithms in Isabelle/HOL). ~ M.P.L. Haslbeck, P. Lammich. #ITP #IsabelleHOL
Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. ~ Enrico Tassi. #ITP #Coq
Higher-order Tarski Grothendieck as a foundation for formal proof. ~ C. Brown, C. Kaliszyk, K. Pąk. #ITP #IsabelleHOL #Logic
A certifying extraction with time bounds from Coq to call-by-value λ-calculus. ~ Y. Forster, F. Kunze. #ITP #Coq
Formal proof of Tarjan’s strongly connected components algorithm in Why3, Coq, and Isabelle. ~ R. Chen et als. #ITP #Why3 #Coq #IsabelleHOL
Formalizing computability theory via partial recursive functions. ~ M. Carneiro. #ITP #LeanProver
Property-based testing in a screencast editor, case study 3: Integration testing. ~ Oskar Wickström. #Haskell #FunctionalProgramming
Either catamorphism. Mark Seemann. #Haskell #FunctionalProgramming
Haskell style guide. ~ Johan Tibell. #Haskell #FunctionalProgramming
Solving programming puzzles without using your brain. ~ Donnacha Oisín Kidney. #Python #Math
Formalizing the solution to the cap set problem. ~ S. Dahmen, J. Hölzl, R.Y. Lewis. #ITP #LeanProver
Quantitative continuity and computable analysis in Coq. ~ F. Steinberg, L. Thery, H. Thies. #ITP #Coq #Math
Hilbert meets Isabelle. (Formalisation of the DPRM theorem in Isabelle/HOL). ~ D. Aryal et als. #ITP #IsabelleHOL #Math
A certificate-based approach to formally verified approximations. ~ F. Bréhard, A. Mahboubi, D. Pous. #ITP #Coq #Math
Proving tree algorithms for succinct data structures. ~ R. Affeldt, J. Garrigue, X. Qi, K. Tanaka. #ITP #Coq
Automatic refactoring for Agda. ~ K. Wibergh. #Msc_Thesis #ITP #Agda
LP based integration of computing and science education in middle schools. ~ Y. Zhang et als. #Teaching #LogicProgramming
Functional programming for Web and mobile (A review of the current state of the art). ~ J. Wälter. #FunctionalProgramming
A role for dependent types in Haskell (Extended version). ~ S. Weirich et als. #Haskell #FunctionalProgramming
Formalization of the axiom of choice and its equivalent theorems. ~ T. Sun, W. Yu. #ITP #Coq #Logic #Math
Formalization of axiomatic set theory in Coq. #ITP #Coq #Logic #Math
Formalization of the axiom of choice and its equivalent theorems in Coq. ~ T. Sun. #ITP #Coq #Logic #Math
TeIL: a type-safe imperative tensor intermediate language. ~ N.A. Rink, J. Castrillon. #ITP #Coq
Rapid prototyping formal systems in MMT: 5 case studies. ~ D. Müller, F. Rabe. #ITP #MMT #Logic
Exploring semantic hierarchies to improve resolution theorem proving on ontologies. ~ S. Small. #ATP #Prover9
Pure programs: Pure functions aren’t enough. ~ Ryan Newton. #Haskell #FunctionalProgramming
Spring cleaning: Parameters and saving!. #Haskell #FunctionalProgramming
Inductive logic programming via differentiable deep neural logic networks. ~ A. Payani, F. Fekri. #ILP #NeuralNetworks #MachineLearning
Relay: A high-level IR for Deep Learning. ~ J. Roesch et als. #FunctionalProgramming #MachineLearning
The inverse of a bijection. ~ Kevin Buzzard. #ITP #LeanProver #Math
A practical introduction to freer monads (Eff). #Haskell #FunctionalProgramming
Functional programming in OCaml. ~ Michael R. Clarkson. #eBook #FunctionalProgramming #OCaml
A verified ODE solver and Smale’s 14th problem. ~ F. Immler. #PhD_Thesis #ITP #IsabelleHOL #Math
An Isabelle/HOL formalisation of Green’s theorem. ~ M. Abdulaziz, L.C. Paulson. #ITP #IsabelleHOL #Math
Formally verified algorithms for upper-bounding state space diameters. ~ M. Abdulaziz, M. Norrish, C. Gretton. #ITP #HOL4
A formally verified validator for classical planning problems and solutions. ~ M. Abdulaziz, P. Lammich. #ITP #IsabelleHOL
A tutorial introduction to structured Isar proofs. ~ T. Nipkow. #ITP #IsabelleHOL
Permutations and permutation groups in Common Lisp. ~ Robert Smith. #CommonLisp #Math
Cultures of programming (Understanding the history of programming through controversies and technical artifacts). ~ T. Petricek, #Programming
Truth and justification in knowledge representation. ~ A. Rodin, S. Kovalyov. #KR #HoTT
Binary heaps for IMP2 in Isabelle/HOL. ~ S. Griebel. #ITP #IsabelleHOL
Exercises on generalizing the induction hypothesis. ~ James Wilcox. #ITP #Coq
Monoid. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming
Empty and unit types. ~ Ashley Yakeley. #Haskell #FunctionalProgramming #TypeTheory
Free monads of free monads. ~ Li-yao Xia. #Haskell #FunctionalProgramming
hsp: Haskell command line text stream processor. #Haskell #FunctionalProgramming
Proofs are not programs. ~ Kevin Buzzard. #ITP #LeanProver #Math
CrystalBall: SAT solving, data gathering, and machine learning. ~ Mate Soos. #SAT #MachineLearning
Teaching the art of functional programming using automated grading (Experience report). ~ A. Hameer, B. Pientka. #Teaching #FunctionalProgramming #OCaml
Learn-OCaml: A Web application for learning OCaml. #Teaching #FunctionalProgramming #OCaml
Selective applicative functors. ~ Andrey Mokhov. [Slides] #Haskell #FunctionalProgramming
Composing monads for a musical performance. ~ N. Rossiter, M. Heather. #Music #CategoryTheory #Haskell
Higher-order type-level programming in Haskell. ~ C. Kiss et als. #Haskell #FunctionalProgramming
Developing an intuition for reduce in JavaScript through Haskell: Monoids. ~ @codefornerds #JavaScript #Haskell #FunctionalProgramming
Parsing typed eDSL. ~ George Agapov. #Haskell #FunctionalProgramming
Haskell quick syntax reference. ~ S.L. Nita, M. Mihailescu. #eBook #Haskell #FunctionalProgramming
Effective problem solving using SAT solvers. ~ C. Bright et als. #ATP #SAT
The Isabelle cookbook (A gentle tutorial for programming Isabelle/ML). ~ C. Urban et als. #ITP #IsabelleHOL
Gröbner bases and Macaulay matrices in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
Formalization of Dubé’s degree bounds for Gröbner bases in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
Gröbner bases, Macaulay matrices and Dubé’s degree bounds in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
Hilbert’s Nullstellensatz in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL
Formal verification of boolean unification algorithms with Coq. ~ D. Richardson et als. #ITP #Coq
Introduction to homotopy type theory. ~ E. Rijke. #HoTT #Logic #math #ITP #Agda
Monte Carlo tableau proof search. ~ M. Färber, C. Kaliszyk, J. Urban. #ATP #Logic #MachineLearning
Authenticated data structures, generically. #Haskell #FunctionalProgramming
Loading games and changing colors! ~ James Bowen #Haskell #FunctionalProgramming
Patterns of functional programming: functional core - imperative shell. ~ J. Casas. #Haskell #FunctionalProgramming
A taste of functional programming in Kotlin. ~ Baseer Al-Obaidy. #FunctionalProgramming #Kotlin
The Functor Combinatorpedia. ~ Justin Le. #Haskell #FunctionalProgramming
The functional programming toolkit. ~ Scott Wlaschin. #FunctionalProgramming
The power of composition (for beginners in FP). ~ Scott Wlaschin. #FunctionalProgramming #Fsharp
Functional design patterns. ~ Scott Wlaschin. #FunctionalProgramming #Fsharp
Implementing recursion with the Y combinator in any language. ~ Michele Riva. #LambdaCalculus #JavaScript #Haskell #Java #Racket #Python #C
UserLAnd: The easiest way to run a Linux distribution or application on Android. #Linux #Android
An interactive way to C. ~ Musa Al-hassy. #Programming #C #Emacs #Org_mode
Presenting the Eshell. ~ Howard Abrams. #Emacs
String interpolation and overlapping instances. ~ William Yao. #Haskell #FunctionalProgramming
Count-Min sketch in Haskell. ~ Victor Adossi. #Haskell #FunctionalProgramming
An opinionated beginner’s guide to Haskell in mid 2019. ~ Varun Gandhi. #Haskell #FunctionalProgramming
foldr under the hood. ~ Neil Mitchell. #Haskell #FunctionalProgramming
Transition to Haskell from Python: Zipping. ~ Chris Martin, Julie Moronuki. #Python #Haskell
Theorema-HOL: Classical Higher-Order Logic in Theorema. ~ A. Maletzky. #ITP #TheoremaHOL
An introduction to Copilot. ~ F. Dedden et als. #Haskell #FunctionalProgramming
Neural theorem provers do not learn rules without exploration. ~ M. de Jong, F. Sha. #ATP #MachineLearning
Linear inequalities in Isabelle/HOL. ~ R. Bottesch, A. Reynaud, R. Thiemann. #ITP #IsabelleHOL #Math
Verifying fold using Monoids in Coq. ~ Dalton Lundy. #ITP #Coq #FunctionalProgramming
Lessons learned while writing a Haskell application. ~ G. Volpe. #Haskell #FunctionalProgramming
An efficient implementation of Galois fields. ~ Stephen Diehl. #Haskell #FunctionalProgramming #Math
A brief guide to a few algebraic structures. ~ Julie Moronuki. #Math #Haskell #FunctionalProgramming
Why I (as of June 22 2019) think Haskell is the best general purpose language (as of June 22 2019). ~ Philip Zucker. #Haskell #FunctionalProgramming
What is a programmable programming language? ~ A. Sanchez. #Programming #Lisp
Introducción a la programación en Julia. ~ Mauricio M. Tejada. #JuliaLang
A mathematical proof isn’t just an intellectual exercise. ~ D. Holland. #Math
En busca de una nueva definición para la inteligencia de las máquinas. ~ Luis Ignacio Hojas Hojas. #IA
Differential game logic in Isabelle/HOL. ~ André Platzer. #ITP #IsabelleHOL
Taking a shortcut! ~ James Bowen. #Haskell #FunctionalProgramming
Python and Emacs Pt. 1. ~ Jonathan Bennett. #Emacs #Python
LiFtEr: Language to encode induction heuristics for Isabelle/HOL. ~ Y. Nagashima. #ITP #IsabelleHOL
A framework for specifying and formally verifying application security policies. ~ C. Shao. #Msc_Thesis #ITP #Coq
On roots of polynomials over F(X)/<p>. ~ C. Schwarzweller. #ITP #Mizar #Math
AI safety as a PL problem. ~ Swarat Chaudhuri. #AI #FormalVerification #MachineLearning
Transition to Haskell from Python: Data classes. ~ Chris Martin , Julie Moronuki. #Python #Haskell
Implement with types, not your brain! #Haskell #FunctionalProgramming
Evaluación de implementaciones alternativas de colas concurrentes en Haskell. ~ T.A: González. #Haskell
Call-by-need is clairvoyant call-by-value. ~ J. Hackett, G. Hutton. #FunctionalProgramming
Elisp reference sheet (Quick reference to the core language of Emacs). ~ Musa Al-hassy. #Programminf #Lisp #Elisp #Emacs
Gerwin’s style guide for Isabelle/HOL. Part 1: Good proofs. ~ Gerwin Klein. #ITP #IsabelleHOL
Gerwin’s style guide for Isabelle/HOL. Part 2: Good style. ~ Gerwin Klein. #ITP #IsabelleHOL
Course: Advanced topics in software verification. ~ Gerwin Klein, June Andronick, Christine Rizkallah, Miki Tanaka. #ITP #IsabelleHOL
CPP considered harmful. ~ Mathieu Boespflug. #Haskell #FunctionalProgramming
The tragedy of the Common Lisp: Why large languages explode. ~ Mark Miller. #Programming
Toward artificial intelligence that learns to write code. ~ K. Martineau. #Programming #AI #DeepLearning
Learning to infer program sketches. ~ M. Nye et als. #Programming #AI #DeepLearning
How to specify it! (A guide to writing properties of pure functions). ~ John Hughes. #Haskell #FunctionalProgramming
Gen: A general-purpose probabilistic programming system with programmable inference. ~ M.F. Cusumano-Towner et als. #AI #JuliaLang
Priority search trees im Isabelle/HOL. ~ P. Lammich, T. Nipkow. #ITP #IsabelleHOL
Purely functional, simple, and efficient implementation of Prim and Dijkstra in Isabelle/HOL. ~ P. Lammich, T. Nipkow. #ITP #IsabelleHOL
Complete non-orders and fixed points in Isabelle/HOL. ~ A. Yamada, and J. Dubut. #ITP #IsabelleHOL
Mathematical method and proof. ~ Jeremy Avigad. #ITP #IsabelleHOL #Logic #Math
A Julia set generator. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming

Julio 2019

Bar-Hillel theorem mechanization in Coq. ~ S. Bozhko, L. Khatbullina, S.Grigorev. #ITP #Coq
Jupyter adaptation of “Learn you a Haskell for great good!” ~ James Brock. #Haskell #FunctionalProgramming #Jupyter
Property-based testing. ~ J. Fowler. #PhD_Thesis #Haskell #FunctionalProgramming
An introduction to computer science research: selected papers with commentary. ~ Camille Akmut. #CompSci
Formal proof and analysis of an incremental cycle detection algorithm. ~ A. Guéneau, J.H. Jourdan, A. Charguéraud, F. Pottier. #ITP #Coq
Formal verification of memory preservation of x86-64 binaries. ~ J.A. Bockenek, F. Verbeek, P. Lammich, B. Ravindran. #ITP #IsabelleHOL
Monday Morning Haskell: Gloss review! ~ James Bowen. #Haskell #FunctionalProgramming
Secure compilation. ~ C. Hritcu et als. #Programming
The Ramanujan machine: Automatically generated conjectures on fundamental constants. ~ G. Raayoni et als. #MachineLearning #Math
Proving tree algorithms for succinct data structures. ~ R. Affeldt, J. Garrigue, X. Qi, K. Tanaka. #ITP #Coq
Formalizing the solution to the cap set problem. ~ S.R. Dahmen, J. Hölzl, R.Y. Lewis. #ITP #LeanProver
Various new theorems in constructive univalent mathematics written in Agda. ~ Martin Escardo. #ITP #Agda #Math
On solving word equations using SAT. ~ Joel D. Day et als. #ATP #SAT
A story told by type errors. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
10 days of neural networks in Haskell. Bogdan Penkovsky. #Haskell #FunctionalProgramming #NeuralNetworks
A taste of type theory. ~ Bartosz Milewski. #TypeTheory #FunctionalProgramming
Neural network verification for the masses (of AI graduates). ~ E. Komendantskaya et als. #AI #Verification #ITP #Coq #ATP #SMT #Z3 #NeuralNetworks
Formalization of a monitoring algorithm for metric first-order temporal logic. ~ J. Schneider, D. Traytel. #ITP #IsabelleHOL #Logic
Proving for Fun: July 2019. #ITP #IsabelleHOL #Coq
Formalization of Rice’s theorem over a functional language model. ~ T.M.F. Ramos, A.A- Almeida, M. Ayala-Rincón. #ITP #PVS
Improving Haskell. ~ M.A.T. Handley, G. Hutton. #Haskell #FunctionalProgramming
Lightweight invertible enumerations in Haskell. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Coding with asymmetric numeral systems. ~ J. Gibbons. #Haskell #FunctionalProgramming
Learn Haskell to be a better programmer. ~ Kwang Yul Seo. #Haskell #FunctionalProgramming
Cutting through the smog: making an air quality bot with Haskell. ~ A. Moreno. #Haskell #FunctionalProgramming
Microsmos: Writing a simple tree-editor with brick. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
Examples and results from a BSc-level course on domain specific languages of mathematics. ~ P. Jansson, S.H. Einarsdóttir, C. Ionescu. #Haskell #FunctionalProgramming #Math
Generic diffing and merging of mutually recursive datatypes in Haskell. ~ A. van Putten. #Msc_Thesis #Haskell #FunctionalProgramming
S Stands for Shock: The European funders’ proposal for Open Access. ~ Jeremy Gibbons.
Abstraction and subsumption in modular verification of C programs. ~ A.W. Appel, L. Beringer. #ITP #Coq
Separation-logic-based program verification in Coq. ~ Qinxiang Cao. #PhD_Thesis #ITP #Coq
A computer-generated proof that nobody understands. ~ Kevin Buzzard. #ATP #Math
Write you a Haskell (Building a modern functional compiler from first principles). ~ Stephen Diehl. #Haskell #FunctionalProgramming
A continuation of Stephen Diehl’s “Write you a Haskell”. #Haskell #FunctionalProgramming
Lemma discovery for induction: A survey. ~ Moa Johansson. #Haskell
From LCF to Isabelle/HOL. ~ L.C. Paulson, T. Nipkow, M. Wenzel. #ITP #IsabelleHOL
Domain-specific language to encode induction heuristics. ~ Yutaka Nagashima. #ITP #IsabelleHOL
Preparing for simulation: Player AI. ~ James Bowen. #Haskell #FunctionalProgramming
Scripting in Haskell and PureScript. ~ Riccardo Odone. #Haskell #PureScript
A formal proof of the termination of Zielonka’s algorithm for solving parity games. ~ R. Abraham. #ITP #IsabelleHOL
Mechanizing Principia Logico-Metaphysica in functional type theory. ~ D. Kirchner, C. Benzmüller, E.N. Zalta. #ITP #IsabelleHOL
Dependently-typed Montague semantics in the proof assistant Agda-flat. ~ C. Zwanziger. #ITP #Agda
I/O logic in HOL. ~ C. Benzmüller, A. Farjami, P. Meder, X. Parent. #ITP #IsabelleHOL
SAT solvers and computer algebra systems: A powerful combination for mathematics. ~ C. Bright, I. Kotsireas, V. Ganesh. #SAT #CAS #Math
Open Sum Types in Haskell with world-peace. ~ Dennis Gosnell (Dennis Gosnell). #Haskell #FunctionalProgramming
Trees as monads. ~ Dimitrios Kalemis. #Haskell #FunctionalProgramming
Lambda calculus. ~ Ben Lynn. #LambdaCalculus #Haskell #FunctionalProgramming
REBA: A refinement-based architecture for knowledge representation and reasoning in robotics. ~ M. Sridharan, M. Gelfond, S. Zhang, J. Wyatt. #AI #KRR #ASP
Dependency learning for QBF. ~ T. Peitl, F. Slivovsky, S. Szeider. #AI
My first fifteen compilers. ~ Lindsey Kuper. #Programming #Compilers #Nanopass
A verified compiler from Isabelle/HOL to CakeML. ~ L. Hupel, T. Nipkow. #ITP #Isabelle/HOL
Multi stage programming in context. ~ M. Pickering, N. Wu, C. Kiss. #Haskell #FunctionalProgramming
Working with source plugins. ~ M. Pickering, N. Wu, B. Németh. #Haskell #FunctionalProgramming
Trustworthy graph algorithms. ~ M. Abdulaziz, K. Mehlhorn, T. Nipkow. #ITP #IsabelleHOL
Certified semantics for miniKanren. ~ D. Rozplokhas, A. Vyatkin, D. Boulytchev. #ITP #Coq
(Co) inductive proof systems for compositional proofs in reachability logic. ~ V. Rusu, D. Nowak. #ITP #IsabelleHOL #Coq
Gradual typing from theory to practice. ~ Sam Tobin-Hochstadt. #Programming
Walker: Automated assessment of Haskell code using syntax tree analysis. ~ R.H. de Vries. #Haskell #FunctionalProgramming
BioShake: a Haskell EDSL for bioinformatics workflows. ~ J. Bedő. #Haskell #FunctionalProgramming
Music as language (Putting probabilistic temporal graph grammars to good use). ~ O. Melkonian #Haskell #FunctionalProgramming #Music
A bridge anchored on both sides: Formal deduction in introductory CS, and code proofs in discrete math. ~ D.G. Wonnacott, P.M. Osera. #Logic #Math #ITP #Coq #Haskell
Experimental evaluation of formal software development using dependently typed languages. ~ F. Tamasi. #ITP #Coq #Agda
Evaluation of function calls in Haskell. ~ Laszlo Treszkai. #Haskell #FunctionalProgramming
Automatically and efficiently illustrating polynomial equalities in Agda. ~ Donnacha Oisín Kidney. #Bachelor_Thesis #ITP #Agda
Building and debugging FRP with CodeWorld and Reflex. ~ Chris Smith. #Haskell #CodeWorld
El zen de Python: Explicado y con ejemplos. ~ Javier Daza. #Programación #Python
A brief analysis of “The zen of Python”. ~ Jonathan Hammond #Programming #Python
Genetic algorithms as shrinkers in property-based testing. ~ F.Y. Lo, C.H. Chen, Y. Chen. #ITP #Coq
Julia’s efficient algorithm for subtyping unions and covariant tuples. ~ B Chung, F. Zappa Nardelli, J. Vitek. #ITP #Coq #JuliaLang
Closure conversion is safe for space. ~ Z. Paraskevopoulou, A.W. Appel. #ITP #Coq
Advanced search with drilling! ~ James Bowen. #Haskell #FunctionalProgramming
Writing a PhD thesis with Org Mode. ~ Daniel Gomez. #Emacs #Org_mode
Writing a Ph.D. thesis with Org Mode (emplate repository). ~ Daniel Gomez. #Emacs #Org_mode
ebib: A BibTeX database manager for Emacs. #Emacs #LaTeX
Summer reading in theory. R.J. Lipton, K.W. Regan. #CompSci
Revelations from repetition: Source code headers in Haskell and Python. ~ S. Carstens, M. Meschede. #Haskell #Python
Una interesante introducción a la lógica difusa. ~ Carlos Bejines. #Lógica #Matemáticas
A sequent calculus for first-order logic in Isabelle/HOL. ~ Andreas Halkjær From. #ITP #IsabelleHOL
Formal verification of trading in financial markets. #ITP #Coq
Decompose ContT. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming
Dimensions and Haskell: Singletons in action. ~ R. Stryungis, D. Rogozin. #Haskell #FunctionalProgramming
Elements of functional programming in Python. ~ Parul Pandey. #Python #FunctionalProgramming
Hybrid relations in Isabelle/UTP. ~ S.D. Foster. #ITP #IsabelleHOL
Formal verification of quantum algorithms using quantum Hoare logic. ~ J. Liu et als. #ITP #IsabelleHOL
Towards a verified model of the Algorand consensus protocol in Coq. ~ M.A. Alturki, J. Chen, V. Luchangco, B. Moore. #ITP #Coq
A certified functional nominal C-unification. ~ M. Ayala-Rincón et als. #ITP #PVS
A predicate transformer semantics for effects (Functional pearl). ~ W. Swierstra, T. Baanen. #ITP #Agda
Kind inference for datatypes. ~ N. Xie, R.A. Eisenberg, B.C.D.S. Oliveira. #Haskell #FunctionalProgramming
Generic enumerators. ~ C. van der Rest, W. Swierstra, M. Chakravarty. #Haskell #FunctionalProgramming
Haskell I/O tutorial. ~ Albert Y. C. Lai. #Haskell #FunctionalProgramming
Mathematical proof of algorithm correctness and efficiency. ~ Vladimir Batoćanin. #CompSci #Algorithms
A curious associativity of the <$> operator. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming
Analyzing our parameters. ~ James Bowen #Haskell #FunctionalProgramming
Insane in the Membrain. ~ Veronika Romashkina. #Haskell #FunctionalProgramming
Rediscovering constructive type theory with Cedille. ~ Aaron Stump. #Haskell #Cedille
Making it easier to program and protect the Web. #CompSci
“Programming Algorithms” Book. ~ Vsevolod Dyomkin. #Programming #Lisp #Algorithms
How to use Binder and Python for reproducible research. ~ Erik Marsja. #Binder #Docker #Jupyter #Python
Generating correctness proofs with neural networks. ~ A. Sanchez-Stern et als. #ITP #NeuralNetworks
Towards a smart contract verification framework in Coq. ~ D. Annenkov, B. Spitters. #ITP #Coq
Building a blog in Haskell with Yesod–using a database. ~ R. Odone. #Haskell #FunctionalProgramming
Euclidean rhythms and Haskell. ~ Erich Grunewald. #Haskell #FunctionalProgramming
A weekend replication of STOKE, a stochastic superoptimiser. #Haskell #FunctionalProgramming
Haskell Dockerfile linter: A smarter Dockerfile linter that helps you build best practice Docker images. #Docker #Haskell #FunctionalProgramming
In praise of strong FP. ~ Aaron Stump. #FunctionalProgramming
Fast polynomial arithmetic in Haskell. #Haskell #FunctionalProgramming
The AI metamorphosis. ~ Henry A. Kissinger, Eric Schmidt, Daniel Huttenlocher. #AI
Langages des maths, langages de l’informatique. #Math #CompSi
Decades-old computer science conjecture solved in two pages. ~ Erica Klarreich. #Math #CompSci
Coq Coq Codet! (Towards a Verified Toolchain for Coq in MetaCoq). ~ M. Sozeau et als. #ITP #Coq
Formalization of the MRDP theorem in the Mizar system. ~ K. Pąk. #ITP #Mizar #Math
Partial correctness of a factorial algorithm. ~ A. Jaszczak, A. Korniłowicz. #ITP #Mizar
Natural addition of ordinals. ~ S. Koch. #ITP #Mizar #Math
Modular effects in Haskell through effect polymorphism and explicit dictionary applications. ~ D. Devriese. #Haskell #FunctionalProgramming
idris-ct: A library to do category theory in Idris. ~ F. Genovese et als.. #Idris #CategoryTheory
Szpilrajn extension theorem in Isabelle/HOL. ~ P. Zeller. #ITP #IsabelleHOL #Math
Fibonacci formalized 1: some sums. ~ Bryan Gin-ge Chen. #ITP #LeanProver #Math
Generating castles for Minecraft using Haskell. ~ Tim Philip Williams. #Haskell #FunctionalProgramming
Cursors, part 6: The forest cursor. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
Testing bipartiteness with monad transformers. ~ Vasily Alferov. #Haskell #FunctionalProgramming
Solving a puzzle in Haskell. ~ Chris Smith. #Haskell #FunctionalProgramming #CodeWorld
The power of RecordWildCards. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
Programming algorithms: A crash course in Lisp. ~ Vsevolod Dyomkin. #CommonLisp
Formalizing extended UTxO and BitML calculus in Agda. ~ O Melkonian. #ITP #Agda
Extensional higher-order paramodulation in Leo-III. ~ A. Steen, C. Benzmüller. #ITP #Leo_III
Functional programming in Scala. ~ P. Chiusano, R. Bjarnason. #eBook #FunctionalProgramming #Scala
Attack trees in Isabelle. ~ F. Kammüller. #ITP #IsabelleHOL
Introducing the Haskell Phrasebook. ~ Chris Martin. #Haskell #FunctionalProgramming
The Haskell Phrasebook. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming
Arithmetic on algebraic data types. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming #Math
Julia: come for the syntax, stay for the speed. ~ J.M. Perkel. #Programming #JuliaLang
Les algorithmes du nouveau lycée technologique, en Python. ~ Alain Busser. #Programming #Python

Agosto 2019

A formal development of a polychronous polytimed coordination language. ~ H. Nguyen Van, F. Boulanger, B. Wolff. #ITP #IsabelleHOL
A verified LL(1) parser generator. ~ S. Lasser et als. #ITP #Coq
Verifying effectful Haskell programs in Coq. ~ J. Christiansen, S. Dylus, N. Bunkenburg. #ITP #Coq #Haskell
Client-side web programming in Haskell: A retrospective ~ Chris Done. #Haskell #FunctionalProgramming
Practical event driven & sourced programs in Haskell. ~ Adam Piper. #Haskell #FunctionalProgramming
Haskell: A functional love story. ~ Ilya Peresadin. #Haskell #FunctionalProgramming
Solving planning problems with Fast Downward and Haskell. ~ Ollie Charles. #Haskell #AI
Code line patterns: Creating maps of Stackage and PyPi. ~ Simeon Carstens, Matthias Meschede. #Haskell #Python
Los intereses comerciales marcan el futuro de la inteligencia artificial. ~ Javier Salas. #IA
IMO 2019 Q1. ~ Kevin Buzzard. #ITP #LeanProver #Math
Exploring cloud builds in Hadrian. ~ David Eichmann. #Haskell
Program synthesis in 2019. ~ James Bornholt. #ProgramSynthesis #FormalVerification #ATP
Considering the order of results when computing Cartesian product. ~ Dominic Orchard. #Haskell #FunctionalProgramming
Formalising Mathematics-in praxis; A mathematician’s very first experiences with Isabelle/HOL. ~ A. Koutsoukou-Argyraki. #ITP #IsabelleHOL #Math
Engineering formal systems in constructive type theory. ~ S. Chafar. #PhD_Thesis #ITP #Coq
Lazy stream programming in Prolog. ~ P- Tarau, J. Wielemaker, T. Schrijvers. #Prolog #LogicProgramming
Optimized Docker builds for Haskell Stack. ~ Tim Spence. #Haskell #Docker
Comparing verification of list functions in LiquidHaskell and Idris. ~ A. Westerberg, G. Ung. #Haskell #LiquidHaskell #Idris #FunctionalProgramming
Dos debates sobre la inteligencia artificial. ~ Javier Sampedro. #IA
China has started a grand experiment in AI education. It could reshape how the world learns. ~ Noah Sheldon. #AI #Education
Equations reloaded (high-level dependently-typed functional programming and proving in Coq). ~ M. Sozeau, C. Mangin. #ITP #Coq
Higher-order type-level programming in Haskell. ~ C. Kiss, T. Field, S. Eisenbach, S. Peyton Jones. #Haskell #FunctionalProgramming
Functional DevOps in a Dysfunctional World. ~ Vaibhav Sagar. #Haskell #Nix
Survey of category theory in Coq. #ITP #Coq #Math
Using the Accelerate library to implement Chebyshev functions. #Haskell #FunctionalProgramming #Math
Functional Blockchain Contracts. ~ Manuel Chakravarty. #Haskell #Blockchain
Exercises in programming style: FP & I/O. ~ Nicolas Fränkel. #Programming
Programming algorithms: Data structures. ~ Vsevolod Dyomkin. #Programming #Lisp #Algorithms
Why Emacs. ~ Kasim Tuman. #Emacs
Selected problems from the International Mathematical Olympiad 2019 in Isabelle/HOL. ~ Manuel Eberl. #ITP #IsabelleHOL #Math
Moving towards ML: Evaluation functions. ~ James Bowen. #Haskell #FunctionalProgramming
Building a better brain. ~ James Bowen. #Haskell #FunctionalProgramming
Communicating concurrent Kleene algebra for distributed systems specification. ~ Maxime Buyse. #AFP #ITP #IsabelleHOL #Math
Verifying finality for Blockchain systems. ~ Karl Palmskog et als. #ITP #Coq #Blockchain
10 years seL4: Still the best, still getting better. ~ Gernot Heiser. #ITP #IsabelleHOL
A Haskell implementation of Conway’s Game of Life, viewable on the console, no external libs. #Haskell #FunctionalProgramming
Formally justified and modular Bayesian inference for probabilistic programs. ~ Adam Michał Ścibior. #PhD_Thesis #Haskell #FunctionalProgramming
Una implementación en Haskell de un lenguaje funcional no determinista. ~ Manuel Velasco Suárez. #TFG #Haskell #FunctionalProgramming
A formally verified HOL algebra for dynamic reliability block diagrams. ~ Y. Elderhalli, O. Hasan, S. Tahar. #ITP #HOL4
What does it mean for a program analysis to be sound? ~ Ilya Sergey. | SIGPLAN Blog #CompSci #Program_analysis
How Monoids are useful in programming? ~ @tsoding #Haskell
Dead-simple TCP/IP services using servant. ~ Justin Le. #Haskell #I1M2016
Polysemy is fun! - Part 2. ~ Raghu Kaippully. #Haskell #FunctionalProgramming
The Ramanujan Machine: Automatically generated conjectures on fundamental constants. ~ Gal Raayoni et als. #MachineLearning #Math
The Ramanujan Machine: Using algorithms to discover new mathematics. #MachineLearning #Math
Monte Carlo Tree Search in NetLogo. ~ F. Sancho. #NetLogo #IA
Dependently typed Haskell in industry (experience report). ~ David Thrane Christiansen et als. #Haskell #FunctionalProgramming
Practical profunctor lenses & optics in PureScript. ~ Thomas Honeyman. #PureScript
Prolog coding guidelines: Status and tool support. ~ F. Nogatz, P. Körner, S. Krings. #Prolog #LogicProgramming
Ten simple rules for writing and sharing computational analyses in Jupyter Notebooks. ~ A. Rule et als. #OpenScience #Jupyter
Building Haskell Apps with Docker. ~ Deni Bertovic . #Haskell #Docker
Basic text processing in functional style. ~ Vitaly Bragilevsky. #Haskell #FunctionalProgramming
Intro to Web Prolog for erlangers. ~ T. Lager #Prolog #LogicProgramming
Building a blog in Haskell with Yesod–Returning JSON. ~ Riccardo Odone #Haskell
Learn more programming languages, even if you won’t use them. ~ Thorsten Ball #Programming
Programming algorithms: Arrays. #Programming #CommonLisp
After Math: (Re)configuring minds, proof, and computing in the postwar United States. ~ Stephanie Aleen Dick. #PhD_Thesis #ATP #Logic #Math
Pearl: How to do proofs? (Practically proving properties about effectful programs’ results). ~ K. Jacobs, A. Nuyts, D. Devriese. #ITP #Agda #FunctionalProgramming
Deep Learning: A philosophical introduction. ~ C. Buckner. #DeepLearning
pretty-simple: pretty-printer for Haskell data types that have a Show instance. ~ Dennis Gosnell. #Haskell #FunctionalProgramming
An introduction to declarative programming in CLIPS and Prolog. ~ J.L. Watkin, A.C. Volk, S. Perugini. #DeclarativeProgramming #CLIPS #Prolog
Easy IHaskell Docker images with Nix. ~ Vaibhav Sagar. #Haskell #Docker #Nix
Partitions of a set. Shayne Fletcher. #Haskell #FunctionalProgramming
Explaining lambda calculus to a front-end web developer. ~ Henri Tuhola #LambdaCalculus
Laplace transform in Isabelle/HOL. Fabian Immler. #ITP #IsabelleHOL #Math
WordNet and Prolog: why not? ~ P. Julian-Iranzo, F. Saenz-Perez. #Prolog #LogicProgramming
Monads as a programming pattern. ~ Samuel Grayson. #Programming #Monads
The monad challenges (A set of challenges for jump starting your understanding of monads). ~ Doug Beardsley. #Haskell #Monads
Coding and reasoning with purity, strong types, and monads. ~ Doug Beardsley (mightybyte). #Haskell #Monads
Haskell: Build tools. ~ Kowainik. #Haskell #Cabal #Stack
Haskell kata: withTryFileLock. ~ M. Snoyman. #Haskell #FunctionalProgramming
How to write a game in Haskell from scratch. ~ Mario Morgenthum. #Haskell #Game
Transition to Haskell from Python. ~ Chris Martin, Julie Moronuki. #Python #Haskell
Dynamically-typed Haskell expressions involving applications and variables. ~ Rudy Matela. #Haskell #FunctionalProgramming
A topological data analysis library for Haskell. ~ Eben Kadile. #Haskell #FunctionalProgramming #Math #Topology
Pretty-printer for Haskell data types that have a Show instance. ~ Dennis Gosnell. #Haskell #FunctionalProgramming
Formalisation of an adaptive state counting algorithm in Isabelle/HOL. ~ Robert Sachtleben. #ITP #IsabelleHOL
Rosette: a solver-aided programming language that extends Racket with language constructs for program synthesis, verification, and more. ~ Emina Torlak. #Programming #Racket #Rosette #DSL #SAT #SMT
Haskell library containing common graph search algorithms. ~ Devon Hollowood. #Haskell #FunctionalProgramming #Algorithms
Verified functional programming. ~ N. Voirol. #PhD_Thesis #FunctionalProgramming #Scala
On monomorphisms and subfields. ~ C. Schwarzweller. #ITP #Mizar #Math
Undecidability of D_< and its decidable fragments. ~ J. Hu, O. Lhoták. #ITP #Agda
Comparison between different definitions of Dependent Object Types (DOTs). ~ J. Hu. #ITP #Agda
Programming languages explained with music. ~ Emma Murray. #Programming
Una serie de videos que te mostrarán de forma práctica y simple, cómo utilizar Emacs para la producción de documentos académicos. #Emacs
Abstract completion, formalized. ~ N. Hirokawa et als. #ITP #IsabelleHOL
Verifying bit-vector invertibility conditions in Coq. ~ B. Ekici et als. #ITP #Coq
Derivations as computations. ~ Andrej Bauer. #ITP #Andromeda
Andromeda: A minimalist implementation of type theory, suitable for experimentation. ~ Andrej Bauer #ITP #Andromeda
The essential tools of Scientific Machine Learning (Scientific ML). ~ Christopher Rackauckas. #MachineLearning #JuliaLang
La historia del desarrollo de software en dos minutos: un siglo de lógica, lenguajes y código. ~ @Alvy #Programación #Historia
Learning to prove theorems via interacting with proof assistants. ~ Adrian Colyer. #ITP #MachineLearning
Typed Lisp, a primer. ~ Musa Al-hassy. #Lisp #Haskell #FunctionalProgramming
Rib: a Haskell library for writing your own static site generator. ~ Sridhar Ratnakumar. #Haskell #FunctionalProgramming
From programs to deep models (Part 1). ~ Eran Yahav. #Programming #MachineLearning
Haskell. History of a community-powered language. ~ Denis Oleynikov, Gints Dreimanis. #Haskell #FunctionalProgramming #History
Haskell ITMO course at CTD. ~ Dmitry Kovanikov, Arseniy Seroka. #Haskell #FunctionalProgramming
Haskel’: Discussion about proposed changes to the Haskell programming language. #Haskell #FunctionalProgramming
Static smart constructors with double splices. ~ Chris Done #Haskell #FunctionalProgramming
Prolog implementation of the Knuth-Bendix completion procedure. ~ Markus Triska. #Prolog #LogicProgramming
New draft paper: Survey on bidirectional typechecking. ~ Neel Krishnaswami. #FunctionalProgramming
Comparison of functional programming languages. ~ Wikipedia. #FunctionalProgramming
Haskell: let vs. where. #Haskell #FunctionalProgramming
Point-free or die: Tacit programming in Haskell and beyond. ~ Amar Shah #Haskell #FunctionalProgramming
Grokking fix. ~ Matt Parsons. #Haskell #FunctionalProgramming
Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL
A formally verified abstract account of Gödel’s incompleteness theorems. ~ A. Popescu, D. Traytel. #ITP #IsabelleHOL #Logic
Isabelle/DOF. (User and implementation manual). ~ A.D. Brucker, B. Wolff. #ITP #IsabelleHOL
Studying algebraic structures using Prover9 and Mace4. ~ R. Arthan, P. Oliva. #ATP #Prover9 #Mace4 #Math
MUNTA: Fully verified model checker for timed automata. ~ Simon Wimmer. #ITP #IsabelleHOL
Type-based resource analysis on Haskell. ~ F. Siglmüller. #Haskell #FunctionalProgramming #Algorithms
Difference between `data` and `newtype` in Haskell. #Haskell #FunctionalProgramming
Type Classes vs. the World. ~ Edward Kmett. #Haskell #FunctionalProgramming
Verifying bit-vector invertibility conditions in Coq. ~ Burak Ekici et als. #ITP #Coq
Reconstructing veriT proofs in Isabelle/HOL. ~ M. Fleury, H.J. Schurr. #ITP #IsabelleHOL #SMT #veriT
Computer mathematics, AI and functional programming. ~ Moa Johansson. #ATP #ITP #Math #Haskell #FunctionalProgramming
IsaHipster: Theory exploration for Isabelle using HipSpec. ~ Moa Johansson. #ITP #IsabelleHOL #Haskell
Kei: A small and expressive dependently typed language. ~ Tiago Campos. #Haskell #FunctionalProgramming
Customizable datatypes. #Haskell #FunctionalProgramming
A very general method of computing shortest paths. ~ Russell O’Connor. #Haskell #FunctionalProgramming
Simple reflection of expressions. ~ Twan van Laarhoven. #Haskell #FunctionalProgramming
simple-reflect: Simple reflection of expressions containing variables. ~ Twan van Laarhoven. #Haskell #FunctionalProgramming
Monoids and finger trees. ~ Heinrich Apfelmus. #Haskell #FunctionalProgramming
All about monoids. ~ Edward Kmett. #Haskell #FunctionalProgramming
Applicative functors. ~ Pat Brisbin. #Haskell #FunctionalProgramming
Advantages of functional programming for Blockchain protocols. #FunctionalProgramming #Blockchain
La incidencia filosófica de la programación lógica. ~ Luís Moniz Pereira. #ProgramaciónLógica #Lógica #IA
Deductive proof of Ethereum smart contracts using Why3. ~ Z. Nehai, F. Bobot. #FormalVerification #Why3
Q-learning primer. ~ James Bowen. #Haskell #FunctionalProgramming
Overcoming boolean blindness with evidence. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
Teaching Haskell for understanding. ~ Julie Moronuki. #Haskell #FunctionalProgramming
The monad fear. #Haskell #FunctionalProgramming
Monads for functional programming. ~ Philip Wadler. #Haskell #FunctionalProgramming
Three useful monads. #Haskell #FunctionalProgramming
Monads in Haskell: Reader. ~ Martin Oldfield. #Haskell #FunctionalProgramming
The State monad: A tutorial for the confused? ~ Brandon Simmons. #Haskell #FunctionalProgramming
The continuation monad. ~ G. Gonzalez. #Haskell #FunctionalProgramming
Continuations from the ground up. ~ Isaac Elliott. #Haskell #FunctionalProgramming
Formalization of sorting algorithms in Isabelle/HOL. ~ Marco Pierre Fernandez Burgos. #BSc_Thesis #ITP #IsabelleHOL
Formalization of sorting algorithms in Isabelle/HOL (Code). ~ Marco Pierre Fernandez Burgos. #ITP #IsabelleHOL
Certified equational reasoning via ordered completion. ~ C. Sternagel, S. Winkle. #ITP #IsabelleHOL
Homotopy type theory: Synthetic homotopy theory and proof verification. ~ M. Blans. #BSc_Thesis #ITP #Agda #HoTT
Free theorems simply, via dinaturality. ~ J. Voigtländer. #Haskell #FunctionalProgramming
Functional dependencies & type families. ~ Gabriel Volpe #Haskell #FunctionalProgramming
Best practices for using functional programming in Python. ~ Tara Smith. #Python #FunctionalProgramming
Automatic white-box testing with free monads. ~ Alexander Granin #Haskell #FunctionalProgramming
Abstraction, intuition, and the “monad tutorial fallacy”. ~ Brent Yorgey. #Haskell #FunctionalProgramming
The trivial monad. ~ Dan Piponi. #Haskell #FunctionalProgramming
A gentle introduction to monad transformers. #Haskell #FunctionalProgramming
pLam: An interpreter for learning and exploring pure λ-calculus. ~ Sandro Lovnički. #LambdaCalculus #Haskell #FunctionalProgramming
What is a monad? #Haskell #FunctionalProgramming
Programming with effects. ~ Graham Hutton. #Haskell #FunctionalProgramming
What is a monad? ~ Graham Hutton. https://youtu.be/t1e8gqXLbsU #Haskell #FunctionalProgramming
Artificial neural networks and simplicial complexes. ~ Eduardo Paluzo. #NeuralNetworks #Math
Formal verification of the equivalence of system F and the pure type system L2. ~ Jonas Kaiser. #PhD_Thesis #ITP #Coq
Deferring the details and deriving programs. ~ Liam O’Connor. #ITP #Agda
Tic tac types: a gentle introduction to dependently typed programming (functional pearl). ~ S. Innes, N. Wu. #FunctionalProgramming #Idris #Haskell
Haskell pyramid. ~ Nick Sanford. #Haskell #FunctionalProgramming
PatternSynonyms for expressive code. ~ Raghu Kaippully. #Haskell #FunctionalProgramming
The Haskell learning curve. #Haskell #FunctionalProgramming
Fixed points and non-fixed points of Haskell functors. ~ Ziyang Liu. #Haskell #FunctionalProgramming
Free monoids and free monads, free of category theory. ~ Ziyang Liu. #Haskell #FunctionalProgramming
Solving the “Beautiful bridges” problem, algebraically. ~ Ziyang Liu. #Haskell #FunctionalProgramming
That guide that could help you get started with Haskell. ~ Djoe Pramono #Haskell #FunctionalProgramming
Set theory: An open introduction. ~ Tim Button. #eBook #SetTheory #Logic #Math
Yet another monad tutorial. ~ Mike Vanier. #Haskell #FunctionalProgramming
IsarMathLib: a library of formalized mathematics for Isabelle/ZF. ~ Slawomir Kolodynski. #ITP #IsabelleZF #Math
IsarMathLib: A library of formalized mathematics for Isabelle/ZF theorem proving environment. ~ Slawomir Kolodynski. #ITP #IsabelleZF #Math
Automated reasoning in first-order real vector spaces. ~ C. Kwan. #MSc_Thesis #ITP #ACL2 #Math
Functional pearl: Heterogeneous random-access lists. ~ W. Swierstra. #FunctionalProgramming #Agda
The Haskell pyramid. ~ Lucas Di Cioccio. #Haskell #FunctionalProgramming
Programming algorithms: Key-values. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms
A community-driven Emacs Lisp style guide. ~ Bozhidar Batsov. #Programming #Emacs #Lisp
A minimal Emacs configuration for Haskell programming. ~ Gil Mizrahi #Emacs #Haskell #FunctionalProgramming
Funtores, aplicativos y mónadas en imágenes. ~ Miguel Á. Moreno #Haskell #ProgramaciónFuncional
Understanding SAT by implementing a simple SAT solver in Python. ~ Sahand Saba. #Python #Logic
Questions and answers about Nix for haskellers. #Hakell #Nix

Septiembre de 2019

Resumen de lecturas compartidas durante el curso 2018-19. #GLC
A case study in basic algebra. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math
Functor, applicative, and monad. ~ TypesLogicsCats #FunctionalProgramming #OCaml #Haskell
Empirical mode decomposition and Hilbert-Huang transform in pure Haskell. ~ Justin Le (@mstk). #Haskell #FunctionalProgramming #Math
TTK: The Topology ToolKit (Topological data analysis and visualization). ~ Julien Tierny (@JulienTierny) et als. #MachineLearning #DataScience #Python
A functional reboot for deep learning. ~ Conal Elliott (@conal). #MachineLearning #DeepLearning #FunctionalProgramming #Haskell
The simple essence of automatic differentiation. ~ Conal Elliott (@conal). #MachineLearning #DeepLearning #FunctionalProgramming #Haskell
PyF: Haskell quasiquoter for string formatting. ~ Guillaume Bouchard. #Haskell #FunctionalProgramming
Functional programming with overloading and higher-order polymorphism. ~ Mark P. Jones. #Haskell #FunctionalProgramming
Announcing the optics library. ~ Adam Gundry. #Haskell #FunctionalProgramming
Merging IO and Either into one monad. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
FunSeqSet: Towards a purely functional data structure for the linearisation case of dynamic trees problem. ~ J.C. Saenz-Carrasco. #Haskell #FunctionalProgramming
Performance analysis of zippers. ~ Vı́t Šefl. #Haskell #FunctionalProgramming
A timeline for logic, λ-calculus, and programming language theory. ~ Dana S. Scott #Logic #LambdaCalculus #Programming #ITP #CompSci
Verifying the DPLL algorithm in Dafny. ~ C.C. Andrici, Ş. Ciobâcă. #Logic #SAT #FormalVerification #Dafny
(Co)inductive proof systems for compositional proofs in reachability logic. ~ V. Rusu, D. Nowak. #ITP #IsabelleHOL #Coq
Making a learning model. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
High performance Haskell. ~ Harendra Kumar. #Haskell #FunctionalProgramming
Functors and lifting. ~ Alicja Raszkowska (@mamrotynka). #Haskell #FunctionalProgramming
From LCF to Isabelle/HOL. ~ L. Paulson, T. Nipkow, M. Wenzel. #ITP #IsabelleHOL
From type theory to setoids and back. ~ Erik Palmgren. #ITP #Agda
Relational algebra with fancy types. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
Why Haskell is important. ~ Mark Karpov. #Haskell #FunctionalProgramming
Introduction to program synthesis. ~ Armando Solar-Lezama.
Ornaments for proof reuse in Coq. ~ Talia Ringer et als. #ITP #Coq
IMO (International Mathematical Olympiad) grand challenge. #AI #Math #ITP #LeanProver
Formal encoding of IMO (International Mathematical Olympiad) problems. ~ Daniel Selsam. #AI #Math #ITP #LeanProver
Automated reasoning for the working mathematician. ~ Jeremy Avigad. #ITP #ATP #Math
Automated reasoning for the working mathematician: notes on some experiments with the use of automation in Isabelle. ~ Jeremy Avigad. #ITP #IsabelleHOL
The great theorem prover showdown. ~ Hillel (@hillelogram). #ITP
Formalism and proofs for esverify. ~ Christopher Schuster. #ITP #LeanProver
Formalização de algoritmos de criptografia em um assistente de provas interativo. ~ Guilherme Gomes Felix da Silva. #MSc_Thesis #ITP #LeanProver
Okay, maybe proofs aren’t dying after all. ~ John Horgan. #Math
LL(1) parser generator verified in Coq. #ITP #Coq
QED at large: A survey of engineering of formally verified software. ~ Talia Ringer et als. #ITP #FormalVerification
The future of mathematics? ~ Kevin Buzzard. #Math #ITP #LeanProver
Introduction aux mathématiques formalisées. ~ Patrick Massot. #Math #ITP #LeanProver
100 theorems for Lean. ~ Floris van Doorn. #ITP #LeanProver #Math
A Coq formalization of boolean unification. ~ Daniel J. Dougherty. #ITP #Coq
Porting HOL Light’s multivariate analysis library: Some lessons. ~ Lawrence C. Paulson. #ITP #IsabelleHOL
Natürliches Schließen in Coq (Ein einführendes Tutorial). ~ Burkhardt Renz. #Logic #ITP #Coq
Neural networks and the satisfiability problem. ~ Daniel Selsam. #PhD_Thesis #Logic #SAT #NeuralNetworks
NeuroSAT: Learning a SAT solver from single-bit supervision. ~ Daniel Selsam. #Logic #SAT #NeuralNetworks
Demystifying MonadBaseControl. ~ Alexis King (@lexi_lambda). #Haskell #FunctionalProgramming
Logic, algebra, and geometry at the foundation of computer science. ~ T. Hoare, A. Mendes, J.F. Ferreira. #Math #CompSci
Breve historia de la Inteligencia Artificial. ~ F. Sancho (@sanchocaparrini). #IA #Historia
CompCertM: CompCert with lightweight modular verification and multi-language linking. ~ Youngju Song et als. #ITP #Coq
Five ways to compute the cartesian product with Haskell. ~ Andrew Ribeiro (@AndrewJRibeiro). #Haskell #FunctionalProgramming
Our journey to type checking 4 million lines of Python. ~ Jukka Lehtosalo. #Python
IA: hombres y máquinas. ~ José Ramón Rodríguez. #IA
Philosophy of Computer Science. ~ William J. Rapaport. #CompSci #Philosophy
How to build Artificial Intelligence we can trust. ~ Gary Marcus (@GaryMarcus). #AI
Running training iterations. | Monday Morning Haskell. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
Functor-oriented programming. ~ Russell O’Connor. #Haskell #FunctionalProgramming
Fun with Typeclasses. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
Verification components for hybrid systems in Isabelle/HOL. ~ Jonathan Julian Huerta y Munive. #ITP #IsabelleHOL #Math
Fourier series in Isabelle/HOL. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math
The DPRM theorem in Isabelle. ~ J. Bayer et als. #ITP #IsabelleHOL #Math
Virtualization of HOL4 in Isabelle. ~ F. Immler, J. Rädle, M. Wenzel. #ITP #IsabelleHOL #HOL4
Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. ~ R. Chen et als. #ITP #IsabelleHOL #Coq #Why3
A verified compositional algorithm for AI planning. ~ M. Abdulaziz, C. Gretton, M. Norrish. #ITP #HOL4 #AI
Proving tree algorithms for succinct data structures. ~ R. Affeldt et als. #ITP #Coq
Introduction à la programmation fonctionnelle avec Haskell. ~ Yann Esposito (@yogsototh). #Haskell #FunctionalProgramming
Falacias lógicas explicadas gráficamente. #Lógica
Pseudomathematics. #Math
Data types as quotients of polynomial functors. ~ J. Avigad, M. Carneiro, S. Hudon. #ITP #LeanProver
Primitive Floats in Coq. ~ G. Bertholon, E. Martin-Dorel, P. Roux. #ITP #Coq
A certificate-based approach to formally verified approximations. ~ F. Bréhard, A. Mahboubi, D. Pous. #ITP #Coq #Math
Higher-order Tarski Grothendieck as a foundation for formal proof. ~ C.E. Brown, C. Kaliszyk, K. Pak. #ITP #IsabelleHOL
Generic authenticated data structures, formally. ~ M. Brun, D. Traytel. #ITP #IsabelleHOL
A verified and compositional translation of LTL to deterministic Rabin automata. ~ J. Brunner, B. Seidl, S. Sickert. #ITP #IsabelleHOL
Formalizing computability theory via partial recursive functions. ~ M. Carneiro. #ITP #LeanProver
A smart A* search monad transformer which supports backtracking user-state. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming #AI
Why types matter. ~ Gabrieλ Volpe (@volpegabriel87).r#/ #Haskell #FunctionalProgramming
Announcing the refinement types library. ~ Nikita Volkov (@NikitaYVolkov). #Haskell #FunctionalProgramming
Programming algorithms: Hash-tables. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms
Best practices for using functional programming in Python. ~ Amandine Lee (@momandine). #Python #FunctionalProgramming
Artificial Intelligence: Foundations of computational agents, second edition. ~ David Poole, Alan Mackworth. #eBook #AI
“Program Verification”: Has it lost its punch? ~ Nikhil Swamy. #FormalVerification
First-order guarded coinduction in Coq. ~ L. Czajka. #ITP #Coq
Formalizing the solution to the cap set problem. ~ S.R. Dahmen, J. Hölzl, R.Y. Lewis. #ITP #LeanProver #Math
Nine chapters of analytic number theory in Isabelle/HOL. ~ M. Eberl. #ITP #IsabelleHOL #Math
Nine chapters of analytic number theory in Isabelle/HOL (Slides). ~ Manuel Eberl (@pruvisto). #ITP #IsabelleHOL #Math
A certifying extraction with time bounds from Coq to call-by-value lambda calculus. ~ Y. Forster, F. Kunze. #ITP #Coq
Formal proof and analysis of an incremental cycle detection algorithm. ~ A. Guéneau et als. #ITP #Coq
A formalization of forcing and the unprovability of the continuum hypothesis. ~ J.M. Han, F. van Doorn. #ITP #LeanProver
Refinement with time (Refining the run-time of algorithms in Isabelle/HOL). ~ M.P.L. Haslbeck, P. Lammich. #ITP #IsabelleHOL
Predicate transformer semantics for hybrid systems: Verification components for Isabelle/HOL. ~ J.J. Huerta y Munive, G. Struth. #ITP #IsabelleHOL
Structure and interpretation of computer programs (JavaScript adaptation). ~ H. Abelson et als. #eBook #Programming #JavaScript
Elle: Foundationally verified compilation for Ethereum. ~ M.M. Alvarez. #ITP #IsabelleHOL #Ethereum
Generating verified LLVM from Isabelle/HOL. ~ P. Lammich. #ITP #IsabelleHOL
Binary-compatible verification of filesystems with ACL2. ~ M.P. Mehta, W.R. Cook. #ITP #ACL2
Verifying that a compiler preserves concurrent value-dependent information-flow security. ~ R. Sison, T. Murray. #ITP #IsabelleHOL
Quantitative continuity and computable analysis in Coq. ~ F. Steinberg, L. Théry, H. Thies. #ITP #Coq
Deriving proved equality tests in Coq-Elpi: Stronger induction principles for containers in Coq. ~ E. Tassi. #ITP #Coq
Complete non-orders and fixed points. ~ A. Yamada, J. Dubut. #ITP #IsabelleHOL #Math
Verified decision procedures for modal logics. ~ M. Wu, R. Goré. #ITP #LeanProver #Logic
The beauty of functional languages in Deep Learning — Clojure and Haskell. ~ Jun Wu. #Clojure #Haskell #FunctionalProgramming #DeepLearning
Making Haskell run fast: the many faces of reverse. ~ Li-yao Xia. #Haskell #FunctionalProgramming #ITP #Coq
Declarative proof translation. ~ C. Kaliszyk, K. Pak. #ITP #IsabelleHOL #Mizar
Formalization of the domination chain with weighted parameters. ~ D.E. Severín. #ITP #Coq #Math
From type theory to setoids and back. ~ E. Palmgren. #ITP #Agda
Verifying randomised social choice. ~ M. Eberl (@pruvisto). #ITP #IsabelleHOL
A formalization of the mutilated chessboard problem in Lean. ~ Jeremy Avigad. #ITP #LeanProver
How to build an automated theorem prover. ~ Jens Otten. #Logic #ATP #Prolog
Building theorem provers using rewriting logic. ~ Carlos Olarte. #Logic #ATP #Maude
Machine-oriented reasoning. ~ Cláudia Nalon. #Logic #ATP
Build your own first-order prover. ~ Jens Otten. #Logic #ATP #Prolog
Stronger higher-order automation: A report on the ongoing Matryoshka project. ~ Jasmin Blanchette et als. #ITP #ATP
Clausal proofs of mutilated chessboards. ~ M.J.H. Heule, B. Kiesl, A. Biere. #ATP #PR
Why I prefer functional programming. ~ Mario Morgenthum. #Haskell #FunctionalProgramming
¿Qué es un lenguaje de programación? (Parte 1). ~ Alejandro Serrano (@trupill). #Programación
La Torre de Babel informática de los lenguajes de programación. ~ Alejandro Serrano (@trupill). #Programación
Overview of automated reasoning and ordering-based strategies. ~ Maria Paola Bonacina. #Logic #ATP
Computable analysis, exact real arithmetic and analytic functions in Coq. ~ F. Steinberg, H. Thies. #ITP #Coq #Math
Not a single proof assistant for all, but proof assistants for everyone. ~ Nicolas Tabareau. #ITP #Coq
Formalisation of probabilistic testing semantics in Coq. ~ Y. Deng, J.F. Monin. #ITP #Coq
Mars Rover Kata in Haskell. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
Building lenses (Implementing basic Haskell lenses in twenty exercises). ~ Mitchell Vitez. #Haskell #FunctionalProgramming
A cheatsheet to the time library. ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
Monday Morning Haskell: Adding random exploration. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming
Functional programming in Coq. ~ Yuxin Deng. #FunctionalProgramming #ITP #Coq #LambdaCalculus
G2Q: Haskell constraint solving. ~ W.T. Hallahan, A. Xue, R. Piskac. #Haskell #FunctionalProgramming
Structural and semantic pattern matching analysis in Haskell. ~ P. Kalvoda, T.S. Kerckhove. #Haskell #FunctionalProgramming
From type theory to Haskell in 10 minutes. ~ Matt Campbell. #Haskell #LambdaCalculus #TypeTheory
What is datatype-generic programming? ~ Max Hallinan. #Haskell #FunctionalProgramming
Seekable parsers in Haskell. ~ Frederik Ramcke. #Haskell #FunctionalProgramming
J. Donald Monk, Mathematical logic and lectures on set theory. #eBook #Logic #Math
The existential risk of Math errors. ~ Gwern Branwen. #Math
Effective problem solving using SAT solvers. ~ Curtis Bright et als. #SAT_solving
Prolog coding guidelines: Status and tool support. ~ F. Nogatz, P. Körner, S. Krings. #Prolog #LogicProgramming
On correctness of an n queens program. ~ W. Drabent. #Prolog #LogicProgramming
Formalization of multiway-join algorithms in Isabelle/HOL. ~ Thibault Dardinier. #ITP #IsabelleHOL
Slick 1.0 Release - Now with a quick and easy template! ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
Prolog fundamentals catchup. ~ James Norman Vladimir Cash (@jamesnvc). #Prolog #LogicProgramming
Tutorial: Creating Web applications in SWI-Prolog. ~ Anne Ogborn. #Prolog #LogicProgramming
Functional Prolog: map, filter and reduce. ~ Paul Brown. #Prolog #LogicProgramming
La deuda de la Inteligencia Artificial con el matemático Gödel. ~ Javier Muñoz de la Cuesta. #Lógica #IA
A zoo of Haskell newtype wrappers. ~ Sven Heyll. #Haskell #FunctionalProgramming
Interesting music in four lines of code. ~ Donya Quick. #Haskell #FunctionalProgramming
An integrated development environment for the Prototype Verification System (PVS). ~ P. Masci, C.A. Muñoz. #ITP #PVS
A formal semantics of Findel (Financial Derivatives Language) in Coq. ~ A. Arusoaie #ITP #Coq
Formal verification of upper bounds on translative packing densities. ~ I. Mulder. #MSc_Thesis #ITP #Coq
Probabilistic programming with Monad‑Bayes. Part 1: first steps. ~ S. Bhat, S. Carstens, M. Meschede. #Haskell #FunctionalProgramming
Learning Haskell: A resource guide. ~ Denis Oleynikov. #Haskell #FunctionalProgramming
The power of adjunctions. ~ Bartosz Milewski. #CategoryTheory #Programming
Optics + Regex: Greater than the sum of their parts. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
Sound and reusable components for abstract interpretation. ~ S. Keidel, S. Erdweg. #Haskell #FunctionalProgramming via @Iceland_jack
Certifying graph-manipulating C programs via localizations within data structures. ~ Shengyi Wang et als. #ITP #Coq
Leveraging highly automated theorem proving for certification. ~ Deni Raco et als. #ITP #IsabelleHOL
Verifying concurrent, crash-safe systems with Perennial. ~ Tej Chajed et als. #ITP #Coq
Lazy stream programming in Prolog. ~ Paul Tarau, Jan Wielemaker, Tom Schrijvers. #Prolog #LogicProgramming
Linear programming in Isabelle/HOL. ~ Julian Parsert and Cezary Kaliszyk. #ITP #IsabelleHOL #Math
Linear algebra of types. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming #Math
Introducción a la Lógica. ~ F. Sancho (@sanchocaparrini). #Lógica
Brevísima historia de la Lógica. ~ F. Sancho (@sanchocaparrini). #Lógica
Monday morning Haskell: Tweaks, fixes, and some results. ~ James Bowen (@james_OWA). #Haskell #FunctionalProgramming #AI
Haskell on Raspberry PI 4. ~ Vaclav Svejcar. #Haskell #FunctionalProgramming #Raspberry
Refactoring the Mars Rover Kata in Haskell. ~ Riccardo Odone (@RiccardoOdone). #Haskell #FunctionalProgramming
Emacs - The best Python editor? ~ Kyle Purdon (@PurdonKyle). #Emacs #Python
A formally verified monitor for metric first-order temporal logic. ~ J. Schneider et als. #ITP #IsabelleHOL
Adaptive online first-order monitoring. ~ J. Schneider et als #ITP #IsabelLEHOL
Isabelle for philosophers. ~ Ben Blumson. #ITP #IsabelleHOL #Logic
Ethereum’s recursive length prefix in ACL2. ~ Alessandro Coglio. #ITP #ACL2 #Ethereum
Eventful GHC (debugging / profiling Haskell via the GHC eventlog). ~ Alp Mestanogullari (@alpmestan). #Haskell #FunctionalProgramming
A formal proof of Hensel’s lemma over the p-adic integers. ~ Robert Y. Lewis. #ITP #LeanProver #Math
Comparison of proof producing systems in SMT solvers. ~ Arjun Viswanathan. #ATP #SMT
Lógica de primer orden: una introducción informal. F. Sancho (@sanchocaparrini). #Lógica
Number theorist fears all published Math is wrong. ~ Mordechai Rorvig. #Math #ITP #AI
Unit testing wai applications. ~ Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
Efficient stochastic programming in Julia. ~ M. Biel, M. Johansson. #Programming #JuliaLang
Mikrokosmos: an educational lambda calculus interpreter. ~ M. Román. #LambdaCalculus #Haskell
Programming algorithms: Trees. ~ Vsevolod Dyomkin. #Programming #CommonLisp #Algorithms
Where did “differentiable programming” come from? ~ Takeo Imai (@bonotake). #DeepLearning
Towards Coq-verified Esterel semantics and compiling. ~ G. Berry, L. Rieg. #ITP #Coq
Quantum computing in Haskell. ~ Christopher Wright. #BSc_Thesis #Haskell #FunctionalProgramming

Octubre de 2019

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

Noviembre de 2019

Neural Networks with Weighty Lenses (DiOptics?) ~ Philip Zucker (@SandMouth). #Haskell #NeuralNetworks #FunctionalProgramming
The future of work: How new technologies are transforming tasks. ~ M. Fleming et als. #AI #ML
Compile your comments in ghcid. ~ Jake Keuhlen. #Haskell #FunctionalProgramming
Scraping Goodreads Sitemaps with Haskell. ~ Marcus Buffett. #Haskell #FunctionalProgramming
How does the continuation monad work? ~ Max Hallinan. #PureScript #FunctionalProgramming
Copilot: A stream DSL for writing embedded C programs. ~ Lee Pike (@pike7464). #Haskell #FunctionalProgramming
Esta IA resuelve un antiguo problema matemático mucho más rápido. #IA
A basic Haskell solution to the robot journeys coding exercise. ~ Mark Seemann (@ploeh). #Haskell #FunctionalProgramming
The natural number game (version 1.06). ~ K. Buzzard, M. Pedramfar. #ITP #LeanProver #Math
Learn Coq in Y minutes tutorial. ~ Philip Zucker (@SandMouth). #ITP #Coq
No Garden of Eden: Adventures in Teaching Haskell to Kids. ~ Peter Berger (@peterb). #Haskell #FunctionalProgramming
The story of Logic. ~ Robert L. Constable. #Logic #Math #ITP
Computational foundations of Mathematics. ~ Robert L. Constable. #Logic Math #CompSci #ITP #Nuprl
Approximate normalization for gradual dependent types. ~ J. Eremondi, É. Tanter, R. Garcia. #GDTL
A review of the Lean theorem prover. ~ Thomas Hales. #ITP #LeanProver
La inteligencia artificial capaz de puntuar con notas sobresalientes en los exámenes de ciencias. ~ @Alvy. #IA
From ‘F’ to ‘A’ on the N.Y. Regents Science Exams: An Overview of the Aristo Project. ~ P. Clark et als. #AI
An implementation of Homotopy Type Theory in Isabelle/Pure. ~ J. Chen. #MSc_Thesis #ITP #IsabellePure #HoTT
A formal proof of PAC learnability for decision stumps. ~ J. Tassarotti, J.B. Tristan, K. Vajjha. #ITP #LeanProver
How to do binary random-access lists simply. ~ Donnacha Oisín Kidney (@oisdk). #Agda #FunctionalProgramming #ITP
Unrolling data with Backpack. ~ Oleg Grenrus. #Haskell #FunctionalProgramming
Category Theory. ~ Jean-Pierre Marquis. #CategoryTheory.
A brief tour of logic and optimization. ~ J. Hooker. #Logic #Optimization
Zermelo Fraenkel Set Theory in Higher-Order Logic. ~ Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
Differential Hoare logics and refinement calculi for hybrid systems with Isabelle/HOL. ~ S. Foster, G. Struth. #ITP #IsabelleHOL
CoqTL: A Coq DSL for rule-based model transformation. ~ Z. Cheng, M. Tisi, R. Douence. #ITP #Coq
Recent trends in STM Haskell. ~ P. Tiwari, S. Meenu. #Haskell #FunctionalProgramming
Introduction to univalent foundations of mathematics with Agda. ~ Martín Hötzel Escardó. #ITP #Agda HoTT
Coq à la carte (A practical approach to modular syntax with binders). ~ Y. Forster, K. Stark. #ITP #Coq
Fixed points and diagonal arguments. ~ Bartosz Milewski (@BartoszMilewski). #Haskell #Math
Python VS Common Lisp, workflow and ecosystem. #Python #CommonLisp
The four simple ways to encode sum-types. ~ Yair Chuchem (@yairchu). #Haskell #FunctionalProgramming
Proving groups with Idris. ~ Boro Sitnikovski## (@BSitnikovski). #Idris #FunctionalProgramming #ITP
Predicates vs functions. ~ Paul Brown. #Prolog #LogicProgramming
Qué es la teoría de categorías y cómo se ha convertido en tendencia. ~ John Baez (@johncarlosbaez). #Teoría_de_categorías #Lógica #Matemáticas #Computación
El problema de Collatz. ~ Juan Arias de Reyna. #Matemáticas
Probabilistic programming with Monad‑Bayes, Part 2: Linear regression. ~ S. Bhat, M. Meschede. #Haskell #FunctionalProgramming
Verified programming of Turing machines in Coq. ~ Y. Forster, F. Kunze, M. Wuttke. #ITP #Coq
Intuitionistic logic: a view of its evolution. ~ A.K. Peters. #Logic #CompSci
Minimal logic and automated proof verification. ~ L. Warren. #PhD_Thesis #ITP #Agda #Logic
Figurate numbers: a historical survey of an ancient mathematics. ~ D. Shane. #Math #History
Propositions as types: some missing links. ~ Kostiantyn Rybnikov (@ko_bx). #Agda #ITP #Math
Formalizing expressiveness of line editors. ~ Boro Sitnikovski. #ITP #Coq
Commanding Emacs from Coq. #ITP #Coq #Emacs
Goldbach: a curious conjecture. ~ R.J. Lipton, K.W. Regan. #Math
GHC exercises (A little course to learn about some of the more obscure GHC extensions). ~ Tom Harding (@am_i_tom). #Haskell #FunctionalProgramming
Linear relation algebra of circuits with HMatrix. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
Smart constructors that cannot fail. ~ Mark Karpov (@mrkkrp). #Haskell #FunctionalProgramming
Named typeclasses in Haskell. ~ Marco Perone (@marcoshuttle). #Haskell #FunctionalProgramming
Source-free machine-checked validation of native code in Coq. ~ K.W. Hamlen, D.Fisher, G.R. Lundquist. #ITP #Coq
Embracing a mechanized formalization gap. ~ A. Spector-Zabusky, J. Breitner, Y. Li, S. Weirich #ITP #Coq #Haskell via @scottfleischman
A probability theory library for the Coq theorem prover. ~ J. Tassarotti. #ITP #Coq #Math
Formalizing the dependency pair criterion for innermost termination. ~ A. Alves Almeida, M. Ayala-Rincón. #ITP #PVS
Computational logic: its origins and applications. ~ L.C. Paulson. #Logic #ITP #IsabelleHOL
Formalising mathematics in simple type theory. ~ L.C. Paulson. #Logic #Math #ITP #IsabelleHOL
A small proof that fin is injective. ~ Donnacha Oisín Kidney (@oisdk). #ITP #Agda
Variational autoencoders in Haskell, or: how I learned to stop worrying and turn my friends into dogs. ~ @heyitdeclan #Haskell #FunctionalProgramming via @SandMouth
The “many worlds” design pattern. ~ Paulo Moura. #LogicProgramming
Facts and fluents vs constants and variables. ~ Paul Brown. #Prolog #LogicProgramming
Abstracting user interaction. ~ Paulo Moura. #LogicProgramming
Monads in Haskell and category theory. ~ Samuel Grahn. #Haskell #FunctionalProgramming #CategoryTheory
Cofree traversable functors. ~ L. Waern. #Haskell #FunctionalProgramming #CategoryTheory
AXolotl: A self-study tool for first-order logic. ~ David M. Cerna. #Logic
Mathematical knowledge management across formal libraries. ~ D. Müller. #PhD_Thesis #MKM #ITP #PVS
2019 state of Haskell survey results. ~ Taylor Fausak (@taylorfausak). #Haskell #FunctionalProgramming
Forgetting to learn logic programs. ~ Andrew Cropper. #ILP #LogicProgramming
Swap the DB based on a config file. ~ Grégoire Charvet. #Haskell #FunctionalProgramming
Encoding problems in boolean satisfiability. ~ Ozan Erdem (@ozanerdem). #Logic #SAT_solving
Finite field polynomial arithmetic based on fast Fourier transforms. ~ Stephen Diehl (@smdiehl). #Haskell #FunctionalProgramming #Math
Mi entorno de trabajo en Emacs. ~ Ondiz. #Emacs
Category theory as a methodology for computational sciences. ~ Xinyuan Sun. #CategoryTheory #Haskell
Deeply integrating C11 code support into Isabelle/PIDE. ~ F. Tuong, B. Wolff. #ITP #IsabelleHOL
Deriving magic and parsing CSV. ~ Grégoire Charvet. #Haskell #FunctionalProgramming
Verified quantum computing. ~ Robert Rand. #ITP #Coq #QuantumComputing
Formally verified quantum programming. ~ Robert Rand. #PhD_Thesis #ITP #Coq #QuantumComputing
A quick reference for mapping Coq tactics to Lean tactics. ~ Joey Dodds. #ITP #Coq #LeanProver
Boring Haskell manifesto (how to get Haskell into your organization, and how to make your organization more productive and profitable with better engineering). ~ M. Snoyman (@snoyberg). #Haskell #FunctionalProgramming
Barbara Liskov: The architect of modern algorithms. ~ Susan D’Agostino (@susan_dagostino). #CompSci #Algorithms
Links to recourses for the Lean Theorem Prover. ~ Floris van Doorn. #ITP #LeanProver
A bare-bones Twitter clone implemented with Haskell + Nix. ~ Gabriel Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
CodeWorld import by Hash. ~ Chris Smith (@cdsmithus). #CodeWorld #Haskell
Certification of breadth-first algorithms by extraction~ D. Larchey-Wendling, R. Matthes. #Coq
Verified self-explaining computation. ~ J. Stolarek, J. Cheney. #ITP #Coq
The 2019/2020 edition of Strathclyde’s CS316 Functional Programming course. ~ Bob Atkey. #Haskell #FunctionalProgramming
Tools for tutoring theoretical computer science topics. ~ Mark McCartin-Lim. #PhD_Thesis #CompSci #Logic #ATP
Formally verified insertion of reference counting instructions. ~ Marc Huisinga. #ITP #LeanProver
A collection of resources for learning type theory and type theory adjacent fields. ~ Daniel Gratzer. #TypeTheory #CategoryTheory #ITP #Coq #LeanProver #HoTT
Constructing infinitary quotient-inductive types. ~ M. Fiore, A.M. Pitts, S.C. Steenkamp. #ITP #Agda
ConCert: A smart contract certification framework in Coq. ~ D. Annenkov, J.B. Nielsen, B. Spitters. #ITP #Coq #Blockchain
ConCert: A framework for smart contract verification in Coq. ~ J.B. Nielsen, D. Annenkov. #ITP #Coq #Blockchain
The sequent calculus calculator. ~ Matteo Kamm, Mike Marti. #BsC_Thesis #Logic #ITP #Elm #FunctionalProgramming
Sequent calculus calculator. #Logic #ITP
Kairos: a Haskell library for live coding Csound performances. ~ L. Foletto. #Haskell #FunctionalProgramming #Music
Supporting the Algebra I curriculum with an introduction to computational thinking course. ~ M.M. Laskowski. #MsC_Thesis #CodeWorld #Haskell #Teaching
Libro de exámenes de programación funcional con Haskell (versión del 25 de noviembre de 2019). #ProgramaciónFuncional #Haskell #I1M2019
Abstractions and constructions from math, implementations in FP languages and formalizations in proof assistants. ~ P. Paradziński. #CategoryTheory
PLT: A path to enlightenment in Programming Language Theory. ~ Steven Shaw (@steshaw). #Programming #TypeTheory #FunctionalProgramming #CategoryTheory via @pparadzinski
RustBelt: Securing the foundations of the Rust programming language. ~ Ralf Jung et als. #ITP #Coq #Rust
From math to machine: translating a function to machine code. ~ Brian Steffens (@brian_steffens). #Haskell #Math
Digging into Rust’s syntax. ~ James Bowen (@james_OWA). #Programming #Rust #Haskell
Conway’s game of life using Haskell and Gloss. ~ Alejandro Serrano (@trupill). #Haskell #FunctionalProgramming #Gloss
Categorical LQR control with linear relations. ~ Philip Zucker (@SandMouth). #Haskell #FunctionalProgramming
Supercharged imperative programming with Haskell and FP. ~ Anupam Jain (@ajnsit). #Haskell #FunctionalProgramming
The enormous theorem. ~ Sarah Spoenemann. #Math
Introducción a la “Introducción de Emacs”. #Emacs
Development of group theory in the language of internal set theory. ~ Zoltan Kocsis #PhD_Thesis #ITP #Agda #Logic #Math
Structured induction proofs in Isabelle/Isar. ~ M. Wenzel. #ITP #IsabelleHOL
Property invariant embedding for automated reasoning. ~ M. Olšák, C. Kaliszyk, J. Urban. #ATP #MachineLearnig
How to learn Haskell in 10 minutes a day. ~ Yulia Gavrilova. #Haskell #FunctionalProgramming
The Makam metalanguage: a tool for rapid language prototyping. ~ Antonis Stampoulis. #Programming #Makam #OCaml
How to make your papers run: Executable formal semantics for your language. ~ Teodoro Freund. #Programming #Makam
The Mind at Work: Guido van Rossum on how Python makes thinking in code easier. ~ Anthony Wing Kosner. #Programming #Python
The revolution in computing education at school: opportunity and challenge. ~ Simon Peyton Jones. #CompSci #Teaching

Diciembre de 2019

A formal proof of the independence of the continuum hypothesis. ~ Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Math
Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. ~ M. Sozeau et als. #ITP #Coq
Verified and verifiable computation with STV algorithms. ~ M.K. Ghale. #PhD_Thesis #ITP #Coq #HOL4
Exploring Euler’s foundations of differential calculus in Isabelle/HOL using nonstandard analysis. ~ J. Rockel. #MsC_Thesis #ITP #IsabelleHOL #Math
Learning functional programming. ~ S. Thompson. #FunctionalProgramming #Haskell
How Julia Robinson helped define the limits of mathematical knowledge. ~ Evelyn Lamb (@evelynjlamb). #Math
A formal proof of PAC learnability for decision stumps. ~ J. Tassarotti, J.B. Tristan, K. Vajjha. #ITP #LeanProver
How does Haskell make your life easier? ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
Introducción de Emacs: Trabajo con ventanas y buffers. #Emacs
What maths is in Lean? ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
Deriving monadic programs. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming
Formulating the Hamiltonian Path problem as a constraint satisfaction problem. ~ Ozan Erdem (@ozanerdem). #CSP
What are the advantages and disadvantages of using Haskell to implement a domain specific language? ~ Tikhon Jelvis. #Haskell #FunctionalProgramming #DSL
A computability proof of Gödel’s first incompleteness theorem. ~ Jørgen Veisdal (@JorgenVeisdal). #Logic #Math
Verifying information flow control libraries. ~ M. Vassena. #PhD_Thesis #ITP #Agda
Category theory by example. ~ I. Murashko, A. Radkov, M, Minshin. #CategoryTheory #Haskell #Scala #Cpp
An implementation of polygraphs. ~ Maxime Lucas. #ITP #Coq
The lambda calculus: A historical and practical tour. ~ R.B. Elrod. #LambdaCalculus
Se logra factorizar el semiprimo RSA-240 de 795 bits. ~ Francisco R. Villatoro (@emulenews). #Matemáticas #Computación
Deep learning for symbolic mathematics. ~ Guillaume Lample (@GuillaumeLample), François Charton. #DeepLearning via @__josejuan__
45 years of formal methods: Challenges and trends. ~ D. Bjørner, K. Havelund. #FormalMethods
Semialgebraic proofs and efficient algorithm design. ~ Noah Fleming, Pravesh Kothari, Toniann Pitassi. #Logic
FourierSAT: A Fourier expansion-based algebraic framework for solving hybrid boolean constraints. ~ A. Kyrillidis, A. Shrivastava, M.Y. Vardi, Z. Zhang. #ATP #Logic #SAT_solving
A probabilistic approach to satisfiability of propositional logic formulae. ~ Reazul Hasan Russel. #Logic #ATP #SAT
Correctness proofs of distributed systems with Isabelle. ~ Martin Kleppmann. #ITP #IsabelleHOL
Mathematics for Computer Science: “Top 10 proof techniques NOT allowed”. #Logic
Exploring the structure of an algebra text with locales. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math
Higher-order, higher-order automatic differentiation. ~ Conal Elliott (@conal). #Haskell #FunctionalProgramming
Haskell implementation of open games. ~ Jules Hedges (@_julesh_). #Haskell #FunctionalProgramming
Four ways to partially apply constraint tuples. ~ Ryan Scott. #Haskell #FunctionalProgramming
Mechanized verification of the correctness and asymptotic complexity of programs. ~ Armaël Guéneau. #PhD_Thesis #ITP #Coq
Challenges in the collaborative evolution of a proof language and its ecosystem. ~ Théo Zimmermann. #PhD_Thesis #ITP #Coq
Haskell vs OCaml. ~ Mark Karpov (@mrkkrp). #Haskell #OCaml #FunctionalProgramming
Non-reformist reform for Haskell modularity. ~ Scott Kilpatrick. #PhD_Thesis #Haskell #FunctionalProgramming
Efficient sampling of SAT and SMT solutions for testing and verification. ~ Rafael Tupynambá Dutra. #PhD_Thesis #SAT #SMT
A list of Haskell articles on good design, good testing. ~ Michael Oswald (@OswaldChocolate). #Haskell #FunctionalProgramming
An online JavaScript/WebAssembly version of Lean. #ITP #LeanProver
Rigorous mathematics. ~ Kevin Buzzard (@XenaProject). #ITP #Math
Measuring Haskell container sizes. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
Data types in Rust: Borrowing from both worlds. ~ James Bowen (@james_OWA). #Rust #Haskell
Reanimate: a library for programmatically generating animations with a twist towards mathematics / vector drawings. #Haskell
Ghosts of departed proofs convenience. ~ Chris Done (@christopherdone). #Haskell
Correct-by-construction typechecking with scope graphs. ~ Katherine Imhoff Casamento. #MSc_Thesis #ITP #Agda
To understand the future of AI, study its past. ~ Rob Toews. #AI
Exploration of neural machine translation in autoformalization of mathematics in Mizar. ~ Q. Wang, C. Brown, C. Kaliszyk, J. Urban. #MachineLearning #ITP #Mizar
A constructive formalization of the weak perfect graph theorem. ~ A.K. Singh, R. Natarajan. #ITP #Coq #Math
Biortogonalidad para corrección de compiladores y adecuación computacional. ~ Alejandro E. Gadea. #PhD_Thesis #ITP #Coq
Introduction to computational thinking: a new high school curriculum using CodeWorld. ~ F. Alegre, J. Underwoood, J. Moreno, M. Alegre. #CodeWorld #Haskel #FunctionalProgramming #Teaching
A generic framework for verified compilers using Isabelle/HOL’s locales. ~ M. Desharnais, S. Brunthaler. #ITP #IsabelleHOL
Logic in secondary education. ~ Michael Genesereth, Vinay Chaudhri. #Logic #Teaching
A survey on theorem provers in formal methods. ~ M.S. Nawaz, M. Malik, Y. Li, M. Sun, M. Lali. #ITP #ATP
Higher-order, higher-order automatic differentiation. ~ Conal Elliott (@conal). #Haskell
Introduction to lambda calculus. ~ G. Smolka. #LambdaCalculus
Computational type theory and interactive theorem proving with Coq. ~ G. Smolka. #eBook #ITP #Coq
Mathematician proves huge result on ‘dangerous’ problem. ~ Kevin Hartnett. #Math
Lazy constructive numbers and the Stern-Brocot tree. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming
Formalization of some central theorems in combinatorics of finite sets. ~ Abhishek Kr Singh. #ITP #Coq #Math
Programming algorithms: dynamic programming. ~ Vsevolod Dyomkin. #Programming #CommonLisp
Dependently typed Haskell in industry (experience report). ~ David Thrane Christiansen. #Haskell #FunctionalProgramming
Dependently typed Haskell in industry (experience report). ~ David Thrane Christiansen et als. #Haskell #FunctionalProgramming
Automatic extraction of Hilbert Calculi associated to fragments of classical logic. ~ Joel Felipe Ferreira Gomes. #BSc_Thesis #Haskell #Logic
Fibonacci formalized 1: some sums. ~ Bryan Gin-ge Chen (@blockspins). #ITP #LeanProver #Math
Fibonacci formalized 2: bees and cars. ~ Bryan Gin-ge Chen (@blockspins). #ITP #LeanProver #Math
A predicate transformer semantics for effects. ~ Wouter Swierstra, Tim Baanen. #Agda #FunctionalProgramming #ITP
Running Lisp in production. ~ Vsevolod Dyomkin. #CommonLisp
A formal proof of the irrationality of ζ(3). ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math
REPLica: REPL instrumentation for Coq analysis. ~ Talia Ringer (@TaliaRinger) et als. #ITP #Coq
Runtime support for multicore Haskell: a retrospective. ~ Simon Marlowe, Simon Peyton Jones, and Satnam Singh. #Haskell #FunctionalProgramming
Casa and Stack. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming
PrologCheatSheet: Basics of relational programming with Prolog. ~ Musa Al-hassy. #Prolog #LogicProgramming
Incomplete and utter introduction to modal logic, Pt. 1. ~ Danya Rogozin. #Logic
Fun with formal methods for better education. ~ N. Shilov, E. Muravev, S. Shilova. #FormalMethods #Math
On the expressive power of indexed applicative and monadic structures. ~ Jan Malakhovski. #PhD_Thesis #Haskell #FunctionalProgramming
Donald Knuth reflects on 50 years of ‘The Art of Computer Programming‘. #Programming
The Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler and Yong Kiam Tan. #ITP #IsabelleHOL #Math
The Lean mathematical library. ~ The mathlib Community. #ITP #LeanProver #Math
Top 10 Haskell open-source projects for Linux users. ~ Jonn Mostovoy. #Haskell #FunctionalProgramming
Course about numerical Python. ~ Rafa Rodríguez Galván (@cucharro). #Programming #Python #Math
Kurt Gödel and the mechanization of mathematics. ~ Juliette Kennedy. #Math #Logic
Logic for exact real arithmetic. ~ H. Schwichtenberg, F. Wiesnet. #Logic #Math #Minlog #Haskell
Isabelle/C: a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. ~ F. Tuong, B. Wolff. #ITP #Isabelle
Counting inversions via rank queries. ~ Brent Yorgey. #Haskell #FunctionalProgramming
Algebraic lenses. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
Haskell art in your browser with Asterius. ~ Sylvain Henry, Shao Cheng. #Haskell #FunctionalProgramming
Presentación del método de Polya para la resolución de problemas. ~ Jimena Fernández García. #Heurística
pretty-relative-time: a little library to describe dates and times in the future or in the past in a nice, human readable, familiar feeling way. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
Prefer to use fail for IO exceptions. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
Automated reasoning and robotics. ~ Zainab Al Kashari, Fatma Al Taheri. #ATP
Calculemus! ~ Brian Hayes (@bit_player). #Programming #Math
A verified prover based on ordered resolution. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel. #ITP #IsabelleHOL
Formal verification of a constant-time preserving C compiler. ~ G. Barthe et als. #ITP #Coq
Programming and interactive proving with Z3Py. ~ Philip Zucker (@SandMouth). #ITP #Z3
Liquidate your assets: reasoning about resource usage in Liquid Haskell. ~ M.A.T. Handley, N. Vazou, G. Hutton. #Haskell #FunctionalProgramming #LiquidHaskell
A glossary of functional programming. ~ John A De Goes #FunctionalProgramming
Notes on Category Theory with examples from basic mathematics. ~ Paolo Perrone (@PaoloPerrone8). #CategoryTheory #Math
Functional programming and justice in a world without time. ~ Anirudh Eka (@anirudh_eka). #FunctionalProgramming
A categorical view of computational effects. ~ Emily Riehl. #CategoryTheory #Math #Programming
Formalising Mathematics in praxis: a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started. ~ Angeliki Koutsoukou-Argyraki (@AngelikiKoutso1). #ITP #IsabelleHOL #Math
Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle. ~ Sven Schneider. #PhD_Thesis #ITP #IsabelleHOL
Stupid Z3Py tricks: verifying sorting networks off of Wikipedia. ~ Philip Zucker (@SandMouth). #Z3 #SMT
Notes on Category Theory in Scala 3 (Dotty). ~ Juan Pablo Romero (@1jpablo1). #CategoryTheory #Scala #FunctionalProgramming
Quotients in Coq. ~ Arthur Azevedo de Amorim. #ITP #Coq
A verification challenge. ~ Arthur Azevedo de Amorim. #ITP #Coq
Cohomology for kids. ~ @RAnachro. #Math
A few Haskell highlights of 2019. ~ Gints Dreimanis. #Haskell #FunctionalProgramming
Python type hints. ~ Guilherme Kunigami (@kunigami). #Python #Programming
Three equivalent ordinal notation systems in cubical Agda. ~ F.N. Forsberg, C. Xu, N. Ghani. #ITP #Agda
Intrinsically-typed definitional interpreters for linear, session-typed languages. ~ A. Rouvoet et als. #ITP #Agda
More stupid Z3Py tricks: Simple proofs. ~ Philip Zucker (@SandMouth). #Z3 #SMT
12 beautiful mathematical theorems with short proofs. ~ Jörg Neunhäuserer. #Math
Some fundamental theorems in mathematics. ~ Oliver Knill. #Math
Famous conjectures in mathematics. ~ Béla Bajnok. #Math
Thirty-six unsolved problems in number theory. ~ F. Smarandache. #Math
Famous mistakes in mathematics. ~ J. Pogonowski. #Math
Formalizing determinacy of concurrent revisions. ~ Roy Overbeek. #ITP #IsabelleHOL
A complete axiomatisation of a fragment of language algebra. ~ Paul Brunet. #ITP #Coq #Math
A mechanized formalization of GraphQL. ~ T. Díaz, F. Olmedo, É. Tanter. #ITP #Coq
Stupid Z3Py tricks strikes back: Verifying a Keras neural network. ~ Philip Zucker (@SandMouth). #Z3 #SMT #Keras #NeuralNetworks
Teaching Haskell with Duet. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming #Duet
The Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math
Verifying x86 instruction implementations. ~ S. Goel et als. #ITP #ACL2

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Lecturas del año 2019.org

Lecturas del año 2019.org

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

Contenido

Enero 2019

Febrero 2019

Marzo 2019

Abril 2019

Mayo 2019

Junio 2019

Julio 2019

Agosto 2019

Septiembre de 2019

Octubre de 2019

Noviembre de 2019

Diciembre de 2019

Files

Lecturas del año 2019.org

Latest commit

History

Lecturas del año 2019.org

File metadata and controls

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

Contenido

Enero 2019

Febrero 2019

Marzo 2019

Abril 2019

Mayo 2019

Junio 2019

Julio 2019

Agosto 2019

Septiembre de 2019

Octubre de 2019

Noviembre de 2019

Diciembre de 2019