Lecturas del año 2016.org

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

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

Enero 2016

• Categorical monads and computer programming. ~ N. Benton #Math #CompSci
• Answer sets and the language of answer set programming. ~ V. Lifschitz #ASP #Declarative_programming
• Formal proof of soundness for an RL prover. ~ A. Arusoaie et als. #ITP #Coq
• ACL2: Implementation of a computational logic. ~ M. Kaufmann #ITP #ACL2
• ACL2 support for interactive proof. ~ M. Kaufmann #ITP #ACL2
• Introduction to ACL2. ~ M. Kaufmann [Slides] #Logic #ITP #ACL2
• The table monad in Haskell. ~ A. Vandenbroucke, T. Schrijvers & F. Piessens #Haskell
• Answer set programming and configuration knowledge representation. ~ A. Falkner #ASP #KR #Logic
• A sample implementation of L-systems in Haskell. ~ F. Allberg #Haskell
• Fixed points for Markov decision processes. ~ J. Hölzl #ITP #Isabelle_HOL
• The rsync algorithm: Just playing with the ideas in rsync with Haskell ~ R. Muthukrishnan #Haskell
• Data vs theory: the mathematical battle for the soul of physics. ~ D.H. Bailey & J.M. Borwein
• A computationally surveyable proof of the Curve25519 group axioms. ~ D.M. Russinoff #ITP #ACL2
• Logique propositionnelle, P, NP. ~ J. Goubault-Larrecq #Logic
• VPHL: A verified partial-correctness logic for probabilistic programs ~ R. Rand & S. Zdancewic #ITP #Coq
• Algebraic numbers in Isabelle/HOL ~ R. Thiemann & A. Yamada #ITP #Isabelle_HOL #AFP
• Emacs org-mode examples and cookbook. ~ E. Neilsen #Emacs
• Pour un raffinement spatio-temporel tuilé ~ S. Archipoff & D. Janin #Haskell
• Lazy dynamic programming. ~ T. Jelvis #Haskell
• High-level functional properties of bit-level programs: Formal specifications and automated proofs. ~ C. Dross et als. #Why3
• Using Elm to create a fun game in just five days. ~ K. Wilcke & A. Kuzmin #Elm
• A Coq library for internal verification of running-times. ~ J. McCarthy et als. #Coq
• Diagrams quick start tutorial. #Haskell #Diagram
• Higher-order representation predicates in separation logic. ~ A. Charguéraud #Coq
• Semi-intelligible Isar proofs from machine-generated proofs. ~ J.C. Blanchette et als. #ITP # ATP #Isabelle_HOL
• Elm in the real world. ~ O. Hanhinen #FP #Elm
• Verified representations of Landau’s “Grundlagen” in the λδ family and in the calculus of constructions. ~ F. Guidi #ITP #Coq
• Formal analysis of geometrical optics using theorem proving. ~ M.U. Siddique #PhD_Thesis #HOL_Light
• Certification of programs with computational effects. ~ B. Ekici #PhD_Thesis #ITP #Coq
• Efficient amortised and real-time queues in Haskell. ~ E. de Vries #Haskell
• Executable relational specifications of polymorphic type systems using logic programming. ~ Ki Yung Ahn #Prolog
• TIPER: Type Inference Prototyping Engines from Relational Specifications of type systems. ~ Ki Yung Ahn #Prolog
• A simple Haskell function. ~ N. Mitchell #Haskell
• Functional programming, abstraction, names. ~ Stephen Diehl #Programming #Haskell #Mat
• On mathematical proving. ~ P. Stefaneas & I.M. Vandoulakis #Math #Agents #Events
• Formal verification of stability properties of cyber-physical systems. ~ M. Chan et als. #ITP #Coq
• Types, abstraction and parametric polymorphism in higher-order logic. ~ O. Kunčar #PhD_Thesis #Isabelle_HOL
• Liouville numbers in Isabelle/HOL. ~ M. Eberl #ITP #Math #Isabelle_HOL #AFP
• Basic geometric properties of triangles. ~ M. Eberl #ITP #Math #Isabelle_HOL #AFP
• The divergence of the prime harmonic series. ~ M. Eberl #ITP #Math #Isabelle_HOL #AFP
• Descartes’ rule of signs. ~ M. Eberl #ITP #Math #Isabelle_HOL #AFP
• Perspectives on formal verification. ~ H.M. Friedman #Logic #Math #CompSci
• Thinking about how and why we prove. ~ Evelyn Lamb #Logic #Math #CompSci #ITP
• Cardinality of number partitions in Isabelle/HOL. ~ L. Bulwahn #ITP #Isabelle_HOL #AFP
• Course notes equational programming: Lambda calculus. ~ Femke van Raamsdonk
• A theorem prover for quantum Hoare logic and its applications. ~ T. Liu et als. #ITP #Isabelle_HOL
• A formally verified proof of the central limit theorem. ~ L. Serafin #ITP #Math #Isabelle_HOL
• What is the modern conception of logic? #1. ~ P. Smith #Logic
• Logicians’ biographies. ~ R. Zach #Logic
• Particle smoothing. ~ D. Steinitz #Haskell
• Introducing dimensional: Statically checked physical dimensions for Haskell. ~ D. McClean #Haskell
• Formalized linear algebra over elementary divisor rings in Coq. ~ G. Cano et als. #ITP #Coq #Math
• Pitfalls in Haskell. ~ S. Kiiskinen #Haskell
• Set covering problem. ~ A. Kaygun #Lisp
• Course: Introduction to functional programming ~ S. Kiiskinen #Haskell
• Introduction to functional programming: Course tasks. ~ S. Kiiskinen #Haskell
• Functional programming 2: Course tasks. ~ S. Kiiskinen #Haskell
• GHC/Haskell language extensions: a digest. ~ Allele Dev #Haskell
• Our functional future or: How I learned to stop worrying and love Haskell. ~ @drombosky & @FugueHQ #Haskell
• Practical recursion schemes at PragPub. ~ @RacquelYerbury #Haskell
• Design, optimization, and formal verification of circuit fault-tolerance techniques. ~ D. Burlyaev #PhD_Thesis #ITP #Coq
• Monad tutorials timeline. #Haskell
• Example pet shop written in Haskell. ~ R. Johnson #Haskell
• Building a business that combines human experts and data science ~ B. Lorica #DataScience
• What’s a natural transformation? ~ L. Palmer #Math #Haskell
• Category theory/natural transformation ~ HaskellWiki. #Math #Haskell
• Type introduction illustrated for casual Haskellers (to get over the Foldable) ~ Takenobu T. #Haskell
• Probabilistic functions and cryptographic oracles in higher order logic. ~ A. Lochbihler #Isabelle_HOL
• Failure of unique factorization ~ D. Lipton #Math
• Catamorphisms in 15 minutes! ~ C. Jones #Haskell #Math
• Understanding F-algebras. ~ @BartoszMilewski #Haskell #Math
• Happy learn Haskell tutorial. #eBook #Haskell

Febrero 2016

• Proof auditing formalised mathematics. ~ M. Adams #ITP #Math
• Clojure for data science. ~ Mike Anderson #DataScience #Clojure
• Now f is continuous (exercise!). ~ R.D. Arthan #ITP #Math #ProofPower
• GPU programming in Haskell using GPipe (Part 1). ~ Tobias Bexelius #Haskell
• GPU programming in Haskell using GPipe (Part 2). ~ Tobias Bexelius #Haskell
• Mixing computations and proofs. ~ M. Beeson #ITP #Logic #Math #CompSci
• Category theory and networks: Corelations in network theory. ~ Azimuth #Math
• Haskell is not for production and other tales. ~ Katie Miller #Haskell
• Haskell for commercial software development. ~ Mike Craig #Haskell
• Anaconda for R users: SparkR and rBokeh. ~ Christine Doig #Python
• Type theory and practical foundations. ~ J. Avigad #Logic #CompSci #ITP
• Homotopy type theory. ~ J. Avigad #HoTT #Math #CompSci
• The Lean theorem prover (system description). ~ L. de Moura, S. Kong, J. Avigad, F. Van Doorn & J. von Raumer #ITP #Lean
• Becoming productive in Haskell. ~ Matthew Griffith #Haskell
• From mathematics to map-reduce. ~ G. Gonzalez #Haskell #Math
• The Isar proof language in 2016. ~ M. Wenzel #ITP #Isabelle #Isar
• A modular, efficient formalisation of real algebraic numbers. ~ W. Li & L.C. Paulson #ITP #Isabelle_HOL #Math
• Monad transformers, free monads, mtl, laws and a new approach. ~ @acid2 #Haskell
• Difference lists and the codensity monad. #Haskell
• Promoting the arrow type. ~ Alexander Vieth #Haskell
• Binary and exponential searches. ~ Ross Paterson #Haskell
• Big data, small data, and the role of logic in machine learning. ~ A. Cropper #Prolog #ILP
• Tutorial: Creating Web applications in SWI-Prolog. ~ Anne Ogborn #Prolog
• Simply logical: Intelligent reasoning by example. ~ P. Flach #eBook #Prolog #Logic #AI
• Parser combinators: parsing for Haskell beginners. #Haskell
• Hammering towards QED. ~ J.C. Blanchette, C. Kaliszyk, L.C. Paulson & J. Urban #ATP #ITP
• FLTKHS: Easy, native GUIs in Haskell using FLTK. ~ A. Siram #Haskell
• A unified Coq framework for verifying C programs with floating-point computations. ~ T. Ramananandro et als. #ITP #Coq
• A reflection on types. ~ S. Peyton Jones, S. Weirich, R.A. Eisenberg & D. Vytiniotis #Haskell
• Empirical evaluation of test coverage for functional programs. ~ Y. Cheng et als. #Haskell
• Theorem proving in Lean. ~ J. Avigad, L. de Moura & S. Kong #eBook #ITP #Lean #Logic #CompSci
• Lambda calculus. ~ S. Das #Logic #CompSci
• Formalisation of ground inference systems in a proof assistant. ~ M. Fleury #ITP #Logic #Isabelle_HOL
• Teaching Haskell to a mathematician. ~ Syd Kerckhove #Haskell
• Introducción a la programación con la ayuda de PSeInt. ~ R. Saucedo #Programación #PSeInt
• Formalizing Jordan normal forms in Isabelle/HOL. ~ R. Thiemann & A. Yamada #ITP #Math #Isabelle_HOL
• Why today’s computer science students need to know more about ‘professional coding’. ~ Mark Warren #CompSci #Coding
• State of Clojure 2015 survey results. ~ Justin Gehtland #Clojure
• Are there some students who can’t learn how to code? ~ D. Blaikie #Programming
• Certified context-free parsing: a formalisation of Valiant’s algorithm in Agda. ~ J.P. Bernardy, P. Jansson #ITP #Agda
• QuickPlot: Quick and easy data visualizations with Haskell. #Haskell
• Magic to do (Can we avoid accepting what we cannot verify?) ~ R.J. Lipton & K.W. Regan #Math
• Compiling Hilbert’s operator. ~ K. Rustan & M. Leino #Dafny
• Hoed: a lightweight tracer and algorithmic debugger. #Haskell
• Foundations of infinitesimal calculus. ~ H.J. Keisler #eBook #Math #OpenLibra
• Viva La Resistance! A Resistance game solver. ~ Lee Pike #Haskell
• Equivalencias entre funciones de Haskell y Maxima. ~ J.A. Alonso #Haskell #Maxima
• Formalization of resolution calculus in Isabelle. ~ A. Schlichtkrull #PhD_Thesis #ITP #Isabelle_HOL #Logic
• Decision trees are free monads over the reader functor. ~ C. Thomas #Haskell
• Making efficient use of memory in Haskell. ~ Will Sewell #Haskell
• Theorema 2.0: Computer-assisted natural-style mathematics ~ B. Buchberger et als. #ITP #Theorema
• Proof and computation in Coq. ~ L. Théry et als. [Slides] #ITP #Coq
• The euclidean algorithm generates traditional musical rhythms. ~ G. Toussaint #Math #Music
• A verified SAT solver framework with learn, forget, restart, and incrementality. ~ J.C. Blanchette #Isabelle_HOL
• The finest imperative language. #Haskell
• A case study on using functional programming for Internet of Things applications. ~ Till Haenisch #FP #IoT
• Symbolic pattern matching in Clojure. ~ S. C. Lynch #Clojure
• Using Crash Hoare Logic for certifying the FSCQ file system. #Coq #Haskell
• Git fundamentos. ~ J. Amieiro Becerra #LibroLibre #Programación #Git #OpenLibra
• Stack traces in GHCi, coming in GHC 8.0.1. ~ S. Marlow #Haskell
• Python programación. ~ L. Rodríguez Ojeda #LibroLibre #Programación #Python #OpenLibra
• Tutorial on type theory. ~ A. Bauer #Logic #CompSci
• Constructive logic for concurrent real number computation. ~ U. Berger #Logic #CompSci
• Formal verification of numerical analysis programs. ~ S. Boldo #ITP #Coq #Math
• Newton sums for an effective formalization of algebraic numbers. ~ C. Cohen & B. Djalal #ITP #Coq #Math
• The Seifert–van Kampen theorem in homotopy type theory. ~ K.B. Hou & M. Shulman #ITP #Agda #Math #HoT
• Tests vs types. ~ K. Mahoney #Haskell
• NumberTheory: A Haskell number theory library. ~ Chris Fredrickson #Haskell
• A gentle introduction to secure computation.
• A Pamphlet against R (Computational intelligence in Guile Scheme). ~ Panicz Maciej Godek #Scheme #Guile #Rstats
• QuickPlot: Quick and easy data visualizations with Haskell. #Haskell
• Verified numerics for ODEs in Isabelle/HOL. ~ F. Immler [Slides] #ITP #IsabelleHOL #Math
• Algebra and analysis in the Lean theorem prover. ~ Rob Lewis #ITP #Lean #Polya #Math
• Conversion of HOL Light proofs into Metamath. ~ M.M. Carneiro #ITP #OpenTheory #Metamath #HOL_Light
• Mathematical theory exploration in Theorema: Reduction rings. ~ A. Maletzky #ITP #Theorema #Math
• Categories: From zero to infinity. ~ P. Schapira #Math
• Fighting spam with Haskell. ~ Simon Marlow. [Slides] #Haskell #Haxl
• Matters computational (Ideas, algorithms, source code). ~ Jörg Arndt #eBook #Algorithms #Programming
• Applications of MaxSAT in data analysis. ~ J. Berg, A. Hyttinen & M. Järvisalo #MaxSAT #Data_analysis
• Formal proof of soundness for an RL prover. ~ A. Arusoaie et als. #ITP #Coq
• The Isabelle refinement framework (for verification of large software systems). ~ P. Lammich #ITP #IsabelleHOL
• Natural language access to data via deduction. ~ R. Waldinger #ATP
• Beyond automation: smart machines + smart humans. ~ T.H. Davenport #AI
• Selling Haskell in the pub. ~ Neil Mitchell #Haskell
• A general BFS solver in NetLogo. ~ F. Sancho #NetLogo #AI
• Seminario agentes, multiagentes y aplicaciones. ~ G. Aranda #IA
• The joy and agony of Haskell in production. ~ S. Diehl #Haskell
• Cálculo numérico con Maxima. ~ J. Ramírez #Maxima #Matemáticas
• Breve manual de Maxima. ~ R. Ipanaqué #Libro #Maxima
• Higher-order recursion abstraction: How to make Ackermann, Knuth and Conway look like a bunch of primitives. #Haskell
• Verifying Buchberger’s algorithm in reduction rings. ~ A. Maletzky #ITP #Theorema #Math
• SimpleFP - A series of increasingly complex purely functional PLs implemented in Haskell. ~ Darryl McAdams #Haskell
• Linear regression in pictures. ~ Aditya Bhargava #Math
• Course: Advanced functional programming. ~ J. Yallop #FP #OCaml #Fω
• Doing data science with Clojure. ~ @sbelak #DataScience #Clojure
• It Is What It Is (And Nothing Else). ~ Robert Harper #CompSci
• State of the Haskell ecosystem (February 2016 edition). ~ G. Gonzalez #Haskell
• Purely functional Web apps. ~ Michał Płachta #Haskell
• Applied logic in engineering. ~ M. Spichkova #Teaching #Logic
• Constraint (logic) programming. ~ R. Barták #Logic #Programming #Prolog
• Proving with types. ~ Matt Parsons #Haskell #Logic
• A framework for certified self-stabilization case study: silent self-stabilizing k-dominating set on a tree. ~ K. Altisen #Coq
• Course: Applied logic in engineering. ~ M. Spichkova & M. Broy #Course #Logic
• Level-confluence of 3-CTRSs in Isabelle/HOL. ~ C. Sternagel, T. Sternagel #IsabelleHOL
• What mathematical logic says about the foundations of mathematics. ~ C. Bernardi. #Logic #Math
• Classical logic and intuitionistic logic: equivalent formulations in natural deduction. ~ R. Moot & C. Retoré. #Logic
• Computability and analysis, a historical approach. ~ V. Brattka. #Math #CompSci
• Automatically proving mathematical theorems with evolutionary algorithms and proof assistants. ~ L.A. Yang et als. #ITP #Coq
• Features of a high school olympiad problem. ~ L. Smolinsky #Math
• A survey on Domain-Specific Languages for machine learning in Big Data. ~ I. Portugal, P. Alencar, D. Cowan #Programming #BigData
• QED reloaded: Towards a pluralistic formal library of mathematical knowledge. ~ M. Kohlhase, F. Rabe #MKM
• Haskell by example. ~ Tatsuya Hirose #Haskell
• Fighting spam with Haskell. ~ Simon Marlow #Haskell
• Dimpl: An efficient and expressive DSL for discrete mathematics ~ R. Jha #Haskell #Math
• Retrieval, transformation and verification of proofs in higher order logic. ~ Shuai Wang #ITP #ProofCloud
• The promise of Artificial Intelligence unfolds in small steps. ~ S. Lohr #AI

Marzo 2016

• Mechanizing a process algebra for network protocols. ~ T. Bourke, R.J. van Glabbeek, P. Höfner #ITP #IsabelleHOL
• The Haskell cheatsheet. ~ J. Bailey #Haskell
• Proving completeness of logic programs with the cut. ~ W. Drabent #Logic #Prolog
• Linear temporal logic in Isabelle/HOL. ~ S. Sickert #ITP #Logic #IsabelleHOL #AFP
• What mathematical logic says about the foundations of mathematics. ~ C. Bernardi #Logic #Math #CompSci
• Haskell meets large scale distributed analytics. ~ A. Mestanogullari & M. Boespflug #Haskell #BigData
• The rigor resolution on undergraduate education ~ Boyer (1995) #CompSci #Education
• Formalized mathematics. ~ J. Harrison #Logic #Math #CompSci
• Proof of correctness of a marching cubes algorithm carried out with Coq. ~ A.N Chernikov & J. Xu #ITP #Coq
• Automated search for Gödel’s proofs. ~ W. Sieg & C. Field #Logic #Math #CompSci #ATP
• Introduction to funcional programming. ~ J. Harrison (1997) #FP #ML
• Teaching logic for computer science: are we teaching the wrong narrative? ~ J.A. Makowsky #Logic #CompSci #Teaching
• Proof relevant corecursive resolution. ~ P. Fu et als. #ITP #Coq #Haskell
• A general A* solver in NetLogo ~ F. Sancho #Netlogo
• The perfect language. ~ Gregory Chaitin #Logic
• La teoría de grupos, el cubo de Rubik y Johann Sebastian Bach. ~ Imanol Pérez #Matemáticas
• Todo entero positivo es suma de tres capicúas. ~ Javier Cilleruelo #Matemáticas
• A Coq library for internal verification of running-times. ~ J. McCarthy et als. #ITP #Coq
• Teaching cryptography. ~ Boaz Barak #Cryptography
• Formal verification of the rank function for succinct data structures. ~ A. Tanaka et als. #ITP #Coq #BigData
• Certified universal gathering in R² for oblivious mobile robots. ~ P. Courtieu et als. #ITP #Coq
• Open source Mathematica compatible Mathics 0.9. ~ Mike James #CAS #Math
• Interactive natural deduction proof editor. ~ Bob Atkey #Logic
• Local search algorithms in NetLogo. ~ F. Sancho #Netlogo
• Solving Sudoku via SAT with Mathematica. ~ M. Sottile #Logic #SAT #Mathematica
• Well-founded unions verified. ~ J. Dawson, N. Dershowitz & R. Goré #ITP #IsabelleHOL
• Variations on noetherianness. ~ D. Firsov, T. Uustalu & N. Veltri #ITP #Agda
• Verified construction of static single assignment form. ~ S. Buchwald, D. Lohner & S. Ullrich #ITP #IsabelleHOL
• The Cartan fixed point theorems in Isabelle/HOL. ~ L. Paulson #ITP #IsabelleHOL #Math #AFP
• Using AlphaGo as a theorem prover. #ATP #AI
• Beginner’s guide to the history of data science. ~ Hannah Augur #DataScience
• Blackstar: Raytracing black holes with Haskell. ~ Sakari Kapanen #Haskell
• Big Data ¿Qué es y cómo nos cambiará la vida? ~ M.A. Trabado #BigData
• Las ecuaciones más bellas de la historia de las matemáticas. ~ R. Pérez #Matemáticas
• Big Data y humanidades digitales: de la computación social a los retos de la cultura conectada. ~ S. Álvaro #BigData
• Formalising confluence in PVS. ~ Mauricio Ayala-Rincón #ITP #PVS
• WIMS (WWW Interactive Multipurpose Server) allows you to work on mathematics interactively via the Internet. ~ G. Xiao #Math
• COGENT: Verifying high-assurance file system implementations. ~ S. Amani et als. #ITP #Coq
• Peculiar pattern found in “random” prime numbers. ~ E. Lamb #Math
• Unexpected biases in the distribution of consecutive primes. ~ R.J. Lemke Oliver & K. Soundararajan #Math
• Propositional resolution and prime implicates generation in Isabelle/HOL. ~ N. Peltier #ITP #IsabelleHOL #Logic
• Haskell is the Dark Souls of programming. ~ Steve Shogren #Haskell
• Using the STM with Haskell. ~ Steve Severance #Haskell
• Guilloche (spirograph) patterns. ~ Ken Takusagawa #Haskell
• From Tarski to Descartes: Formalization of the arithmetization of euclidean geometry. ~ P. Boutry et als, #ITP #Coq #Math
• Reasoning about programs. ~ P. Manolios #ITP #ACL2
• Constructive analysis and experimental mathematics using the Nuprl proof assistant. ~ M. Bickford #ITP #Nuprl #Math
• SMT solving for functional programming over infinite structures. ~ B. Klin & M Szynwelski #Haskell
• An introduction to mechanized reasoning. ~ M. Kerber, C. Lange & C. Rowat #AR #ITP
• Random binary heaps, separable permutations, and numbers that multiply to factorials. ~ #Algorithmic
• The SAT revolution: solving, sampling, and counting ~ Moshe Y. Vardi [Slides] #Logic #CompSci
• Efficient binary serialization ~ M. Snoyman #Haskell
• Self-formalisation of Higher-Order Logic. ~ R. Kumar et als. #ITP #HOL4
• Optical quantum gates formalization in HOL Light. ~ S.M. Beillahi, M.Y. Mahmoud y S. Tahar #ITP #HOL_Light
• Static vs. dynamic functional languages ~ Sami Badawi #FP #Haskell #Lisp #Clojure #Scala
• Structure-aware version control (A generic approach using Agda). ~ V. Cacciari Miraldo & W. Swierstra #Agda #Haskell
• Markov chains and Markov decision processes in Isabelle/HOL. ~ J. Hölzl #IsabelleHOL
• Formally verified approximations of definite integrals. ~ A. Mahboubi et als. #ITP #Coq #Math
• Extensible domain specific languages. ~ C. Schmalhofer & A. Biehl #Haskell
• Hakaru: An embedded probabilistic programming language in Haskell. ~ #Haskell
• Case studies in constructive mathematics. ~ E. Parmann #PhD_Thesis #ITP #Coq #Math
• Extensible and efficient automation through reflective tactics. ~ G. Malecha & J. Bengtson #Agda
• The method “Model Elimination” of D.W.Loveland explained. ~ M. Lévy #Logic #ATP
• Un dérivateur formel Ocaml en 5 minutes. ~ G. Connan #Math #OCaml
• Computational thinking, 10 years later. ~ J.M. Wing #CompSci
• History and philosophy of types. ~ T. Petricek #Logic #CompSci
• Hoed: A lightweight Haskell tracer and debugger. ~ #Haskell
• Functional data validation using monads and applicative functors. ~ Gianmario Spacagna #Big_Data #FP #Scala
• Adventures in functional Big Data. ~ Matthew Eric Bassett #FP #Big_Data
• Learning data science using functional Python. ~ Joel Grus #Data_science #FP #Python
• Past, present and future of AI: a fascinating journey. ~ Ramón López de Mantaras #AI
• Probabilistic logic programming tutorial. ~ F. Riguzzi & G. Cota #Logic #Programming #Prolog

Abril 2016

• Towards formal proof metrics. ~ D. Aspinall & C. Kaliszyk #ITP
• Haskell for data science. ~ John Cant #Haskell #Data_science
• Haskell for data science. ~ Vladimir Alekseichenko [Video] #Haskell #Data_science
• Simple linear regression in Haskell. ~ Josh Walters #Haskell
• roshask: Haskell client library for the ROS robotics framework. ~ #Haskell #ROS
• Computabilidad, complejidad computacional y verificación de programas. ~ R. Rosenfeld y J. Irazábal #Libro #Computación
• Automating proofs. ~ Chris Edwards | Communications of the ACM #ATP
• Composing (music) in Haskell. ~ Stuart Popejoy [Video] #Haskell #Music
• Composing (music) in Haskell. ~ Stuart Popejoy [Slides] #Haskell #Music
• Haskell, startups, and domain specific languages. ~ Adam Wespiser [Video] #Haskell
• The Happstack book: Modern, type-safe Web development in Haskell. ~ Jeremy Shaw #Haskell #Web #Book
• (Co)induction: it’s a thing! ~ V. Robert #Logic
• Comparing unification algorithms in first-order theorem proving. ~ K. Hoder, A. Voronkov #Logic #Algorithms
• Descending sort in Haskell. ~ Roman Cheplyaka #Haskell
• Beyond Good and Evil (Formalizing the security guarantees of low-level compartmentalization). ~ Y. Juglaret et als. #ITP #Coq
• STM (Software Transactional Memory) in Haskell. ~ Steve Severance #Haskell
• Computing the uncomputable. ~ John Baez #Logic #Math #CompSci
• The logic of real and complex numbers. ~ John Baez #Logic #Math
• Correctness and concurrent complexity of the Black-White Bakery algorithm. ~ W.H. Hesselink #ITP #PVS
• The sym package: Definitions for permutations with an emphasis on permutation patterns and permutation statistics. ~ #Haskell #Math
• Au delà des réels: méthodes numériques en informatique. ~ G. Connan #Book #Math #Python
• Variations on noetherianness. ~ D. Firsov, T. Uustalu, N. Veltri #ITP #Agda #Math
• Introducing Haskell, functional abstraction and computation by calculation, reasoning about functional programs. ~ #Haskell
• Formal languages, formally and coinductively. ~ Dmitriy Traytel #IsabelleHOL
• MapReduce. ~ Junghoon Kang #MapReduce #Big_Data
• Matasano crypto challenges solutions in Haskell. ~ Christopher Blanchard #Haskell
• Desugaring Haskell’s do-notation into applicative operations. ~ S. Marlow et als. #Haskell
• Automatic predicate testing in formal certification (You’ve only proven what you’ve said, not what you meant!) ~ F. Slama #ITP
• ASlib: A benchmark library for algorithm selection. ~ B. Bischl et als. #Algorithms #Machine_learning
• Formalization of phase ordering. ~ T. Cogumbreiro, J. Shirako & V. Sarkar #ITP #Coq
• Algorithms, efficiency and complexity. ~ S. Kambhampati #Algorithms
• Algebrite: Computer Algebra System in Javascript. ~ #CAS #Math #Javascript
• (Hyper) sequent calculi for the ALC (S4) description logics. ~ J.P. Muñoz et als. #Logic #Programming #ML
• Functional programming vs. imperative programming. ~ #Programming
• Coeffects: Context-aware programming languages. ~ Tomas Petricek #Programming
• Full stack Lisp (Build and deploy modern Lisp applications). ~ P. Penev #Lisp
• Premiers pas avec Python. ~ H. Hounwanou #eBook #Python
• Datafun: a functional Datalog. ~ M. Arntzenius & N.R. Krishnaswami #PD #Logic #Racket
• Algorithmic composition: A gentle introduction to music composition using Common LISP and Common Music. ~ M. Simoni #Lisp #Music
• Functional models of Hadoop MapReduce with application to Scan. ~ K. Matsuzaki [Slides] #BigData
• Löb’s theorem (A functional pearl of dependently typed quining). ~ J. Gross, J. Gallagher, B. Fallenstein #ITP #Agda #Logic
• Worst practices should be hard. ~ G. Gonzalez #Haskell
• A brief tour of Haskell for Scala programmers. ~ Ed Conolly #Haskell #Scala
• Isotope: a chemistry library for calculating masses of elements and molecules. ~ Michael Thomas #Haskell #Chemistry
• On distributive AG-groupoids. ~ A. Khan et als. #ATP #Prover9 #Math
• Titato: Tic tac toe in Haskell. ~ Taylor Fausak #Haskell
• forallX: Cambridge (a textbook for introductory formal logic) ~ Tim Button #eBook #Logic
• Basic data analysis with CL without frameworks. ~ A. Kaygun #Lisp
• Mathematistan (The landscape of mathematics). ~ Martin Kuppe #Math
• A software methodology for compiling quantum programs. ~ T. Häner et als. #Haskell #Quantum_computing
• Various computer generated pictures and animations. ~ C. Oudard #Haskell #Gloss
• Machine learning and computer algebra. ~ Z. Huang #PhD_Thesis #ATP #MetiTarski #Math #ML
• Programación funcional: ADT, teoría de categorías, functores y monads. ~ A. Monsalve #Haskell
• El proceso de formalización de la lógica matemática (La crisis de la geometría euclídea). ~ B. Stonek #Lógica
• Consideraciones sobre la lógica y sobre el funcionamiento de la matemática. ~ B. Stonek #Lógica #Matemáticas
• Understanding typing judgments. ~ D. Elkins #Agda
• Usos prácticos de los monoides. ~ L. López #Haskell
• What will humans do when artificial intelligence can do everything? ~ Sally Painter #AI
• Alda: A music programming language for musicians. ~ #Clojure #Music
• Max subarray in Haskell. ~ D. Lettier #Haskell
• Why functional programming matters. ~ J. Hughes #FP
• Understanding functors, applicatives and monads. ~ A.Y. Bhargava #Haskell
• Haskell: GADTs y desarrollo Web. ~ A. Serrano #Haskell
• Who checks the checkers? (You won’t believe the answer to this one). ~ Z. Zhang et als. #ITP #Coq
• Composing bijections, surjections, and injections. ~ Noah Luck Easterly #Haskell
• Experiments on the construction of functions. ~ Alexander Vieth #Haskell
• A new method of verification of functional programs. ~ A.M. Mironov #Verification #FP
• Dynamic programming in Haskell. ~ Thomas Sutton #Haskell #Algorithms
• A machine-checked constructive metatheory of computation tree logic. ~ C. Doczkal #PhD_Thesis #ITP #Coq #Logic
• Hadron: Construct and run Hadoop MapReduce programs in Haskell. ~ #Haskell #MapReduce
• Formal Concept Analysis. ~ D. Fensel & F. Facca #FCA
• 1st Order Logic Formal Concept Analysis: from logic programming to theory. ~ L. Chaudron & N. Maille #FCA #Logic #Programming #ILP
• Proof-relevant pi-calculus. ~ R. Perera & J. Cheney #ITP #Agda
• Scientific computation and functional programming. ~ J. Karczmarczuk #Haskell #Physic
• learn-physics: Haskell code for learning physics. ~ S.N. Walck #Haskell #Physics
• Shine: Declarative graphics for the browser. ~ F. Gazzetta #Haskell #JavaScript
• 3 ways to generate lazy Fibonacci sequences in Clojure. ~ Y. Sharvit #Clojure
• An example with Dedekind cuts. ~ C. Mummert #Math #Algorithms
• Categories for programmers: Adjunctions. ~ B. Milewski #Haskell
• Lazy processing and optimization of discrete sequences. ~ J. Karczmarczuk #Haskell #Math
• Evaluating SMT solvers for software verification. ~ A. Healy et als. #SMT #Verification
• Beyond Clojure: Haskell. ~ Martin Trojer #Haskell #Clojure
• Implementing the game 2048 in less than 90 lines of Haskell. ~ Gregor Ulm #Haskell
• Clause selection in reolution-style theorem provers. ~ R. Veroff #ATP
• The most unreliable technique in the world to compute pi. ~ J. Karczmarczuk #Haskell #Math
• List and comprehension extensions. ~ A. Altman #Haskell
• The matrix cookbook (A desktop reference for quick overview of mathematics of matrices). ~ K.B. Petersen & M.S. Pedersen #eBook #Math
• The probability and statistics cookbook. ~ M. Vallentin #eBook #Math #Statistic
• Breadth-first numbering: Lessons from a small exercise in algorithm design (Functional pearl). ~ Chris Okasaki #Haskell
• Bombyard: a clone of the minesweeper game in Haskell. ~ T. Fausak #Haskell #Game #Gloss
• Functional differentiation of computer programs. ~ J. Karczmarczuk #Haskell #Math
• A verified and executable implementation of reduced ordered binary decision diagrams in Isabelle/HOL. ~ J. Michaelis et als. #IsabelleHOL
• Vers une théorie de l’intelligence. ~ J.P. Delahaye #AI
• Chemical computing with Clojure. ~ C. Meier #Clojure
• Data is code. ~ G. Gonzalez #Haskell
• Computing symbolic gradient vectors with plain Haskell. ~ Dan Aloni #Haskell #Math
• A Cantor trio: denumerability, the reals, and the real algebraic numbers. ~ R. Gamboa & J. Cowles #ITP #ACL2 #Math
• A formalisation of the Cocke-Younger-Kasami algorithm in Isabelle/HOL. ~ M. Bortin #ITP #IsabelleHOL
• A port of MiniPRL to Haskell with co-/inductive types bolted on the side. ~ T. Sutton #Haskell
• No faster-than-light observers (Using Isabelle/HOL to verify first-order relativity theory) ~ M. Stannett, I Németi #IsabelleHOL
• A Turing machine simulator written in Haskell. ~ N. Lochner #Haskell

Mayo 2016

• Formal verification of NTRUEncrypt scheme. ~ G.R. Moghissi, A. Payandeh #ITP #IsabelleHOL
• Structuring depth-first search algorithms in Haskell. ~ D.J. King, J. Launchbury #Haskell
• A formal exploration of Nominal Kleene Algebra. ~ P. Brunet, D. Pous #ITP #Coq #Logic
• MapReduce program synthesis. ~ C. Smith, A. Albarghouthi #MapReduce #Verification
• Haskell resources. ~ Mouna Cheikhna #Haskell
• A programming and problem-solving seminar. ~ J.D. Hobby & D.E. Knuth (1983) #Programming
• Gröbner bases theory in Isabelle/HOL. ~ F. Immler & A. Maletzky #ITP #IsabelleHOL #Math
• Notions of computation as monoids. ~ E. Rivas & M. Jaskelioff. #Haskell
• Functional data structures. ~ M. Ivanovié & V. Kumcak. #Haskell
• El problema de los tres caballeros y los tres criados ~ R. Ibáñez #Matemáticas #Computación
• Spivey’s generalized recurrence for Bell numbers in Isabelle/HOL. ~ L. Bulwahn #ITP #IsabelleHOL #Math #AFP
• Juega con el ordenador cuántico de IBM. ~ David Sarabia #Programación
• Randomised social choice theory in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL #AFP
• The incompatibility of SD-efficiency and SD-strategy-proofness in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL #AFP
• Uncertain: Manipulating numbers with inherent experimental/measurement uncertainty. ~ Justin Le #Haskell
• Knuth-Morris-Pratt algorithm for substring matching in Haskell. ~ Twan van Laarhoven #Haskell #Algorithm
• Aho–Corasick string matching algorithm. ~ #Algorithm
• Implementation of Aho-Corasick algorithm in Haskell. ~ #Haskell #Algorithm
• Solving and verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. ~ M.J.H. Heule et als. #ATP #SAT
• Liquid Haskell. ~ G. Gonzalez #Haskell
• Comparison of implementations of the Newton-Raphson in Python and Clojure. ~ #Python #Clojure #Math
• Combinat: A collection of functions to generate, manipulate, visualize and count combinatorial objects. ~ #Haskell #Math
• A formal proof of the max-flow min-cut theorem for countable networks. ~ A. Lochbihler #ITP #IsabelleHOL
• Some concepts from automata theory in Haskell. ~ Samuel Schlesinger #Haskell
• Category theory in Coq 8.5. ~ A. Timany, B. Jacobs #ITP #Coq
• User-defined literals in Haskell via QuasiQuotes. ~ Harry Garrood #Haskell
• Functional programming in practice. ~ M. Borkent #Scala #Haskell #Clojure
• A mathematical proof takes 200 terabytes to state. ~ M. James #ATP #SAT #Math
• Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. ~ M.J.H. Heule et als. #ATP #SAT
• An introduction to Moessner’s theorem and Moessner’s sieve. ~ P. Urbak #Haskell #Math
• A dual to Moessner’s sieve. ~ P. Urbak #Haskell #Math
• Formalizing graph theory and planarity certificates. ~ L. Noschinski #PhD_Thesis #Isabelle_HOL
• HLinear: Exact dense linear algebra in Haskell. ~ A. Ghitza & M. Westerholt-Raum #Haskell #Math
• A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory. ~ K.B. Hou et als. #ITP #Agda #HoTT
• A characteristic function of Moessner’s sieve ~ P. Urbak #Haskell #Math
• This Turing machine should run forever unless Maths is wrong. ~ J. Aron #Math #CompSci
• A relatively small Turing machine whose behavior is independent of set theory. ~ A. Yedidia & S. Aaronson #Math #CompSci
• Mindless, verified (erasably) coding using dependent types. ~ Jonathan Leivent #Coq #Algorithms
• Mindless, verified (erasably) coding using dependent types, phase 2. ~ Jonathan Leivent #Coq #Algorithms
• Rank-balanced trees. ~ B. Haeupler, S. Sen & R.E. Tarjan. #Algorithms
• A Haskell to JVM compiler that supports GHC Haskell. ~ Rahul Muttineni #Haskell #Java
• Computer Algebra Library for Chez Scheme (R6RS). ~ #Scheme #CAS
• Números y hoja de cálculo: Rachas de dígitos. ~ Antonio Roldán #Matemáticas #Programación
• Functional modelling of musical harmony: An experience report. ~ J.P. Magalhaes & W.B. de Haas #Haskell
• Verified functional programming in Agda. ~ A. Stump #eBook #Agda #FP #Logic #Programming
• Algorithms for bayesian networks. ~ @alpheccar #Haskell
• Automated theorem proving in a first-order logic with first class boolean sort. ~ E. Kotelnikov #ATP #Logic
• Flag-based big-step semantics. ~ C.B. Poulsen & P.D. Mosses #Coq
• MendellianGenetics: Project for simulating Mendel’s genetics. Written in Haskell. ~ #Haskell #Genetics
• Simplified Common Lisp reference. ~ Jakub Trávník #Lisp
• The evolution of a Haskell programmer. ~ F. Ruehr #Haskell
• A Haskell reading list. ~ S. Diehl #Haskell
• Automatic propagation of uncertainty with AD. ~ Justin Le #Haskell
• Formalization of quantum protocols using Coq. ~ J. Boender, F. Kammüller & R. Nagarajan #Coq
• Implementing programming languages. ~ A. Ranta #eBook #Programming
• Learn you an Agda and achieve enlightenment! ~ Liam O’Connor-Davis #Agda
• Haskell design patterns: .Extended modules. ~ Jasper Van der Jeugt #Haskell
• Plastelina interactive logic games. ~ #Logic #Game
• Loopless gray code enumeration and the tower of Bucharest. ~ F. Herter & G. Rote #Algorithms #Python
• Lightweight higher-order rewriting in Haskell. ~ E. Axelsson & A. Vezzosi #Haskell
• Towards a theory of reach. ~ J. Fowler & G. Huttom #Haskell
• Type class instances for type-level lambdas in Haskell. ~ T. Alkemade & J. Jeuring #Haskell
• Structure and interpretation of classical mechanics. ~ G.J. Sussman, J. Wisdom & M.E. Mayer #Scheme
• Communicating mathematics: Useful ideas from computer science- ~ C. Wells #Math #CompSci #Teaching
• DSLsofMath: Domain specific languages of mathematics. ~ #Haskell #Math
• Programmable signatures. ~ A. Persson & E. Axelsson #Haskell
• Functional differential geometry. ~ G.J. Sussman, J. Wisdom & W. Farr #FP #Scheme
• The world’s first artificially intelligent lawyer gets hired. ~ C. Weller #AI
• Perron-Frobenius theorem for spectral radius analysis in Isabelle/HOL. ~ J. Divasón et als. #IsabelleHOL
• Simple balanced binary search trees. ~ P. Ragde #Haskell
• Sequence implementations in Haskell. ~ P.R. Borges #Haskell
• Axioms for modelling cubical type theory in a topos. ~ I. Orton & A.M. Pitts #ITP #Agda
• Introduction to literate programming. ~ H. Abrams #Programming #Emacs #Clojure
• Why GNU Emacs? ~ rekado #Emacs
• Emacs support library for PDF files. ~ #Emacs #PDF
• Compass-free navigation of mazes. ~ P. Scott & J. Fleuriot #ITP #HOL_Light
• CodeWorld’s big decisions. ~ C. Smith #Haskell #Teaching #CodeWorld
• Bootstrap: a curriculum for students ages 12–16, teaching algebraic concepts through coding. ~ #Teaching #CompSci #Math
• Bootstrap curriculum. ~ Wikipedia #Teaching #CompSci #Math
• WeScheme: an online programming environment based on DrRacket and Scheme. ~ #Racket #Scheme
• Games from basic data structures. ~ M. Bovee, K. Burke & C. Tennenhouse #Games #Data_structures #Algorithms
• Modeling data with functional programming in R. ~ Brian Lee Yung Rowe #Data_Science #FP
• The joy and agony of Haskell in production. ~ S. Diehl #Haskell
• Functional programming with structured graphs. ~ B.C.d.S. Oliveira & W.R. Cook #Haskell
• A modular way to reason about iteration. ~ J.C. Filliätre & M. Pereira #Why3
• Formal verification of real-time function blocks using PVS. ~ L. Pang et als. #ITP #PVS
• Refinement based verification of imperative data structures. ~ P. Lammich #ITP #IsabelleHOL
• Practical dependent types in Haskell: Type-safe neural networks (Part 1). ~ Justin Le #Haskell
• A practical Template Haskell tutorial. ~ #Haskell
• Specification and proof of high-level functional properties of bit-level programs. ~ C. Fumex et als. #Why3
• Mathematics is applied by everyone except applied mathematicians ~ David P. Wilson #Math
• ¿Matemáticas para la industria, matemáticas de segunda? ~ Mikel Lezaun #Matemáticas
• Deductive evaluation: formal code analysis with low user burden. ~ B.L. Di Vito #PVS
• Emacs org-mode examples and cookbook. ~ Eric Neilsen #Emacs
• Two-hundred-terabyte maths proof is largest ever (A computer cracks the Boolean Pythagorean triples problem — but is it really maths?) ~ E. Lamb #Math #CompSci
• Philosophical questions about programming. ~ Tomas Petricek #Programming
• The matrix reproved (Verification Pearl). ~ M. Clochard, L. Gondelman & M. Pereira #Why3 #Math
• Producing all ideals of a forest, formally (verification pearl). ~ J.C. Filliâtre & M. Pereira #Why3
• Formal verification of the rank algorithm for succinct data structures. ~ A. Tanaka, R. Affeldt & J. Garrigue #Coq #BigData
• CSV encoding and decoding in Haskell with Cassava. ~ J.P. Villa #Haskell #Data_Science

Junio 2016

• MathCheck2: A SAT+CAS verifier for combinatorial conjectures. ~ C. Bright et als. #SAT #CAS #Math
• Proof assistants as a routine tool? ~ Neil Strickland #ITP
• ¿Esto es Matemáticas? (¿Pueden los ordenadores realizar demostraciones matemáticas?) ~ Manuel de León #Matemáticas #Computación
• An introduction to scientific Python (and a bit of the maths behind it) - Pandas. ~ J. Moir #Python #DataScience
• A very general method of computing shortest paths. ~ Russell O’Connor #Haskell
• Cardinality of equivalence relations in Isabelle/HOL. ~ L. Bulwahn #ITP #IsabelleHOL #AFP
• Conjugate partitions. ~ A. Kaygun #Lisp #Math
• Computer experiments are transforming mathematics. ~ E. Klarreich. #Math #CompSci
• Mechanizing proofs about Mendler-style recursion. ~ R. Jacob-Rao, A. Cave & B. Pientka #Coq
• Using real projects as motivators in programming education. ~ M. Konecki, S. Lovrenčić & M Kaniški #Programming
• Recursion to iteration, part 1: The simple method, secret features, and accumulators. ~ Tom Moertel #Python
• Functional binomial queues. ~ D.J. King #Haskell #Algorithms
• A simple implementation technique for priority search queues. ~ R. Hinze #Haskell #Algorithms
• Does this drone sport the World’s most secure OS? ~ Jeremy Kirk #sel4 #Verification
• Towards verified construction for planar class of a qualitative spatial representation. ~ S. Moriguchi et als. #ITP #Coq
• ODE solver as a functional fold. ~ J.D. Cook #Haskell #Math
• Abstract algebra for Scala. ~ #Scala
• How programming supports math class, not the other way around. ~ C. Bartlo #Programming #Math
• Perspectives for proof unwinding by programming languages techniques. ~ D. Ilik #Logic #Math #CompSci
• EdisonAPI: A library of efficient, purely-functional data structures (API). ~ Chris Okasaki #Haskell
• Rex: A Haskell quasi-quoter for typeful results of regex captures. ~ M. Sloan #Haskell
• Software foundations, version 4.0 (May 2016). ~ Benjamin C. Pierce et als. #Coq #Logic #CompSci
• Haskell style guide. ~ J. Tibell #Haskell
• Formalization of normal random variables. ~ M. Qasim #ITP #HOL
• nanoCoP: A non-clausal connection prover. ~ J. Otten #ATP #Logic #Prolog #CompSci
• Google moves closer to a universal quantum computer. ~ P. Ball #CompSci
• Why are so many mathematicians also musicians? ~ D.H. Bailey & J.M. Borwein #Math #Music
• Experimental computation and visual theorems: Part I: the computer as collaborator. ~ J.M. Borwein #Math #CompSci
• Experimental computation and visual theorems: Part III. walking on numbers. ~ J.M. Borwein #Math #CompSci
• First experimental demonstration of a quantum Enigma machine. ~ MIT Technology Review #CompSci
• Distributed systems in Haskell. ~ Will Yager #Haskell
• Coq’Art, CPDT and SF: a review of books on Coq proof assistant. ~ J. Stolarek #ITP #Coq
• Chi-square goodness of fit test example with primes. ~ J. Cook #Math #Python
• Haskell Tutorials, a tutorial. ~ Yann Esposito #Haskell
• Create a game with Haskell. ~ #Haskell #Game
• Formalizing semantic bidirectionalization with dependent types. ~ H. Grohne, A. Löh & J. Voigtländer #ITP #Agda
• Insertion sort implemented as a fold. ~ J. Cook #Haskell
• Computing higher moments with a fold. ~ J. Cook #Haskell #Statistics
• Tools for thought. ~ Howard Rheingold #eBook #CompSci
• A tool for thought. ~ David Nolen #ClojureScript
• Algo pasa con Haskell. ~ @__josejuan__ #Haskell
• A complete tutorial to learn data science in R from scratch. ~ Manish Saraswat #Rstats #DataScience
• Formally verified countermeasures against cache based attacks in virtualization platforms. ~ J. Campo #PhD_Thesis #Coq
• Mastering programming. ~ Kent Beck #Programming
• Analysing big time-series data in the cloud. ~ T. Petricek #Fsharp #BigData
• Formal methods for secure software construction. ~ B. Goodspeed #Idris
• Haskell programming from first principles - Follow-up resources ~ Peter Bhat Harkins #Haskell
• HGeometry: Geometric algorithms, data structures, and data types. ~ Frank Staals #Haskell #Math
• Proving type class laws for Haskell. ~ A. Arvidsson, M. Johansson & R. Touche #Haskell
• FizzBuzz in Haskell by embedding a domain-specific language. ~ M. Piróg #Haskell
• The Recamán sequence. ~ Brent Yorgey #Math
• Queueing and glueing for optimal partitioning (Functional Pearl). ~ S.C. Mu, Y.H. Chiang & Y.H. Lyu #Algorithms #Haskell
• Sequent calculus as a compiler intermediate language. ~ Simon Peyton Jones et als. #Logic #Haskell
• The story of Haskell at IMVU. ~ Chad Austin #Haskell
• Reachability, confluence, and termination analysis with state-compatible automata. ~ B. Felgenhauer & R. Thiemann #Isabelle/HOL
• A survey of satisfiability modulo theory. ~ D. Monniaux #ATP #SMT
• ASCII art diagrams in Emacs org-mode. ~ J.D. Cook #Emacs
• Designing functional implementations of graph algorithms. ~ N. Danilenko #Haskell #Algorithms #Math
• Formal methods for secure software construction. ~ B. Goodspeed #Idris
• Contribution of Warsaw logicians to computational logic. ~ D. Niwiński #Logic #CompSci
• Implementing graph grammars for intelligence analysis in OCaml. ~ R. Moten, K. Anyanwu-Ogan & S. Miranshah #OCaml
• A visual guide to graph traversal algorithms. ~ #Algorithms
• A fully automatic theorem prover with human-style output. ~ M. Ganesalingam & W.T. Gowers #ATP #Haskell #Math #CompSci
• Introducción a la demostracción asistida por ordenador con Isabelle/HOL. ~ J.A. Alonso #Isabelle_HOL
• Programs and proofs (Mechanizing Mathematics with dependent types). ~ I. Sergey #Coq
• Visual theorem proving with the Incredible Proof Machine. ~ J. Breitner #Logic #ITP
• Theory in the time of Big Data (What is the role of theory today?) ~ R.J. Lipton & K.W. Regan #Teaching #CompSci
• Teaching Theory in the time of Data Science/Big Data. ~ A.C. Gilbert & A. Rudra #Teaching #CompSci
• A formal proof of Cauchy’s residue theorem. ~ W. Li & L.C. Paulson #ITP #IsabelleHOL #Math
• The formalization of discrete Fourier transform in HOL. ~ Z. Shi et als. #ITP #HOL #Math
• Automatic functional correctness proofs for functional search trees. ~ T. Nipkow #ITP #IsabelleHOL
• Formalizing the Edmonds-Karp algorithm. ~ P. Lammich & S.R. Sefidgar #ITP #IsabelleHOL
• Regular expressions implemented in Haskell ~ G. Gonzalez #Haskell
• Two-way automata in Coq. ~ C. Doczkal & G. Smolka #ITP #Coq
• Getting started with GHCJS dev. ~ David Johnson #Haskell #JavaScript #GHCJS
• Teaching machines to predict the future. ~ MIT News #CompSci
• Hereditarily finite sets in constructive type theory. ~ G. Smolka & K. Stark #ITP #Coq #Math
• An Isabelle/HOL formalisation of Green’s theorem. ~ M. Abdulaziz & L.C. Paulson #ITP #IsabelleHOL
• An introductory talk to functional programming & typeclasses. ~ R. Raja http://bit.ly/2917wGS #FP #Scala
• A dependent security type system for concurrent imperative programs. ~ T. Murray et als. #ITP #IsabelleHOL #AFP
• Usar mónadas es mucho más fácil de lo que crees, empezando con la programación funcional.~ @__josejuan__ #Haskell
• The secret spiritual history of calculus (Integral calculus originated in a 17th-century debate that was as religious as it was scientific). ~ A. Alexander #Math
• Why software startups should hire functional programmers. ~ Martijn Rutten #FP #Haskell
• A tutorial implementation of Hindley-Milner type inference (Algorithm W) in Haskell. ~ http://bit.ly/293vemQ #Haskell
• Cardinality of multisets in Isabelle/HOL. ~ L. Bulwahn #ITP #Math #IsabelleHOL #AFP
• Proving divide and conquer complexities in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL
• Paradigmas de programación: programación imperativa y programación declarativa. ~ @LoopaDev #Programación
• Parallel combinatorics. ~ J. Aranda #Haskell #Math
• Manual de cálculo científico en SageMath. ~ A. Aceña, J. Armijos y M. Llerena #SageMath
• Spock: a lightweight Haskell web framework. ~ #Haskell
• Importancia de la programación funcional en un mundo paralelo. ~ @LoopaDev #Programación #PF

Julio 2016

• The resolution calculus for first-order logic in Isabelle/HOL. ~ A. Schlichtkrull #ITP #Isabelle/HOL #Logic
• IsaFoL: Isabelle Formalization of Logic. ~ #ITP #Isabelle/HOL #Logic
• CodeWorld for younger ages! ~ C. Smith #Haskell #Teaching #CodeWorld
• Blocks for CodeWorld. ~ #Haskell #Teaching #CodeWorld
• Translating Scala programs to Isabelle/HOL. ~ L. Hupel & V. Kuncak #IsabelleHOL #Scala
• Qué hace un tipo de sistemas cuando se le cae todo el sistema. ~ Javier Pastor #Programación
• OpenDreamKit: Open Digital Research Environment Toolkit for the Advancement of Mathematics. ~ #MKM #Math #CompSci
• Finding proofs in Tarskian geometry. ~ M. Beeson & L. Wos #ATP #OTTER #Math
• Automating free logic in Isabelle/HOL. ~ C. Benzmüller & D. Scott #ITP #IsabelleHOL
• 15 free Haskell books & tutorials to help you learn the Haskell programming language. ~ Hacker Lists #Haskell
• Programs and proofs (Mechanizing mathematics with dependent types). ~ Ilya Sergey #ITP #Coq #Math #eBook
• Common Lisp ecosystem and the software distribution model. ~ D. Kochmański #Lisp
• Verified computer linear algebra. ~ J. Aransay & J. Divasón #ITP #IsabelleHOL #Math
• Category theory for the sciences. ~ David Spivak #eBook #Math #CompSci
• A tutorial on the universality and expressiveness of fold ~ G. Hutton #Haskell
• Functional geometry. ~ Peter Henderson #FP
• Functional geometry in julia notebook demo. ~ S. Gowda #Julia
• A formalizing of Berlekamp’s factorization algorithm. ~ J. Divasón et als. #ITP #IsabelleHOL #Math
• A framework for verifying depth-first search algorithms in Isabelle/HOL. ~ P. Lammich & R. Neumann #ITP #IsabelleHOL
• Four months with Haskell. ~ Alexis King #Haskell
• Original Apollo 11 guidance computer source code, in assembly, for Command Module and Lunar Module. ~ #Programming
• Arithmetic coding with folds and unfolds. ~ R. Bird & J. Gibbons #Haskell
• Eastman maximal comma-free codes in Haskell. ~ Brent Yorgey #Haskell
• The Isar proof language in 2016. ~ Makarius Wenzel #IsabelleHOL
• Abstract nonsense for functional programmers (a introduction to category theory). ~ Edsko de Vries #Haskell
• Optimal purely functional priority queues (1996). ~ G.S. Brodal & C. Okasaki #Algoritm #FP #ML
• Tackling intractable computing problems. ~ Aaron Dubrow #CompSci
• Literate programming: presenting code in human order ~ J.D. Cook #Programming
• Aprende Haskell rápido y difícil. ~ Y. Esposito & D. Campoverde #Haskell #Tutorial
• List of incomplete published mathematical proofs. ~ Wikipedia #Math
• Graph algorithms. ~ Wikipedia book #eBook #Algorithms #Math
• From Hilbert to Tarski. ~ G. Braun, P. Boutry & J. Narboux #ITP #Coq #Math
• Purely functional incremental computing. ~ D. Firsov & W. Jeltsch #Haskell
• Formalizing the Edmonds-Karp algorithm in Isabelle/HOL. ~ P. Lammich, S.R. Sefidgar #ITP #IsabelleHOL
• Haskell Hero: un manual interactivo del lenguaje Haskell para principiantes. ~ S. Novák #Haskell
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. ~ J. Aransay & J. Divasón #IsabelleHOL
• On the formalization of some results of context-free language theory. ~ M.V.M. Ramos et als. #ITP #Coq
• Formalization of context-free language theory. ~ M.V.M. Ramos #PhD_Thesis #ITP #Coq
• Dive into GHC: intermediate forms. ~ S. Diehl #Haskell
• Org-Mode and writing papers: some tips. ~ C.R. Donley #Emacs #LaTeX
• Verified functional algorithms (Volume 3 of the software foundations series). ~ A.W. Appel #Coq
• Extensiones de bases de datos relacionales y deductivas: fundamentos teóricos e implementación. ~ G. Aranda #Tesis #PL
• El zen de Javascript: a la búsqueda de la armonía del código. ~ C. Benítez #Programación #JavaScript
• Verification of an LCF-style first-order prover with equality. ~ A.B. Jensen et als. #ITP #IsabelleHOL #Logic
• A proof of the compositions of time interval relations. ~ F. Ghourabi & K. Takahashi #ITP #IsabelleHOL
• Doing data science with Clojure. ~ #Data_Science #Clojure
• The joy of programming to learn. ~ Eric Normand #Programming
• Scala is the new golden child. ~ Chris McKinlay #Scala
• Graphs: a balancing act. ~ Francesco Mazzoli #Haskell #Gloss
• Graph problems and vector-matrix multiplications in Haskell. ~ N. Danilenko #Haskell #Math
• All sorts of permutations (Functional Pearl). ~ J. Christiansen, N. Danilenko, S. Dylus #Haskell
• A rule based approach to teach mathematics using animation. ~ N. Sharaf, S. Abdennadher, T. Frühwirth #CHR #Prolog
• Threading the Arduino with Haskell. ~ M. Grebe & A. Gill #Haskell
• Using DSLs to help people solve rule-based problems. ~ N. Naus & J. Jeuring #Clean
• The surprise paradox in Isabelle/HOL. ~ J. Breitner #ITP #IsabelleHOL #Logic
• Generating random planar graphs. ~ P. Vasconcelos #Haskell #QuickCheck
• Verification of optimised 48-bit multiplications on AVR. ~ J. Schmaltz & P. Schwabe #ACL2
• Proving type class laws for Haskell. ~ A. Arvidsson, M. Johansson & R. Touche #Haskell
• Numbers aplenty: Interesting natural numbers and their properties. ~ #Math
• Logic programming with graph automorphism: Integrating nauty with Prolog (a tool paper). ~ M. Frank & M. Codish #Prolog
• Recursion schemes, part III: folds in context. ~ P. Thomson #Haskell
• Algebraic patterns: Semigroup. ~ P. Nilsson #Haskell
• A formally verified proof of the central limit theorem. ~ J. Avigad, J. Hölzl & L. Serafin #ITP #IsabelleHOL #Math
• Test data generators. ~ K. Claessen #Haskell #QuickCheck
• Efficient R programming (A practical guide to smarter programming). ~ C. Gillespie & R. Lovelace #Rstats #DataScience
• Constructive Galois connections: Taming the Galois connection framework for mechanized metatheory. ~ D. Darais & als. #Coq
• Haskell operator tutorial. ~ M. Snoyman #Haskell
• FitSpec: refining property sets for testing Haskell programs. ~ R. Matela #Haskell
• A Haskell Cheat Sheet. ~ R. Matela http://bit.ly/2a7sDYX #Haskell
• A Haskell Typeclasses Cheat Sheet. ~ R. Matela http://bit.ly/2a7sDYX #Haskell
• Git magic. ~ Ben Lynn #Git #eBook
• Three approaches to monads. ~ Lawrence Evans #Haskell
• The mechanization of mathematics. ~ M. Beeson [Slides] #ATP #ITP #Math
• The mechanization of mathematics ~ M. Beeson #ATP #ITP #Math
• Datafun: a functional datalog. ~ M. Arntzenius & N.R. Krishnaswami #Racket #Prolog
• La programación funcional y las arquitecturas multicore: estado del arte. ~ J.G. Hoyos y A. Puertas #PF
• Property testing using QuickCheck. ~ P. Vasconcelos #Haskell #QuickCheck
• A brief intro to QuickCheck. ~ Stuart Gunter #Haskell #QuickCheck
• Modular verification for computer security. ~ Andrew W. Appel #Verification
• Deriving a probability density calculator (Functional Pearl). ~ W.M. Ismail & C.C. Shan #Haskell
• Proust: a nano proof assistant. ~ P. Ragde #Racket #Logic
• The Lax-Milgram theorem. A detailed proof to be formalized in Coq. ~ F. Clément & V. Martin #Math #Coq
• Análisis de desempeño de HASKELL en la ejecución de algoritmos paralelizados con primitivas. ~ A. Puertas y J.G. Hoyos #Haskell
• Parallel evaluation strategies for lazy data structures in Haskell. ~ P. Totoo #Haskell #PhD_Thesis
• The most important idea in Computer Science. ~ E. Normand #CompSci #Lisp #Turing
• The magic of abstraction ~ E. Normand #Programming
• Soundly proving B method formulae using typed sequent calculus. ~ P. Halmagrand #Zenon
• Ghostbuster: A tool for simplifying and converting GADTs. ~ T.L. McDonell & als. #Haskell
• Principles of programming languages. ~ M. Grant, Z. Palmer y S. Smith #Programming #OCaml #eBook
• Proving correctness of a compiler using step-indexed logical relations. ~ L. Rodrı́guez, M. Pagano & D. Fridlender #Coq
• Queueing and glueing for optimal partitioning (Functional Pearl). ~ S.C. Mu & als. #Algorithms #Haskell
• Constructive geometry and the parallel postulate. ~ Michael Beeson #Math #eBook
• Proof and computation in geometry. ~ Michael Beeson #Math #Otter
• Web meme generator: A web application for creating memes from pictures. ~ #Haskell
• Aterrizando en la programación funcional. ~ @__josejuan__ #Programación #PF #Haskell
• Refinement through restraint: bringing down the cost of verification. ~ L. O’Connor & als. #IsabelleHOL
• Mathematical logic and computers (Some interesting examples). ~ Michael Beeson #Logic #ATP #Otter
• Automating change of representation for proofs in discrete mathematics. ~ D. Raggi, A. Bundy, G. Grov, A. Pease #IsabelleHOL
• String diagrams for free monads (Functional Pearl). ~ M. Piróg & N. Wu #Haskell
• Criptografía desde el punto de vista de la programación funcional. ~ D. Rodríguez #Haskell #TFG
• Análisis formal de conceptos desde el punto de vista de la programación funcional. ~ M. Najarro #Haskell #TFG
• HGE2D: 2D game engine written in Haskell. ~ Martin Buck #Haskell #Games
• Exception safety. ~ Haskell-lang.org #Haskell #Tutorial
• A literate program implementing the microKanren relational programming language. ~ seantalts #Haskell
• High-performance client-side web applications through Haskell EDSLs. ~ A. Ekblad #Haskell
• Relation-algebraic verification of Prim’s minimum spanning tree algorithm. ~ W. Guttmann #ITP #IsabelleHOL
• Lazy graph processing in Haskell. ~ P. Dexter, Y. Liu & K. Chiu #Haskell
• Un viaje a la historia de la informática. ~ #Informática #Historia
• Using programming to teach mathematics. ~ A. Cangiano #Math #Programming

Agosto 2016

• Modularity in Mathematics. ~ J. Avigad #Math #CompSci
• Quick specifications for the busy programmer. ~ N. Smallbone et als. #Haskell #QuickSpec
• Sistema de tipos en Haskell. ~ Daniel Mery #Haskell
• Puzzle solving in Haskell. ~ Nicolas Mattia #Haskell
• Cryptographic block ciphers in functional programming: A case study on Feldspar and AES. ~ Gregor Ulm #Haskell
• Code generation for a simple first-order prover. ~ J. Villadsen et als. #IsabelleHOL #SML
• A calculus for variational programming. ~ S. Chen, M. Erwig & E. Walkingshaw #Haskell
• Zero knowledge proofs for NP. ~ Jeremy Kun #Logic
• Behavior-driven development (BDD) in Haskell with Hspec. ~ J.Carlos Pazmiño #Haskell #Hspec #BDD
• Beginner’s Luck (A language for property-based generators). ~ L. Lampropoulos et als. #Haskell
• How to twist pointers without breaking them. ~ S. Chauhan, P.P. Kurur & B.A. Yorgey #Haskell
• Catamorphisms in 15 minutes! ~ C. Jones #Haskell #Math
• Example driven development. ~ W. Hughes #Emacs #Programming
• Report on the NSF workshop on formal methods for security. ~ S. Chong et als. #Formal_methods
• Why writing correct software is hard … and why math (alone) won’t help us. ~ #CompSci #Math
• Formalized timed automata. ~ S. Wimmer #IsabelleHOL
• Functional reactive programming, refactored. ~ I. Perez, M. Bärenz & H. Nilsson #Haskell
• Guilt free Ivory. ~ T. Elliott et als. #Haskell
• A tool for the automatic generation of logical models of order-sorted first-order theories ~ R. Gutiérrez et als.#Logic
• AGES: a tool for generate logical models, for use with order-sorted first order logic. ~ #Haskell
• Consistent consequences formalized. ~ M. van Delft #ITP #Coq
• Calculating functional programs. ~ J. Gibbons #Haskell
• Playing with Mersenne numbers. ~ A. Cangiano #Math #Python
• Ptolemy’s theorem in Isabelle/HOL. ~ L. Bulwahn #ITP #IsabelleHOL #Math #AFP
• Formally verified complexity analysis of a functional language. ~ S. Wimmer #IsabelleHOL
• Holophrasm: a neural automated theorem prover for higher-order logic. ~ D. Whalen #ATP
• Comonads and day convolution. ~ Phil Freeman #Haskell
• The early development of programming languages. ~ D.E. Knuth & L.T. Pardo #Programming #History
• A decision procedure for univariate real polynomials in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL #Math
• Functional programming and intelligent algorithms. ~ Hans Georg Schaathun #Haskell #AI
• Interactive proofs in higher-order concurrent separation logic. ~ R. Krebbers et als. #ITP #Coq
• Safe zero-cost coercions for Haskell. ~ J. Breitner et als. #Haskell
• Towards a verifiable topology of data. ~ L. Lambán, F.J. Martín, J. Rubio & J.L. Ruiz pp. 113-116. #ACL2
• Foundations of mathematics: reliability and clarity: the explanatory role of mathematical induction. ~ J.T. Baldwin #Math
• A formal, resource consumption-preserving translation of actors to Haskell. ~ E. Albert et als. #Haskell
• Declare and access tuple fields with labels. ~ @christopherdone #Haskell
• Formal availability analysis using theorem proving. ~ W. Ahmed & O. Hasan #HOL4
• Λ◦λ : Functional lattice cryptography. ~ C. Peikert & E. Crockett #Haskell
• Overview of ExCAPE (Expeditions in Computer Augmented Program Engineering). ~ R. Alur #Programming
• Scaling up superoptimization. ~ P. Phothilimthana #Programming
• Inductive functional programming. ~ U. Schmid #Programming
• Leon: an automated system for verifying, repairing, and synthesizing functional scala programs. ~ #Scala
• The calculus of computation: decision procedures with applications to verification. ~ A. Bradley & Z. Manna #Logic
• Synthesis, analysis, and verification. ~ V. Kuncak & O. Lhotak #Compsci
• Software synthesis using automated reasoning. ~ R. Piskac #ATP
• Example-directed synthesis: a type-theoretic interpretation. ~ J. Frankle et als. #Programming
• Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. ~ I. Sergey et als. #Coq
• Type-and-example-directed program synthesis. ~ S. Zdancewic #Programming
• Myth: type-and-example-driven program synthesis for functional programming languages. ~ Peter-Michael Osera #Ocaml
• A theoretician’s guide to the experimental analysis of algorithms. ~ D.S. Johnson #Algorithms
• Certified context-free parsing: a formalisation of valiant’s algorithm in Agda. ~ J.P. Bernardy & P. Jansson #Agda
• Programming languages for pre-mechanical calculating tools. ~ B. Mélès #CompSci #Math
• Implementing hol in an higher order logic programming language. ~ C. Dunchev et als. #Logic #λProlog
• Deriving Moessner’s sieve from Horner’s method. ~ P. Urbak #Haskell #Math
• Lazy depth-first search and linear graph algorithms in Haskell. ~ D.J. King & J. Launchbury #Haskell
• Formalized linear algebra over elementary divisor rings in Coq. ~ G. Cano et als. #ITP #Coq #Math
• Free delivery (Functional pearl). ~ Jeremy Gibbons #Haskell
• CoSMed: A confidentiality-verified social media platform. ~ F. Raimondi et als. #IsabelleHOL
• mySQL-Haskell: a MySQL driver written entirely in Haskell. ~ winterland1989 #Haskell
• On Tarski’s axiomatic foundations of the calculus of relations. ~ H. Andréka, S. Givant, P. Jipsen, I. Németi #Mace4
• Aplicative programming with naperian functors. ~ J. Gibbons #Haskell
• mueval: A secure sandboxed Haskell interpreter for pure function evaluation. ~ @gwern #Haskell
• A grid of Moessner triangles. ~ P. Urbak #Haskell #Math
• Propositions as types generalised: The Rosetta Stone ~ P. Wadler #Programming
• Lecture notes on spectral graph methods. ~ M.W. Mahoney #Math
• MagicHaskeller: Automatic inductive functional programmer by systematic search. ~ #Haskell
• How to read a scientific paper. ~ S. Keshav #Research
• How to implement an algorithm from a scientific paper. ~ Emmanuel Goossaert #Programming
• Physics, topology, logic and computation: A Rosetta stone. ~ J.C. Baez & M. Stay #CompSci
• Reasoner-aid research: potentials and popularity. ~ S. Wang #ATP #ITP
• Haskell relational record (A pragmatic embedded system for type-safe and composable SQL queries). ~ K. Hibino et als. #Haskell
• Practical probabilistic programming with monads. ~ A. Scibior #Haskell
• Beautiful Racket: learn how to make your own programming languages with Racket (and why). ~ M. Butterick #Racket
• Rosette: solver-aided programming language that extends Racket for program synthesis, verification, and more. ~ #Rosette #Racket
• Certified derivative-based parsing of regular expressions. ~ R. Lopes, R. Ribeiro, C. Camarao #Idris
• Pattern synonyms. ~ M. Pickering, G. Érdi, S.P. Jones & R.A. Eisenberg #Haskell
• Taint analysis for system-wide privacy audits: a framework and real-world case studies. ~ M. von Maltitz et als. #IsabelleHOL
• Revisiting software transactional memory in Haskell1. ~ M. Le, R. Yates & M. Fluet #Haskell
• Formal semantics of firewalls in Isabelle/HOL. ~ C. Diekmann #IsabelleHOL
• Formalisation and execution of Linear Algebra: theorems and algorithms. ~ J. Divasón #PhD_Thesis #ITP #IsabelleHOL #Math
• Haskell for beginners. ~ J. Moronuki #Haskell
• Analyzing programs with Z3. ~ T. Jelvis #Haskell #Z3 #SMT
• Functional reactive programming. ~ T. Jelvis #FRP #Haskell
• QuickCheck testing for fun and profit. ~ J. Hughes #Haskell #QuickCheck
• A formal study of Moessner’s sieve. ~ P. Urbak #ITP #Coq #Math
• Modeling communication network requirements for an integrated clinical environment in PVS. ~ C. Bernardeschi et als. #PVS
• Inductive graphs. ~ T. Jelvis #Haskell
• Simple firewall in Isabelle/HOL. ~ C. Diekmann, J. Michaelis & M. Haslbeck #IsabelleHOL #AFP
• Thinking with laziness. ~ T. Jelvis #Haskell
• Verified analysis of algorithms for the list update problem. ~ M. Haslbeck #MsC_Thesis #IsabelleHOL
• Reading code with Emacs: controlling what’s displayed. ~ Nat Knight #Emacs
• Functional programming by example. ~ c. rodrigues #haskell #ocaml #scheme #clojure
• Algorithms for reduced ordered binary decision diagrams (for Isabelle/HOL). ~ J. Michaelis et als. #IsabelleHOL #AFP
• The benefits (not features!) of programming with Haskell. ~ Robb Shecter #Haskell
• Formalising in Isabelle/HOL a simplicial model for homotopy type theory: a naive approach. ~ J. Aransay et als. #IsabelleHOL
• Should i do that? using relational reinforcement learning and declarative programming to discover domain axioms. ~ #ASP #Prolog
• Automating black-box property based testing. ~ Jonas Duregård #Phd_Thesis #Haskell
• Comment Haskell a changé ma vision de développeur sur de nombreux points et notamment le typage ~ G. Bouchard #Haskell
• Haskell, monads and purity. ~ Tikhon Jelvis #Haskell
• Python 3 for scientists. ~ Stephanie Douglas et als. #Python
• Cheat sheet for exploratory data analysis in Python. ~ M. Saraswat #DataScience #Python
• A curious connection between continued fractions and combinatorics. ~ Dan Piponi #Haskell #Math
• Le compilateur GHC Haskell en version 8.0.1. ~ Guillaume Bouchard #Haskell
• Build GHC in Vagrant. ~ Hiroshi Ogawa #Haskell #Vagrant
• Introduction to scientific software deployment and development. ~ Damien Francois #Programming
• CurryCheck: Checking properties of Curry programs. ~ M. Hanus #Curry
• Unwanted Haskell triangle. ~ C. Martin #Haskell
• hindent 5: One style to rule them all. ~ Chris Done #Haskell
• A formalization of elementary group theory in the proof assistant Lean. ~ A. Zipperer #ITP #Lean #Math
• cabal new-build is a package manager. ~ E.Z. Yang #Haskell
• Sets, logic, computation (An open logic text). ~ R. Zach #eBook #Logic
• How to compile GHC on Windows using Stack and the new Shake-based GHC build system. ~ Neil Mitchell #Haskell

Septiembre 2016

• Culling concurrency theory: Reusable and trustworthy meta-theory, proof techniques and separation results. ~ J. Åman #IsabelleHOL
• Answer set programming for logical analysis of data. ~ K Becker et als. pp. 15-26 #ASP #Prolog #DataScience #LAD
• ladoscope: tools for logical analysis of data. ~ P. Lemaire #DataScience #LAD #OCaml
• Build GHC on Windows using Hadrian and Stack. ~ A. Mokhov #Haskell
• Craft3e: Code for “Haskell: the craft of functional programming”, 3rd ed. ~ S. Thompson #Haskell
• DataHaskell: an open source Haskell Data Science organization. ~ #Haskell #DataScience
• Currying is delicious. ~ J. Moronuki #Haskell
• Function compose, type cut, and the algebra of logic. ~ X. Yuheng #Logic #CompSci #Scheme
• Getting started with Haskell using Stack. ~ #Haskell
• Set-theoretic mereology. ~ Joel David Hamkins #Logic #Math
• Has-Sci: A collection of computational methods in science. ~ Sarthak Bagaria #Haskell #Physics
• Reproducible research in the mathematical sciences. ~ D. Donoho & V, Stodden #Math #CompSci
• Haskell for Data Science. ~ G. Gonzalez #Haskell #DataScience
• Problemas de satisfacción de restricciones. ~ F. Sancho #AI
• Formal reasoning about programs. ~ Adam Chlipala #eBook #Logic #CompSci #ITP #Coq
• How the Königsberg bridge problem changed mathematics. ~ Dan Van der Vieren #Math
• Proofs and programs. ~ @JohnDCook #Math #CompSci
• Inteligencia artificial: Colonias de hormigas. ~ Daniel Riera #IA
• How hard, really, is SAT? ~ R.J Lipton & K.W. Regan #Logic #CompSci
• A variant of the superposition calculus in Isabelle/HOL. ~ N. Peltier #ITP #IsabelleHOL #Logic #AFP
• Haskell basics: functions and pictures. ~ J. Breitner #Haskell #CodeWorld
• The new CIS-194 (The Haskell minicourse at the University of Pennsylvania). ~ J. Breitner #Haskell
• Una de las demostraciones más bonitas de Paul Erdös. ~ #Matemáticas
• An elegant proof from Erdös. ~ J.D. Cook #Math
• Learn you an Elm. ~ J. Eremondi & A. Neslusan #Elm
• haskell-emacs: Write Emacs extensions in Haskell. ~ #Haskell #Emacs
• Stone algebras in Isabelle/HOL. ~ W. Guttmann #ITP #IsabelleHOL #Math #AFP
• Deriving Haskell lenses from an adjunction in the Kleisli category using Yoneda. ~ B, Milewski #Haskell
• Why is list comprehension bad? ~ Xah Lee #Programming
• An algebra of synchronous atomic steps. ~ I.J. Hayes et als. #ITP #IsabelleHOL
• Automated reasoning and Amazon s2n. ~ Colm MacCárthaigh #Cryptography #AR #Cryptol #Haskell
• Part one: Verifying s2n HMAC with SAW. ~ J. Dodds #Cryptography #AR #Cryptol #Haskell
• Part two: Specifying HMAC in Cryptol. ~ J. Dodds #Cryptography #AR #Cryptol #Haskell
• DataHaskell wiki. ~ #Haskell #DataScience #DataHaskell
• The new and improved Programming Languages Zoo. ~ Andrej Bauer #Programming
• The Programming Languages Zoo (A potpourri of programming languages). ~ A. Bauer & M. Pretnar #Programming
• Columbia creates data set cleaner. ~ Kay Ewbank #DataScience
• The base of a string theory for Haskell ~ Edward Z. Yang #Haskell
• A formal proof of the incompatibility of SD-efficiency and SD-strategy-proofness. ~ M.Eberl #ITP #IsabelleHOL
• CodeWorld: Educational computer programming environment using Haskell. ~ C. Smith http://bit.ly/2bYjVOB #Haskell #CodeWorld
• HaskellStarter: A project that demonstrates getting up and running with Haskell. ~ Josh Cough #Haskell
• How to teach computational thinking. ~ stephen wolfram #education #compsci
• emacs configurations for latex. ~ irreal #emacs #latex
• A curated list of awesome coq frameworks, libraries and software. ~ #Coq
• How to write a package in Haskell and interact with the code inside of it. ~ Chris Allen #Haskell
• Proving non-deterministic computations in agda. ~ S. Antoy, M. Hanus & S. Libby #Agda #Curry
• Using Haskell for a declarative implementation of system Z inference. ~ S. Kutsch & C. Beierle #Haskell
• Iptables-semantics in Isabelle/HOL. ~ C. Diekmann & L. Hupel #IsabelleHOL #AFP
• A framework for extending microkanren with constraints. ~ J. Hemann & D.P. Friedman #Racket
• Selene: a generic framework for model checking concurrent programs from their semantics in Maude. ~ A. Riesco & G. Suárez #Maude
• Huri: a clojure library for the lazy data scientists. ~ Simon Belak #Clojure #DataScience
• Doing data science with Clojure. ~ Simon Belak #Clojure #DataScience
• Los polinomios de Rudin-Shapiro. ~ Café Matemático #Matemáticas
• Intro to formal logic 2nd ed. — readers wanted! ~ Peter Smith #Logic
• IDRIS: Systems programming meets full dependent types. ~ E.C. Brady #Idris
• Emacs configuration in 24 minutes. ~ Mohammed Ismail #Emacs
• Example driven development. ~ Wilfred Hughes #Emacs #Lisp
• Creating and running unit tests directly in source files with org-mode. ~ Frederick Giasson #Clojure #Emacs
• An implementation of Deflate in Coq. ~ C.S. Senjak & M. Hofmann #Coq
• What does Flatland have to do with Haskell? ~ Tony Fischetti #Haskell
• Formalized confluence of quasi-decreasing, strongly deterministic conditional TRSs. ~ T. Sternagel & C. Sternagel #ITP #IsabelleHOL
• A reimplementation of the Statistics.Sample module using the foldl package. ~ Alex Mason #Haskell
• Working with data in Haskell. ~ Chris Done #Haskell #DataScience
• A short mechanized proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle. ~ #IsabelleHOL
• Applicative style programming. ~ J.L. García http://bit.ly/2cPvy7o #Haskell
• A short Haskell FileStore tutorial. ~ M. Mayer #Haskell #Git #Darcs #Mercurial
• Emacs for Haskell. ~ M. Mayer #Haskell #Emacs
• Top algorithms used by data scientists. ~ G. Piatetsky #DataScience
• Lógica formal y argumentación como disciplinas complementarias. ~ G. Palau #Lógica
• learn-physics: Haskell code for learning physics. ~ S.N. Walck #Haskell #Physic
• Practical string processing in Haskell. ~ K. Osanai #Haskell
• Certifying a crash-safe file system. ~ Haogang Chen #PhD_Thesis #Coq
• Modules that enable one to write simulation scripts in Haskell. The examples particularly simulate some of the laws of mechanics. ~ #Haskell
• Formal semantics & verification for the Border Gateway Protocol. ~ K. Weitz et als. #Coq
• La estética del código fuente: a la búsqueda del Arte en la Programación. ~ Carlos Benítez #Programación
• Toward a history of mathematics focused on procedures. ~ P. Blaszczyk et als. #Math #History
• Axiomatizing category theory in free logic. ~ C. Benzmüller & D.S. Scott #ITP #IsabelleHOL
• Folds and infinite lists. ~ @argumatronic #Haskell
• Set theory and its place in the foundations of mathematics (a new look at an old question). ~ M. Džamonja #Logic #Math
• Machine-checked mathematics. ~ A. Mahboubi #ITP #Math
• Teenage Haskell. ~ Tim Docker #CodeWorld #Haskell
• SAT/SMT solving in Haskell. ~ Masahiro Sakai #Haskell #SAT #SMT
• Introduction to Stack’s Docker integration. ~ Yuji Yamamoto #Haskell #Stack #Docker
• Mechanized analysis of a formalization of Anselm’s ontological argument by Eder and Ramharter. ~ J. Rushby #ITP #PVS
• Proofs and assurance (The case of the ontological argument). ~ J. Rushby #ITP #PVS
• Assurance and formal methods. ~ J. Rushby #Formal_methods
• Formal models for human-machine interactions. ~ J. Rushby #Formal_methods
• Assurance in the internet of things and for automated driving. ~ J. Rushby #Formal_methods #IoT
• Practical Haskell: simple file mirror (part 1). ~ M. Snoyman #Haskell
• Álgebra Linear: com um pouco de Mecânica Quântica. ~ D. Krause #eBook #Math
• A proof of the halting theorem. ~ R.J Lipton & K.W. Regan #Logic #CompSci
• Music as code talks. ~ Chris Ford #Programming #Music
• Equilibrium graphs. ~ P. Cabalar, C. Pérez & G. Pérez #Logic #ASP
• Beginning Haskell. ~ Tom Prior #Haskell
• Stone algebras in Isabelle/HOL. ~ W. Guttmann #IsabelleHOL #Math #AFP
• Math-aware search engines: physics applications and overview. ~ D.C. Pineau #Math #MKM
• Practical Haskell: simple file mirror (part 2). ~ M. Snoyman #Haskell
• Social network processes in the Isabelle and Coq theorem proving communities. ~ J. Fleuriot, S. Obua, P. Scott #IsabelleHOL #Coq
• Distributed agent-based automated theorem proving in order-sorted first-order logic. ~ Dohan Kim #ATP
• The influence of Haskell: new Java Spring release contains functional web framework ~ @poutsma http://bit.ly/2cAr3PU #Haskell
• L’intelligence artificielle, ce n’est plus de la science-fiction. ~ Christine Siméone #IA
• Your first Haskell application (with Gloss) ~ Andrew Gibiansky #Haskell #Cabal #Gloss #Game
• GIF as time paradox: between transience and permanence. ~ #Math #GIF #Mathematica
• Refinement reflection: Haskell as a theorem prover. ~ R. Jhala #Haskell #LiquidHaskell #Logic
• Certification of context-free grammar algorithms. ~ D. Firsov #PhD_Thesis #Agda
• Data science and the perfect team. ~ Ryan Swanstrom #DataScience
• Semiring programming: a framework for search, inference and learning. ~ V. Belle & L. de Raedt #Programming
• Allen’s interval calculus in Isabelle/HOL. ~ F. Ghourabi #ITP #IsabelleHOL #AFP
• Leibniz’ dream. ~ The Ratiocinator #Logic #CompSci #Leibniz
• Under the spell of Leibniz’s Dream. ~ Edsger W.Dijkstra #Logic #CompSci #Leibniz

Octubre 2016

• Mathematical components. ~ A. Mahboubi, E. Tassi, Y. Bertot, G. Gonthier #ITP #Coq #Math #eBook
• On the functional interpretation of OCL. ~ D. Calegari & M. Viera #Haskell
• List of logical lists. ~ Adolfo Neto #Logic
• Failing faster: Overlapping patterns for property-based testing. ~ J. Fowler & G. Hutton #Haskell
• Tutorial on reasoning in expressive non-classical logics with Isabelle/HOL. ~ A. Steen, M. Wisniewski & C. Benzmüller #IsabelleHOL
• Big Logic: verifying the correctness of large systems. ~ J.D. Cook #Logic #CompSci
• Sparse linear algebra datastructures and algorithms in Haskell. ~ Marco Zocca #Haskell
• Total functional programming. ~ D.A.Turner #Haskell
• Thonny: Python IDE for beginners. ~ #Python
• A theoretician’s guide to the experimental analysis of algorithms. ~ D.S. Johnson #Algorithmic
• Dependent types at work. ~ A. Bove & P. Dybjer #Haskell
• Foundations of data science. ~ A. Blum, J. Hopcroft & R. Kannan #eBook #DataScience
• Proof assistants for natural language semantics. ~ S. Chatzikyriakidis & Z. Luo #ITP #Coq
• Verified algorithms for context-free grammars in Coq. ~ J. Hofmann #Coq
• On the applications of interactive theorem proving in computational sciences and engineering. ~ A. Tahat #ITP #PVS
• Modular deductive verification of sampled-data systems. ~ Daniel Ricketts et als. #Coq
• ¿Se puede liberar la programación del estilo de von Neumann? ~ F. Sancho #Programación
• An introduction to programming and proving with dependent types in Coq. ~ A. Chlipala #Coq
• La lógica matemática: una disciplina en busca de encuadre. ~ J. Ferreirós #Lógica
• Mind the gap: Addressing behavioural inconsistencies with formal methods. ~ J.K.F. Bowles & M.B. Caminati #IsabelleHOL #Z3
• Refinement reflection on ADTs: Lists are monoids. ~ R. Jhala #Haskell #LiquidHaskell #Logic
• Intersecting chords theorem in Isabelle/HOL. ~ L. Bulwahn #ITP #Isabell/HOL #Math #AFP
• Bullipedia: un caso de construcción social de conocimiento gastronómico. ~ A. Jiménez #PhD_Thesis
• HLogo: A parallel Haskell variant of NetLogo. ~ N. Bezirgiannis, I.S.W.B. Prasetya & I. Sakellariou #Haskell
• What makes a program elegant? ~ Robin K. Hill #Programming
• Essentials missed by mathematics education (for good reasons, and with bad consequences). ~ W. Neuper #Math #Education #ITP
• “Systems that explain themselves” for engineering education. ~ W.A. Neuper #Education #TP
• Foundations of Mathematics (Oct. 15, 2016). ~ Ken Kubota #Logic #Math #ITP
• A toy Mathematica interpreter in Haskell. ~ Yonghao Jin #Haskell #Mathematica
• Razonamiento formalizado: Del sueño a la realidad de las pruebas. ~ J.A. Alonso #RA2016
• Du rêve à la réalité des preuves. ~ Jean-Paul Delahaye #RA2016
• Proof assistants: History, ideas and future. ~ H. Geuvers #RA2016
• A short survey of automated reasoning. ~ J. Harrison #RA2016
• Computer math proof shows reasoning power. ~ G. Kolata #RA2016
• Computers and the sociology of mathematical proof. ~ D. MacKenzie #RA2016
• What is automated theorem proving?. ~ G. Sutcliffe #RA2016
• The HoTT Library: A formalization of homotopy type theory in Coq. ~ A. Bauer et als. #ITP #Coq #HoTT
• Formalising real numbers in homotopy type theory. ~ G. Gilbert #ITP #Coq #Math
• Analyzing program termination and complexity automatically with AProVE ~ J. Giesl et als. #AProVe
• Cours: Automated reasoning. ~ J. Fleuriot #AR #Logic #IsabelleHOL #RA2016
• Refinement reflection (or, how to turn your favorite language into a proof assistant using SMT). ~ N. Vazou & R. Jhala #Haskell
• Stable matching in Isabelle/HOL. ~ Peter Gammie #IsabelleHOL #AFP
• Persistent data structures. ~ G. Kunigami #OCaml
• A simple embedded probabilistic programming language. ~ Jared Tobin #Haskell
• Efficient certified resolution proof checking. ~ L. Cruz-Filipe et als. #ITP #Coq #Logic
• A taste of Haskell. ~ Dennis Felsing #Haskell
• Calling Python libraries from Haskell. ~ John Millikin #Python #Haskell
• Verifying Haskell programs using constructive type theory. ~ A. Abel at als. #Haskell #Agda
• hs2agda: a tool for formally verifying haskell code in Agda. ~ Langston Barrett #Haskell #Agda
• Automation of separation logic using auto2. ~ B. Zhan #IsabelleHOL
• Modal logics for nominal transition systems in Isabelle/HOL. ~ T. Weber et als. #IsabelleHOL #AFP
• How are programs found? (Speculating about language ergonomics with Curry-Howard). ~ J. Emerich #CompSci #Math
• Formal reasoning. ~ H. Geuvers #Logic
• Florida Tech, CS: Functional programming (Fall 2016). ~ Ryan Stansifer #Haskell
• Building small native languages with Haskell. ~ S. Diehl #Haskell
• Efficient certified resolution proof checking. ~ L. Cruz-Filipe, J. Marques-Silva & P. Schneider-Kamp #ITP #Coq #SAT

Noviembre 2016

• Verified parallel string matching in Haskell. ~ N. Vazou & J. Polakow #Haskell #LiquidHaskell
• Certified convergent Perceptron learning. ~ T. Murphy, P. Gray & G. Stewart #Coq #ML
• A functional approach to library construction for conceptual reasoning. ~ DWP MacMillan #Haskell
• Automation of separation logic using auto2. ~ B. Zhan #IsabelleHOL
• Verificación formal de la lógica de Hoare en Isabelle/HOL. ~ N. González #IsabelleHOL
• Introductory Programming Subject in European Higher Education. ~ V. Aleksić & M. Ivanović #Programming #Education
• The theory and practice of Randori coding dojos. ~ J. Rooksby, J. Hunt & X. Wang #Programming
• Haskell vs. other programming languages. ~ ~ S. Diehl #Programming Haskell
• A Coq formal proof of the Lax–Milgram theorem. ~ S. Boldo et als. #ITP #Coq #Math
• Write your own theorem prover. ~ P. Scott #Haskell #Logic
• Covariance and contravariance. ~ M. Snoyman #Haskell
• Exceptions best practices in Haskell. ~ M. Snoyman #Haskell
• The best Functional Programming blogs and how to get started. ~ Medium #FP #Haskell #Scala #Clojure #Elixir #Erlang #FSharp
• Theorem prover museum. ~ M. Kohlhase #ATP #ITP
• Artificial Intelligence (Provisional Lecture Notes). ~ M. Kohlhase #AI
• Computational Logic (320441 CompLog Lecture Notes). ~ M. Kohlhase #Logic
• Living in Emacs. ~ Irreal #Emacs
• Expressiveness of deep learning in Isabelle/HOL. ~ A. Bentkamp #IsabelleHOL #AFP
• Trees that grow (an early draft). ~ S. Najd & S. Peyton Jones #Haskell
• Concrete semantics with Isabelle/HOL (Advanced course at Universität des Saarlandes). ~ J. Blanchette et als. #IsabelleHOL
• Extending superposition with integer arithmetic, structural induction, and beyond. ~ S. Cruanes #PhD_Thesis #Logic #ATP #OCaml
• A brief presentation of OCaml. ~ S. Cruanes #OCaml
• Popular Math books at Goodreads. ~ #Math #Books
• Coming to terms with quantified reasoning. ~ L. Kovács, S. Robillard & A. Voronkov #ATP #Vampire
• Observations of a functional programmer. ~ Yaron Minsky #FP #OCaml
• Practical recursion schemes ~ Jared Tobin #Haskell
• What Artificial Intelligence can and can’t do right now. ~ Andrew Ng #AI
• Functional programming in Clojure. ~ Troy Miles #FP #Clojure
• Contributions to a computational theory of policy advice and avoidability. ~ N. Botta, P. Jansson & C. Ionescu #Idris
• “Let us calculate!”: Leibniz, Llull, and the computational imagination. ~ J. Gray #Leibniz #Math #CompSci
• CertSkel: a verified compiler for a Coq-embedded GPGPU DSL. ~ I. Asakura et als. #ITP #Coq
• Beginning practical Haskell (An introductory Haskell programming course). ~ Richard Cook #Haskell
• Theorem proving in Lean. ~ J. Avigad, L. de Moura y S. Kong #ITP #Lean
• Interactive and automated theorem proving for non-classical logics (Tutorial at GCAI 2016). ~ C. Benzmüller #IsabelleHOL #Logic
• teaspoon: Solving the curriculum-based course timetabling problems with Answer Set Programming. ~ M. Banbara #ASP
• Haskell tutorial and cookbook. ~ M. Watson #Haskell #eBook
• Solving the 15-Puzzle with Haskell and diagram. ~ J. Rosenbluth #Haskell
• Haskell numeric types: quick reference. ~ J. Rosenbluth #Haskell
• ¿Puede existir matemática sin computación? ~ F. Sancho #Matemáticas #Computación
• Monte Carlo connection prover. ~ M. Färber, C. Kaliszyk & J. Urban #ATP #ML #leanCoP
• Comparative concurrency with Haskell. ~ M. Snoyman #Haskell
• A Haskell study syllabus (Learn professional-grade Haskell coding practices quickly and efficiently). ~ FP Complete #Haskell
• A verified low-level formatting EDSL in Agda. ~ M. van Geest #MsC_Thesis #Agda
• Software libre bajo Linux: Una alternativa para las Matemáticas de México. ~ G.M. Ortigoza #Matemáticas #Computación
• Fundamental concepts in programming languages. ~ C. Strachey #Programming
• Proving opacity of a pessimistic STM. ~ S. Doherty et als. #IsabelleHOL
• Haskell for dummies. ~ M. Snoyman #Haskell
• SAW provides the ability to formally verify properties of code written in C, Java, and Cryptol. ~ #Haskell #Formal_verification
• Hackage dependency monitor. ~ #Haskell
• Donald Knuth was the first Erlang programmer. ~ A. Videla #Programming #Erlang
• Boolean pythagorean triples problem. ~ Wikipedia #Math #Logic #CompSci
• Spreading the Gospel of Haskell. ~ M. Snoyman #Haskell
• Máximo producto en la partición de un número (2). ~ Antonio Roldán #Matemáticas #Programación
• Programming and mathematical thinking. ~ A.M. Stavely #eBook #Math #Programming #Python
• The coder’s apprentice: learning programming with Python 3. ~ P. Spronck #eBook #Programming #Python
• Towards certified compilation of financial contracts. ~ D. Annenkov & M. Elsman #Coq #Haskell
• New computer algebra system: OSCAR ~ #Math #CompSci #CAS
• Introducción a la Lógica (para informáticos). ~ L.M. Pardo #Lógica
• Bach and the musical Möbius strip. ~ Tony Phillips #Math #Music
• plots: Diagrams based plotting library. ~ #Haskell
• Simulate physics on generalized coordinate systems using Hamiltonian Mechanics and automatic differentiation. ~ #Haskell
• UCI datasets: data sets for statistics and machine learning, in Haskell. ~ #Haskell
• Why category theory matters: a functional programmer’s perspective. ~ J.N. Oliveira #Math #FP
• Proofs from THE BOOK. ~ M. Aigner & G.M. Ziegler #Math
• Euclid’s theorem: proofs of infinitude of primes. ~ Wikipedia #Math
• Fermat numbers are coprime. ~ ProofWiki #Math
• Foldl: Composable, streaming, and efficient left folds. ~ G. Gonzalez #Haskell
• An interactive tutorial on numerical optimization. ~ Ben Frederickson #Math #Javascript
• Simple unsolved math problem: How often does an integer occur as a binomial coefficient? ~ W. David Joyner #Math
• Adventures in enumerating balanced brackets. ~ Brent Yorgey #Haskell
• The generic-random library, part 1: simple generic Arbitrary instances. ~ Brent Yorgey #Haskell
• Haskell documentation, 2016 update. ~ M. Snoyman #Haskell
• Group theory in Haskell. ~ #Haskell #Math
• Formally certified round-off error analysis of floating-point functions. ~ M Moscato, L Titolo, A Dutle, CA Muñoz #PVS
• GHC optimization and fusion. ~ Mark Karpov #Haskell

Diciembre 2016

• Implementation of Bourbaki’s Elements of Mathematics in Coq: Part two, from natural numbers to real numbers. ~ J. Grimm #Coq #Math
• Beautiful folds are practical, too. ~ G. Gonzalez #Haskell
• Beautiful folds in Scala. ~ A. Warski #Scala
• Scala, the language for Data Science. ~ D. Arenas #Scala #DataScience
• Do you like Scala? Give Haskell a try! ~ P. Kant #Haskell #Scala
• Introduction to functional reactive programming (FRP), Yampa, and Arrows. ~ H. Nilsson #FRP #Haskell
• Demostración asistida por ordenador. ~ J.M. Aransay y C. Domínguez #IsabelleHOL #Matemáticas
• Analyzing programs with Z3 and Haskell. ~ T. Jelvis #Haskell #SMT
• Proust: A nano proof assistant. ~ Prabhakar Ragde #ITP #Logic #Racket
• Course: Logic and Computation. ~ Prabhakar Ragde #ITP #Logic #Racket #Agda #Coq
• An algebra of graphs. ~ Andrey Mokhov #Haskell #Math
• Learn Quantum Mechanics with Haskell. ~ Scott N. Walck #Haskell #Physics
• Domain-specific languages of mathematics: presenting mathematical analysis using functional programming. ~ C. Ionescu #Haskell #Math
• The Bricklayer Ecosystem: Art, Math, and Code. ~ V. Winter, B. Love & C. Corritore #Programming #Math
• Paraconsistency in Isabelle/HOL. ~ A. Schlichtkrull & J. Villadsen #Logic #IsabelleHOL #ITP
• Denotational semantics of IMP without fixed points. ~ Jeremy Siek http://bit.ly/2hfy8X2 #Coq
• Liquid Haskell: Haskell as a theorem prover. ~ Niki Vazou #PhD_Thesis #Haskell
• A formal proof of a Unix path resolution algorithm. ~ R. Chen, M. Clochard, C. Marche #ITP #Coq
• Course: Computer-aided reasoning for software engineering. ~ Vijay Ganesh #ATP #Logic #CompSci
• Algoritmos voraces. ~ Carlo Frabetti #Algorítmica
• Twelve monads of Christmas. Day 1: IO — Our ugly friend. ~ Ben Clifford #Haskell
• Twelve monads of Christmas. Day 3: Maybe — Mini-lists, or mini-exceptions. ~ Ben Clifford #Haskell
• Towards verified computer algebra. ~ M. Dénès, C. Cohen, A. Mörtberg #Coq #Math
• Logic in Computer Science. ~ Thierry Coquand #Logic #CompSci
• Principes des langages de programmation. ~ Eric Goubault #eBook #CompSci #OCaml
• Plotting a weight chart using Emacs Org-Mode and Gnuplot. ~ Praveen Kumar #Emacs #GnuPlot
• ¡Olvida OO y a pensar funcionalmente! ~ Javier Onielfa [Vídeo] #Haskell
• Formally verified differential dynamic logic. ~ B. Bohre et als. #IsabelleHOL #Coq #Logic
• Extensible records explained. ~ Fumiaki Kinoshita #Haskell
• AI in biological modelling. ~ F. Fages #AI
• DeepBach: a steerable model for Bach chorales generation. ~ G. Hadjere, F. Pachet #AI
• The calculus of dependent lambda eliminations. ~ A. Stump #Agda
• A gentle introduction to functional programming in Haskell. ~ K.A. Lambert #eBook #Haskell
• Markov processes in Isabelle/HOL. ~ J. Hölzl #IsabelleHOL
• Haskell in the Datacentre: how we tuned the GHC runtime to make Haskell run better at scale. ~ Simon Marlow #Haskell
• A fun refactoring example in Haskell. ~ Pascal Hartig #Haskell
• The great A.I. awakening. ~ Gideon Lewis-Krausdec #AI
• Normalisation by evaluation for type theory, in type theory. ~ T. Altenkirch & A. Kaposi #Agda
• Efficient certified RAT verification. ~ L. Cruz-Filipe et als. #SAT #Coq #ACL2
• Zeller’s congruence algorithm to calculate the day of the week. ~ #Haskell
• Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Three Structures. ~ J. Grimm #Coq #Math
• Formal foundations of 3d geometry to model robot manipulators. ~ R. Affeldt & C. Cohen #Coq #Math
• Verification of certifying distributed programs (Case study: leader election). ~ S. Akili, K. Völlinger #Coq
• PureScript mediante ejemplos (Programación funcional para la Web). ~ Phil Freeman #PureScript #eBook
• Mónadas. ~ Mario Román | LibreIM #Haskell
• Jupyter Notebooks for the “Python Data Science Handbook”. ~ Jake Vanderplas #Python #DataScience #eBook
• How to teach introductory logic to undergraduates. ~ Diary of Dr. Logic #Logic
• Specification driven programming: A design pattern. (Solving the dichotomy between solution and test). ~ C. Kohlhepp #Lisp
• A bird’s eye view of functional programming. ~ Brooklyn Zelenka #FP #Haskell
• 8 ways to report errors in Haskell. ~ Eric Kidd #Haskell
• hs-logo: an interpreter for the Logo Programming Language, written in Haskell. ~ #Haskell #Logo
• Data frames for tabular data. ~ Anthony Cowley #Haskell
• Reflecting on Haskell in 2016. ~ Stephen Diehl #Haskell
• Formalization and assessment of Lowe’s modal ontological argument. ~ D. Fuenmayor #IsabelleHOL
• Validating the meta-theory of programming languages with Haskell. ~ G. Fachini #Haskell
• Mutual recursion in final encoding. ~ Andreas Herrmann #Haskell
• Introducing the Hamilton library. ~ Justin Le #Haskell
• Proving Stuff in Haskell. ~ Mads Buch #Haskell
• Little languages. ~ David Laing #Haskell
• Tamarin prover: a powerful tool for the symbolic modeling and analysis of security protocols. ~ #Haskell
• The theory of abstract objects. ~ E. Badstübner, D. Kirchner & P. Schießl #IsabelleHOL
• Formal verification for ASP: A case study using the PVS theorem prover. ~ F. Aguado et als. #ITP #PVS #ASP
• Mathematical components (The Book) ~ Assia Mahboubi & Enrico Tassi #eBook #Coq #Math
• McCarthy Math. ~ Harry Prevor #Lisp #Python #Math
• Proving God’s existence by automating Leibniz’ algebra of concepts. ~ M. Bentert et als. #IsabelleHOL
• Quo Vadis program verification. ~ Krzysztof R. Apt #Verification
• Haskell-style Fibonacci in Python. ~ Joel Grus #Haskell #Python
• What Python can learn from Haskell. ~ Bob Ippolito #Python #Haskell
• The Zen of Python. ~ #Python
• The Zen of Haskell. ~ #Haskell
• How pythonic is Haskell? ~ Mike Meyer #Haskell #Python
• Haskell gets static typing right. ~ Andres Löh #Haskell
• Functional programming with Python. ~ Alexey Kachayev #FP #Python
• A formalization of the Berlekamp–Zassenhaus factorization algorithm. ~ J. Divasón et als. #IsabelleHOL #Math
• Elegant and efficient Python. ~ S.R. Hastings #Python
• Computational algebra system in Haskell. ~ Hiromi Ishii #Haskell #Math
• The idea of Lisp. ~ Eric Normand #Lisp
• The next 700 safe tactic languages. ~ B. Ziliani et als. #Coq
• Computerized verification of formal reconstructions of Anselm’s argument by Eder and Ramharter. ~ L. Grätz & F. Schütz #IsabelleHOL
• Fiction as model theory. ~ Robin K. Hill #Logic
• Software project maintenance is where Haskell shines. ~ Chris Done #Haskell
• F-algebras or: how I learned to stop worrying and love the type system. ~ Anthony Burzillo #Haskell
• Twelve monads of Christmas. ~ Ben Clifford #Haskell