Lecturas del año 2018.org

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

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

Enero 2018

• Haskell notes for professionals book. #eBook #Haskell
• An extensible ad hoc interface between Lean and Mathematica. ~ R.Y. Lewis #ITP #Lean #Mathematica
• Template Haskell tutorial. ~ M. Karpov #Haskell
• Algoritmo de Monte Carlo aplicado a búsquedas en espacios de estados. ~ F. Sancho #IA
• ProofSweeper: Play Minesweeper by formally proving your moves in Idris. ~ Andrew Miller #Idris #Haskell
• Haskell containers package. ~ Matt Renaud #Haskell
• The falling factorial of a sum. ~ L. Bulwahn #IsabelleHOL
• Functional programming for mathematical computing. ~ Matthias Endler #Haskell
• Libro de exámenes de programación funcional con Haskell (versión del 6 de enero de 2018). #Haskell #I1M2017
• The foundations of mathematics. ~ K. Kunen #eBook #Logic #Math
• Is State a Comonad? ~ Edward Kmett #Haskell
• Finite of sense and infinite of thought: a history of computation, logic and algebra, part I. ~ Ron Pressler #Logic #Math #CompSci
• Formal verification: the gap between perfect code and reality. ~ Ray Wang #Formal_methods
• Coming soon: machine-checked mathematical proofs in everyday software and hardware development. ~ Adam Chlipala #ITP
• Snårkl: Somewhat practical, pretty much declarative verifiable computing in Haskell. ~ G. Stewart, S. Merten, L. Leland #Haskell
• TWAM: A certifying abstract machine for logic programs. ~ B. Bohrer, K. Crary #ITP #LF
• The Kuratowski closure-complement theorem in Isabelle/HOL. ~ P. Gammie, G. Gioiosa #ITP #IsabelleHOL #Math
• The Shoelace formula for the area of a polygon. ~ Atabey Kaygun #CommonLisp #Math
• Monads are just monoids in the category of endofunctors. ~ Axel Wagner #Haskell #Math
• 10 awkward moments in math history. ~ Elena Nisioti #Math #History
• Hezarfen: a theorem prover for intuitionistic propositional logic in Idris. ~ Joomy Korkut #Idris #Haskell #Logic
• Las universidades de EEUU al fin lo han reconocido: empezar a programar por Java es una mala idea. ~ Esther Miguel Trula
• Haskell et programmation fonctionnelle, ma conviction. ~ Frédéric Menou #Haskell
• A formally verified implementation of multivariate Taylor models in Isabelle/HOL. ~ C. Traut, F. Immler #ITP #IsabelleHOL
• An Isabelle/HOL formalisation of Green’s theorem. ~ M. Abdulaziz, L.C. Paulson #ITP #IsabelleHOL #Math
• Introduction to Singletons (Part 2). ~ Justin Le #Haskell
• A friendly introduction to mathematical logic. ~ Christopher C. Leary #eBook #Logic
• NP-hard does not mean hard. ~ Jeremy Kun | Math ∩ Programming #CompSci
• Œuf: Minimizing the Coq extraction TCB. ~ E. Mullen et als. #Coq
• The simple essence of automatic differentiation. ~ Conal Elliott #Haskell
• linearmap-family: Purely-functional, coordinate-free linear algebra. ~ Justus Sagemüller #Haskell #Math
• From neural networks to the Category of composable supervised learning algorithms in Scala with compile-time matrix checking based on singleton-types. ~ Pascal Voitot #Scala
• CodeWorld: The why, what, and how of teaching Haskell to children. ~ Chris Smith #Haskell
• How to teach computational thinking. ~ Stephen Wolfram #Teaching #CompSci
• Integrating computer science in math: the potential is great, but so are the risks. ~ Emmanuel Schanzer #Teaching #CompSci #Math
• Bootstrap: a research project at Brown University that offers a series of curricular modules built around purely mathematical programming. #Teaching #CompSci #Math
• “Let us calculate!”: Leibniz, Llull, and the computational imagination. ~ Jonathan Gray
• A tableaux calculus for reducing proof size. ~ M.P. Lettmann, N. Peltier #Logic #ATP
• Haskell in middle and high school mathematics. ~ F. Alegre, J. Moreno #Haskell #Math
• Mathematics for middle and high school in Haskell. #Haskell #Math
• Applicative functors and data validation, part II. ~ Carlos Morera de la Chica #Haskell
• Extending higher-order logic with predicate subtyping: application to PVS. ~ Frédéric Gilbert #ITP #PVS
• Supermonads and superapplicatives. ~ J. Bracker, H. Nilsson #Haskell #Agda
• Lecture notes on rewriting theory. ~ F. Blanqui
• Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. ~ S. Amani, M. Bégel, M. Bortin, M. Staples #ITP #IsabelleHOL
• Guía turística de Sevilla con Scratch. ~ @programamos #Scratch
• Formal microeconomic foundations and the First Welfare Theorem. ~ C. Kaliszyk, J. Parsert #ITP #IsabelleHOL
• A primer on boolean satisfiability. ~ Emina Torlak #Logic #SAT #Racket
• Course: Computer-aided reasoning for software. ~ E. Torlak #AutomatedReasoning #Logic
• Functional programming principles in Scala. ~ Martin Odersky #FunctionalProgramming #Scala
• Formalizing data management systems: a case study of Syndicate protocol. ~ C.K. Wang, H. Xu #ITP #Coq
• Computational Quadrinitarianism (Curious Correspondences go Cubical). ~ Gershom Bazerman #CompSci
• A random walk through experimental mathematics. ~ E.Y.S. Chan, R.M. Corless #Math #Programming
• λ-calculus. ~ Christian Sternagel #Logic #Haskell #CompSci
• Shrink fast correctly! ~ Olivier Savary Bélanger, Andrew W. Appel #ITP #Coq
• Hofstadter’s Q sequence. ~ Atabey Kaygun #CommonLisp #Math
• Ten common myths about Computer Science. #CompSci
• Reasoning about functional programs. ~ Christian Sternagel #Logic #Haskell
• Resources for teaching with formal methods. ~ Jeremy Avigad #FormalMethods
• Computer understandable mathematics. ~ Josef Urban #ATP #ITP #Math
• The specification and analysis of use properties of a nuclear control system. ~ M.D. Harrison, P.M. Masci, J. Creissac Campos and P. Curzon #ITP #PVS
• Efficiency of functional programs. ~ Christian Sternagel and Harald Zankl #Haskell
• History of interactive theorem proving. ~ John Harrison, Josef Urban and Freek Wiedijk #ITP
• Computational thinking as an emergent learning trajectory of mathematics. ~ Tiina Partanen #Math #CompSci
• Verification of a concurrent garbage collector. ~ Yannick Zakowski #PhDThesis #ITP #Coq
• Typing of functional programs. ~ Christian Sternagel #Logic #FunctionalProgramming
• Creando un videojuego paso a paso con Scratch desde cero. ~ Jesús Moreno León #Scratch
• Domain modelling with Haskell: data structures. ~ Oskar Wickström #Haskell
• Liquid Haskell: refinement types for Haskell. ~ Niki Vazou #Haskell #LiquidHaskell
• Sequences, yet functions: the dual nature of data-stream processing. ~ S. Herbst, J. Tenschert, A.M. Wahl, K. Meyer-Wegener #ITP #Coq
• Course: Functional programming. ~ Christian Sternagel et als. #Haskell
• How to prove a compiler correct. ~ Daniel Patterson #Haskell
• Explaining type errors. ~ B. Yorgey, R. Eisenberg, H. Eades #Haskell
• Relational characterisations of paths. ~ R. Berghammer, H. Furusawa, W. Guttmann, P. Höfner #ITP #IsabelleHOL
• Functors done quick! ~ James Bowen #Haskell
• Programando un laberinto con Scratch, ¡para principiantes! ~ Alejandra Sánchez Acosta #Scratch
• Dafny overview. ~ K. Rustan M. Leino #Dafny
• “Interpreters a la Carte” in Advent of Code 2017 Duet. ~ Justin Le #Haskell
• Formalization of Bachmair and Ganzinger’s ordered resolution prover. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel and U. Waldmann (Code) #ITP #IsabelleHOL
• Haskell functions as functors, applicatives and monads. ~ Eli Bendersky #Haskell
• The nesting instinct. ~ Julie Moronuki #Haskell
• Model theory and machine learning. ~ H. Chase, J. Freitag #Logic #AI
• Computer-assisted proving of combinatorial conjectures over finite domains: a case study of a chess conjecture. ~ P. Janičić, F. Marić, M. Maliković #ITP #IsabelleHOL
• Pointwise Kan extensions. ~ Bartosz Milewski #CategoryTheory #Haskell
• Cracking codes with Python: An introduction to building and breaking ciphers. ~ Al Sweigart #eBook #Programming #Python
• RedPRL: a proof assistant for Computational Higher-Dimensional Type Theory. #ITP #RedPRL #SML
• Computational (higher) type theory. ~ R. Harper and C. Angiuli #RedPRL #SML
• Context Free/cfdg: a simple language for generating stunning images. With only a few lines you can describe abstract art, beautiful organic scenery, and many kinds of fractals.
• Elsa: a lambda calculus evaluator. ~ R. Jhala. #Haskell #Logic #LambdaCalculus
• China enters the battle for AI talent. #AI
• Toward scalable verification for safety-critical deep networks. ~ L. Kuper et als. #NeuralNetworks #SMT
• El curioso caso de la secuencia de Goodstein. ~ M.A. Morales | El Aleph #Matemáticas
• A conversation with Stephen Cook. #CompSci
• Collatz sequence (yet again). ~ Atabey Kaygun #CommonLisp #Math
• Introduction to functional programming in Python. ~ Spiro Sideris #FunctionalProgramming #Python
• Finitary-based domain theory in Coq: An early report. ~ M.A. AbdelGawad #ITP #Coq
• Domain modelling with Haskell: Generalizing with Foldable and Traversable. ~ Oskar Wickström #Haskell
• LambdaCase in the wild. ~ Matt Noonan #Haskell
• Recursion schemes, Part 4½: Better living through base functors. ~ Patrick Thomson #Haskell
• Lambda calculus in Clojure (Part 2). ~ Sergio Rodrigo Royo #LambdaCalculus #Clojure
• Free: You can now read classic books by MIT Press on archive.org #eBooks
• When is Haskell more useful than R or Python in Data Science? ~ Tikhon Jelvis #Haskell #Rstats #Python #DataScience
• Programming R at native speed using Haskell. ~ M. Boespflug, F. Domínguez, A. Vershilov #Haskell #Rstats
• A hashing-based graph implementation in Haskell. ~ Patrick Dougherty #Haskell
• Selling laziness. ~ Alex Beal #Programming
• Why functional programming matters. ~ John Hughes #FunctionalProgramming #Miranda
• A toy Wolfram Language interpreter in Haskell. ~ Yonghao Jin #Haskell
• Org-mode: An integrated language and editor. ~ Alex Beal #Emacs #Haskell
• Why sum types matter in Haskell. ~ Will Kurt #Haskell
• Intrinsically-typed definitional interpreters for imperative languages. ~ C. Bach Poulsen, A. Rouvoet, A. Tolmach, R. Krebbers #ITP #Agda
• Monads are not what they seem (Uncovering the hidden nature of programming concepts). ~ T. Petricek #Math #CompSci
• Securing complex software systems using formal verification and specification. ~ X. Qi #FormalVerification
• Programación funcional: la programación del futuro. ~ Moises Vázquez #ProgramacionFuncional #Haskell
• A verified ODE solver and the Lorenz attractor. ~ F. Immler #ITP #IsabelleHOL
• Un vistazo al futuro: revisando demostraciones matemáticas con la computadora. ~ Moisés Vázquez #DAO
• Formalizing the meta-theory of first-order predicate logic. ~ H. Herberlin, S.Y. Kim, G. Lee #ITP #Coq #Logic
• Category theory: a gentle introduction. ~ Peter Smith #CategoryTheory
• Investigations in computer-aided mathematics: experimentation, computation, and certification. ~ Thomas Sibut Pinote #PhDThesis #ITP #Coq
• Formal methods for probabilistic programming. ~ D. Selsam, P. Liang, D.L. Dill #ITP #Lean
• Certigrad: Bug-free machine learning on stochastic computation graphs. ~ D. Selsam #ITP #Lean

Febrero 2018

• Homotopy type theory, univalent foundation, and binary trees. ~ R. Beauvile #ITP #Coq #HoTT
• DSLsofMath: typing mathematics. ~ Patrik Jansson, Cezar Ionescu #Haskell #Math
• The Elfe system: Verifying mathematical proofs of undergraduate students. ~ Maximilian Doré, Krysia Broda #Math #Elfe
• AI for marketing. ~ Chandrakumar #AI
• HOL Light QE. ~ Jacques Carette, William M. Farmer, Patrick Laskowski #ITP #HOL_Light
• Dissecting the State monad with Operational and Free monads. ~ Robbie Langer #Haskell
• El λ–cálculo (sin tipos y con tipos). ~ B.C. Ruiz y P. Guerrero #Matemáticas #Computación
• A tutorial introduction to the lambda calculus. ~ Raul Rojas #Logic #CompSci
• “Speaking” mathematics with “systems that explain themselves”. ~ Walther Neuper #ITP #Math
• Relational equivalence proofs between imperative and MapReduce algorithms. ~ B. Beckert et als. #ITP #Coq
• The magic “Just do it” type class. ~ J. Breitner #Haskell
• Numerical computing is fun (A guide to principles of computer science and numerical computing for all ages). ~ Mikko Kotila #CompSci #Python #Jupiter
• Spirals, snowflakes & trees: Recursion in pictures. ~ G. Keller & M.M.T. Chakravarty #Haskell #Fractals
• Fractals in Haskell (Escape-time fractals created with Haskell and GD). ~ Greg Heartsfield #Haskell #Fractals
• Drawing trees with Haskell and Cairo. ~ Ilmari Heikkinen #Haskell #Fractals
• Org Beamer reference card. ~ Fabrice Niessen #Emacs #OrgMode #LaTeX
• A verified Lenstra-Lenstra-Lovász basis reduction algorithm in Isabelle/HOL. ~ J. Divasón, S. Joosten, R. Thiemann and A. Yamada #ITP #IsabelleHOL #Math
• Haskelling Bitcoin (The case for Bitcoin development in Haskell). ~ M. Alshiekh #Haskell #Bitcoin
• Calcul formel et preuves formelles. ~ Assia Mahboubi #ITP #Mizar #ACL2 #IsabelleHOL #HOL_Light #Coq #Agda #Lean
• A monadic framework for relational verification: Applied to information security, program equivalence, and optimizations. ~ N. Grimm et als. #SMT #Fsharp
• Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem. ~ J. Divasón et als. #ITP #IsabelleHOL
• Ciencias de la Computación (mejores programas y programadores). ~ Lourdes del Carmen González Huesca #Computación
• Curso: Lógica computacional. ~ Lourdes del Carmen González Huesca #Lógica #Computación #Haskell #Prolog #Coq
• Revisiting ‘Monadic parsing in Haskell’. ~ Vaibhav Sagar #Haskell
• Cellular Christmas Tree. ~ Mistral Contrastin #Haskell
• A Coq formalization of normalization by evaluation for Martin-Löf type theory. ~ P. Wieczorek, D. Biernacki #ITP #Coq
• Logic lectures: Gödel’s basic logic course at Notre Dame. #Logic
• The wizard monoid. ~ G. González #Haskell
• A Lean formalization of Matiyasevič’s theorem. ~ Mario Carneiro #ITP #Lean
• 9 desafíos en 9 lenguajes de programación. ~ Eduardo Díaz Cortés #Clojure #Erlang #Fsharp #Go #Haskell #Kotlin #Rust #Scala #Swift
• Egyptian fractions. ~ Atabey Kaygun #CommonLisp #Math
• Free monads for cheap interpreters. ~ James Haydon #Haskell
• First-order terms in Isabelle/HOL. ~ Christian Sternagel, René Thiemann #ITP #IsabelleHOL
• Predicting the next US President by simulating the electoral college. ~ B. Kostadinov #Rstats #DataScience #CompSci
• Programs and proofs (Mechanizing Mathematics with dependent types). ~ Ilya Sergey #ITP #Coq #Math
• Treaps in Isabelle/HOL. ~ Manuel Eberl, Max Haslbeck and Tobias Nipkow #ITP #IsabelleHOL
• The error function in Isabelle/HOL. ~ Manuel Eberl #ITP #IsabelleHOL
• Linus sequence. ~ Atabey Kaygun #CommonLisp
• Lambda calculus tools and interpreter written in Haskell. #Haskell #LambdaCalculus
• For the love of algorithms. ~ Lance Fortnow
• An opinionated guide to Haskell in 2018. ~ Alexis King #Haskell
• Twerk, a twitter archive parser with pipes utilities (in Haskell). ~ Nicolas B. #Haskell
• A verified factorization algorithm for integer polynomials with polynomial complexity. ~ Jose Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada #ITP #IsabelleHOL
• Formal verification of spacecraft control programs using a metalanguage for state transformers. ~ A. Mokhov, G. Lukyanov, J. Lechner #Haskell
• When good components go bad: formally secure compilation despite dynamic compromise. ~ G. Fachini et als. #ITP #Coq
• Foundations of functional programming languages. ~ Andrés Sicard Ramírez #FunctionalProgramming #LambdaCalculus
• Una formalización del sistema de los números reales. ~ Jorge O. Acevedo y José L. Echeverri #ITP #Agda #Math
• ¿Qué lenguajes de programación se usan más los fines de semana? ~ Julia Silge #DataScience #Haskell
• What programming languages are used most on weekends? ~ Julia Silge #DataScience #Haskell
• Verified over-approximation of the diameter of propositionally factored transition systems. ~ M. Abdulaziz, C. Gretton, M. Norrish #ITP #HOL4
• The simply typed lambda calculus (in Agda). ~ Jonathan Prieto-Cubides #ITP #Agda #LambdaCalculus
• Monadic list functions. ~ Donnacha Oisín Kidney #Haskell
• Sn̊arkl: Somewhat practical, pretty much declarative verifiable computing in Haskell. ~ G. Stewart, S. Merten, L. Leland #Haskell
• Hydra Ludica: Une preuve d’impossibilité de prouver simplement. ~ P. Castéran #ITP #Coq
• Introducing the backprop library. ~ Justin Le #Haskell
• ¿Cómo puede “Blockchain” hacernos más libres? #Blockchain
• Org-noter: A synchronized, Org-mode, document annotator. ~ Gonçalo Santos #Emacs
• Corecursion and coinduction: what they are and how they relate to recursion and induction. ~ Mike Gordon
• What I Wish I’d Known When I Started Functional Programming. ~ Tikhon Jelvis #FunctionalProgramming
• Coqatoo: Generating natural language versions of Coq proofs. ~ A. Bedford #ITP #Coq
• Exact real arithmetic implemented by fast binary Cauchy sequences. ~ Joe Hermaszewski #Haskell #Math
• Verifying asymptotic time complexity of imperative programs in Isabelle/HOL. ~ B. Zhan, M.P.L. Haslbeck #ITP #IsabelleHOL
• My attempt to understand the backpropagation algorithm for training neural networks. ~ Mike Gordon
• The higher-order prover Leo-III. ~ A. Steen, C. Benzmüller #ITP
• Proof pearl: Magic wand as frame. ~ Q. Cao, S. Wang, A. Hobor, A.W. Appel #ITP #Coq
• Reading for programmers. ~ P. Limanowski #Emacs
• Quotes about programming and computer science. ~ A. Thompson #Quote #Programming #CompSci
• Van Eck’s sequence. ~ Atabey Kaygun #CommonLisp #Math
• Applicative parsing I: building the foundation. ~ James Bowen #Haskell
• VST-Floyd: A separation logic tool to verify correctness of C programs. ~ Q. Cao, L. Beringer, S. Gruetter, J. Dodds, A.W. Appel #ITP #Coq
• Mathematical Logic in Computer Science. ~ A. Kfoury #Logic #CompSci
• Do computers really think? ~ R. Colin Johnson #AI
• From gameplay to symbolic reasoning: Learning SAT solver heuristics in the style of Alpha(Go) Zero. ~ F. Wang, T. Rompf #ATP #SAT
• Superposition with datatypes and codatatypes. ~ J.C. Blanchette, N. Peltier, S. Robillard #ATP #Vampire
• Lagrange four-square theorem examples. ~ Ken T Takusagawa #Haskell #Math
• Conventional interfaces in functional programming. ~ Carlos Morera #Haskell
• I believe P=NP. ~ Emanuele Viola #CompSci #Math
• Learning a SAT solver from single-bit supervision. ~ D. Selsam et als. #ATP #SAT #NeuralNetwork
• Group theory in Haskell. ~ Spencer Hubbard #Haskell #Math
• Free monoidal functors. ~ Bartosz Milewski #Haskell #CategoryTheory
• massiv: Efficient Haskell arrays featuring parallel computation. ~ Alexey Kuleshevich #Haskell
• ProofWatch: Watchlist guidance for large theories in E. ~ Z. Goertzel, J. Jakubův, S. Schulz, J. Urban #APT
• Relational algebra in Haskell. ~ Spencer Hubbard #Haskell #Math
• Haskell exercises with automatic tests. ~ Alexey Kuleshevich #Haskell
• Atomic expressions generically. ~ Neil Mitchell #Haskell
• ATPboost: Learning premise selection in binary setting with ATP feedback. ~ B. Piotrowski, J. Urban #ATP #ML
• Simply typed lambda calculus in Haskell. ~ Spencer Hubbard #Haskell #Math
• A verified messaging system. ~ W. Mansky, A.W. Appel, A. Nogin #ITP #Coq
• A formal proof of the minor-exclusion property for treewidth-two graphs. ~ C. Doczkal, G. Combette, D. Pous #ITP #Coq
• Free monoidal profunctors. ~ Bartosz Milewski #Haskell #CategoryTheory
• Higher groups in Homotopy Type Theory. ~ U. Buchholtz, F. van Doorn, E. Rijke #ITP #Lean #Math #HoTT
• Journées francophones des langages applicatifs 2018 (JFLA 2018). ~ S. Boldo, N. Magaud
• Type theory and functional programming. ~ S. Thompson #eBook #FunctionalProgramming #TypeTheory
• Some notes about how I write Haskell. ~ @aisamanra #Haskell
• Constructive mathematics and computer programming. ~ P. Martin-Löf #Math #CompSci
• Automated reasoning and ultra-intuitionism. ~ R.L. Constable #Logic #ATP #ITP
• Educating computer science educators online (A Racket MOOC for elementary math teachers of Finland). ~ T. Partanen, P. Niemelä, L. Mannila, T. Poranen #Racket
• A Coq formalisation of a core of R. ~ M. Bodin #ITP #Coq #Rstats
• Beauty and the beast (Eta Haskell for JVM). ~ Jarek Ratajski #Haskell
• David Hilbert y la defensa del rigor matemático. ~ F. Bombal #Matemáticas
• ASCII fractals in Haskell. ~ Jan Mas Rovira #Haskell
• Logic programming applications: What are the abstractions and implementations? ~ Y.A. Liu #LogicProgramming
• Making agile development processes fit for V-style certification procedures. ~ S. Bezzecchi, P. Crisafulli, C. Pichot, B. Wolff #ITP #IsabelleHOL
• A minimal (<500 LOC) programming language capable of proving theorems about its own terms. #Haskell #Logic
• Un fallo de programación desvió al primer Ariane 5 de 2018 de su trayectoria. ~ @Wicho #Programación
• Let’s not forget the ‘Science’ in ‘Computer Science’. ~ W.S. Saba #CompSci
• Comparing classical and relativistic kinematics in first-order logic. ~ K. Lefever, G. Székely #Logic #Physics
• Modal logic! Propositional logic! Tableaux! ~ R. Zach #Logic
• Boxes and diamonds (An open introduction to modal logic). ~ R. Zach #eBook #Logic
• A multi-language computing environment for literate programming and reproducible research. ~ E. Schulte, D. Davison, T. Dye, C. Dominik #Emacs
• Org-mode and R: An introduction. ~ Erik Iverson #Emacs #OrgMode #Rstats
• The emacs org-mode (Reproducible research and beyond). ~ A. Leha #Emacs #OrgMode #Rstats
• Verified memoization and dynamic programming. ~ S. Wimmer, S. Hu, T. Nipkow #ITP #IsabelleHOL
• Notes on category theory in the context of (functional) programming. ~ J.W. Buurlage #FunctionalProgramming #Haskell #CategoryTheory
• ASTs with Fix and Free. ~ Chris Penner #Haskell
• Getting started with Org mode. ~ Harry Schwartz #Emacs #OrgMode
• SLC2018: Presentación del “Seminario de Lógica Computacional” (2018).
• Reproducibility and Old Faithful. ~ Dominic Steinitz #Haskell #DataScience
• Abstract completion, formalized. ~ N. Hirokawa, A. Middeldorp, C. Sternagel, S. Winkler #IsabelleHOL
• Using Emacs, Org-mode and R for research writing in social sciences (A toolkit for writing reproducible research papers and monographs). ~ Vikas Rawal #Emacs #OrgMode #Rstats
• Coqatoo: Generates natural language versions of Coq proofs. ~ Andrew Bedford #ITP #Coq
• Liquid Haskell tutorial. ~ Andres Löh #Haskell #LiquidHaskell
• Faithful semantical embedding of a dyadic deontic logic in HOL. ~ C. Benzmüller, A. Farjami, X. Parent #ITP #IsabelleHOL #Logic
• Formal proof: reconciling correctness and understanding. ~ C.S. Calude, C. Müller #ITP #Logic
• A collection of short Org-mode snippets demonstrating the usage of code blocks. ~ Eric Schulte #Emacs #OrgMode
• Why data science is simply the new astrology. ~ Karthik Shashidhar #DataScience
• Hoare logics for time bounds. ~ M.P.L. Haslbeck, T. Nipkow #ITP #IsabelleHOL #SLC2018
• Paradigms of artificial intelligence programming: case studies in Common Lisp. ~ Peter Norvig #eBook #AI #CommonLisp
• A categorical manifesto. ~ J.A. Goguen #CategoryTheory #CompSci #Math
• A theory of functional programming. ~ Eric Normand #FunctionalProgramming
• Links to some of the most famous articles about mathematics. #Math
• The death of proof. ~ John Horgan #Math
• The immortaility of proof. ~ Steven G. Krantz #Math
• A DARPA perspective on Artificial Intelligence. ~ John Launchbury #AI
• Interpretable machine learning (A guide for making black box models explainable). ~ Christoph Molnar #MachineLearning #XAI
• Timeline of artificial intelligence. #AI
• Build large polyglot projects with Bazel … now with Haskell support. ~ M. Boespflug, M. Karpov, M. Kowalczyk #Haskell #Bazel
• El sistema de tipos de Haskell/GHC y sus extensiones. ~ Guillaume Hoffmann #Haskell

Marzo 2018

• Fast machine words in Isabelle/HOL. ~ A. Lochbihler #ITP #IsabelleHOL
• Teaching quantum physics to a computer. ~ Oliver Morsch #MachineLearning
• Artificial intelligence and its applications in healthcare and pharmacy. ~ Atul Adhikari #AI
• A reproducible research toolkit. #Emacs #OrgMode #Rstats
• Using Emacs, Org-mode and R for Research Writing in Social Sciences. ~ Vikas Rawal #Emacs #OrgMode #Rstats
• Matemática discreta en Haskell. ~ María Dolores Valverde Rodríguez #Haskell #Matemáticas #OpenLibra
• A theory of architectural design patterns in Isabelle/HOL. ~ Diego Marmsoler #ITP #IsabelleHOL
• From math to machine: translating a function to machine code. ~ Brian Steffens #Programming #Math #Haskell #Imperative_language #Assembly_language #Machine_code #I1M2017
• A Game in Haskell: Dino Rush. ~ Joe Vargas #Haskell #Game
• Comonad Transformers in the Wild. ~ Isaac Elliott #Haskell
• Haskell with Reactive Banana and GTK3. ~ Paul Johnson #Haskell
• CLI program for pretty-printing Haskell datatypes. ~ Dennis Gosnell #Haskell
• A gentle introduction to monad transformers. #Haskell
• Curso intensivo de Google sobre aprendizaje automático e inteligencia artificial (en español). #IA
• Org mode pour LaTeXiens. ~ Fabrice Niessen #Emacs #OrgMode #LaTeX
• Haskell for the imperative. ~ Laurence Emms #Haskell
• Getting started with Haskell. ~ Laurence Emms #Haskell
• The type language. ~ Laurence Emms #Haskell
• Mandelbrot fractal in Haskell. ~ Laurence Emms #Haskell
• Quick specifications for the busy programmer. ~ N. Smallbone, M. Johansson, K. Claessen, M. Algehed #Haskell
• Quick-Sort: a pet peeve. ~ A. Nunes-Harwitt, M. Gambogi, T. Whitaker #Haskell
• Data Science predicts Oscar winner. ~ Lucy Black #AI #DataScience
• Successful companies use Erlang and Elixir. #FunctionalProgramming #Erlang #Elixir
• Natural deduction and the Isabelle proof assistant. ~ J. Villadsen, A. Halkjær, A. Schlichtkrull #ITP #IsabelleHOL #Logic
• NaDeA: A Natural Deduction Assistant with a formalization in Isabelle. #IsabelleHOL #Logic #NaDeA
• The Sequent Calculus Trainer: a tool that aims at supporting students in learning how to correctly construct proofs in the sequent calculus for propositional logic and first-order logic with equality. #Logic
• Proof search in the sequent calculus for first-order logic with equality. ~ Arno Ehle #ATP #Logic
• Image processing with Juicy Pixels and Repa. ~ Mark Karpov #Haskell
• History of Mathematics. ~ Doron Zeilberger #Math #History
• Learning how to prove: From the Coq proof assistant to textbook style. ~ S. Böhne, C. Kreitz #ITP #Coq #Logic
• Concise history of Mathematics. ~ Dirk J. Struik #eBook #Math #History
• Hypothesis: Annotate the web, with anyone, anywhere. ~ @hypothes_is #Annotation
• Haskell without the theory. ~ Saurabh Nanda #Haskell
• Trying out GHC compact regions for improved latency (Pusher case study). ~ Mateusz Kowalczyk #Haskell
• The Sequent Calculus Trainer with automated reasoning (Helping students to find proofs). ~ A. Ehle, N. Hundeshagen, M. Lange #Logic
• In Mathematics, mistakes aren’t what they used to be (Computers can’t invent, but they’re changing the field anyway). ~ Siobhan Roberts #Math #CompSci
• Implicit Runge Kutta and GNU scientific library. ~ Dominic Steinitz #Haskell #Math
• ¿Qué demonios es la programación funcional? ~ Rodrigo de Frutos #ProgramacionFuncional
• Funtores, Aplicativos y Mónadas en imágenes. ~ Miguel Á. Moreno #Haskell
• QWIRE practice: Formal verification of quantum circuits in Coq. ~ R. Rand, J. Paykin, S. Zdancewic #ITP #Coq
• Measuring functions in Criterion. ~ Patrick Dougherty #Haskell
• Simple fractals in Haskell. ~ @Mike_K_Houghton #Haskell
• Hammer for Coq: automation for dependent type theory. ~ Ł. Czajka, C. Kaliszyk #ITP #Coq
• Symbolic execution: intuition and implementation. ~ Alex #Haskell
• Making a text adventure in Haskell (Part 1). ~ Laurence Emms #Haskell
• A Coq formalisation of SQL’s execution engines. ~ V. Benzaken et als. #ITP #Coq
• Applied functional programming course. #Haskell
• Simple puzzle with rotating circles. ~ Ilya V. Portnov #Haskell #Gloss
• Object oriented programming in Haskell. ~ Edsko de Vries #Haskell
• Proof Pearl: Constructive extraction of cycle finding algorithms. ~ D. Larchey-Wendling #ITP #Coq #SLC2018
• MonadFix and the lazy and strict state monad. ~ Moritz Kiefer #Haskell
• Haskell design patterns: The handle pattern. ~ Jasper Van der Jeugt #Haskell
• Implementing a safer sort with linear types. ~ Alexander Vershilov, Arnaud Spiwack #Haskell
• Constructive decision via redundancy-free proof-search. ~ D. Larchey-Wendling #ITP #Coq #SLC2018
• Who needs category theory? ~ A. Blass, Y. Gurevich #CategoryTheory #CompSci
• Generating artwork with Haskell. ~ Benjamin Kovach #Haskell
• Proposal recommends AI training in China’s primary, secondary schools. #AI
• Using Org Mode, LaTeX, Beamer, and Medibang Paint to make a children’s book. ~ Sacha Chua #Emacs #OrgMode #LaTeX #Beamer
• Emacs #1: Ditching a bunch of stuff and moving to Emacs and org-mode. ~ John Goerzen #Emacs #OrgMode
• Emacs #2: Introducing org-mode. ~ John Goerzen #Emacs #OrgMode
• Emacs #3: More on org-mode. ~ John Goerzen #Emacs #OrgMode
• MDP+TA = PTA: Probabilistic timed automata, formalized (short paper). ~ S. Wimmer, J. Hölzl #ITP #IsabelleHOL
• Writing simple Haskell. ~ Gil Mizrahi #Haskell
• Making a text adventure in Haskell (Part 2). ~ Laurence Emms #Haskell
• Clara-rules: Forward-chaining rules in Clojure. #Clojure
• Clojure and AI. ~ Michael Pershyn #Clojure #AI
• Correct-by-construction finite field arithmetic in Coq. ~ J. Philipoom #ITP #Coq #Math
• Data visualization with Haskell: NYC public urination. ~ David Lettier #Haskell #DataScience
• A compendium of clean graphs in R (version 2.0). ~ E.J.Wagenmakers, Q.F. Gronau #Rstats
• Foundations of Mathematics. ~ Ken Kubota #Math #Logic #LamdaCalculus #ITP #IsabelleHOL #Coq #PVS #Agda
• Formalization techniques for asymptotic reasoning in classical analysis. ~ R. Affeldt, C. Cohen, D. Rouhling #ITP #Coq #Math
• Breadth-first search in Haskell. ~ David Lettier #Haskell
• Intelligible Artificial Intelligence. ~ D.S. Weld, G. Bansal #AI #XAI
• How to design programs (2nd edition, 2018). ~ M. Felleisen, R.B. Findler, M. Flatt, S. Krishnamurthi #eBook #Programming #DrRacket
• Weight-balanced trees in Isabelle/HOL. ~ T. Nipkow, S. Dirix #IsabelleHOL
• Max subarray in Haskell. ~ David Lettier #Haskell
• Text Reflow in Haskell. ~ Laurence Emms #Haskell
• Discrete structures. ~ M.G. Knepley #eBook #Math #ITP #Coq
• The OEIS now contains 300,000 integer sequences. ~ C. Lawson-Perfect #Math
• On cryptographic attacks using backdoors for SAT. ~ A. Semenov et als. #SAT
• Verlet integration (Physics simulation in Clojure). ~ M. Metz #Clojure #Physics
• Domain modeling with Haskell data structures. ~ Oskar Wickström #Haskell
• Multiplicar es mas fácil de lo que piensas. ~ Juan Arias de Reyna #Matemáticas #Algorítmica
• Formalized first-order logic. ~ A.H. From. #ITP #IsabelleHOL #Logic
• Course: Functional programming and intelligent algorithms. ~ Hans Georg Schaathun #Haskell #AI
• Narcissus: Deriving correct-by-construction decoders and encoders from binary formats. S. Suriyakarn, C. Pit-Claudel, B. Delaware, A. Chlipala #ITP #Coq
• Formalized unification algorithms. ~ K. Hvidtfeldt #ITP #IsabelleHOL #Logic
• Explanation in Mathematics (in “The Stanford Encyclopedia of Philosophy”). ~ Paolo Mancosu #Math #Philosophy
• Rose trees, breadth-first. ~ Donnacha Oisín Kidney #Haskell
• Lessons learned. ~ Laurence Emms #Haskell
• Haskell’s triangle: or, more fun with recursion. ~ Thomas Cothran #Math #Haskell #JavaScript
• Máquinas listas, pero sin sentido común. ~ Ramon López de Mántaras #IA
• Formalization of a near-linear time algorithm for solving the unification problem. ~ K.F. Brandt #ITP #IsabelleHOL #Logic
• Making a text adventure in Haskell (Part 3). ~ Laurence Emms #Haskell
• Seven sketches in compositionality: An invitation to applied category theory. ~ B. Fong, D.I Spivak #CategoryTheory
• Fundamental tools for Math in 2018. ~ Robert L. Read #Math
• CoCalc: Collaborative Calculation in the Cloud. ~ @cocalc_com #Math #SageMath
• Well-founded unions. ~ J. Dawson, N. Dershowitz, R. Goré #ITP #IsabelleHOL
• Build systems à la carte. ~ A. Mokhov, N. Mitchell, Simon Peyton Jones #Haskell
• Attack trees in Isabelle: CTL semantics, correctness and completeness. ~ F. Kammüller #ITP #IsabelleHOL #Logic
• ‘Grand unified theory of maths’ nets Abel Prize ~ D. Castelvecchi #Math
• From logic and math to code. For dummies. Part III. Dependent types. ~ R. Krivtsov #Logic #FunctionalProgramming
• Argumentation theory for mathematical argument. ~ J. Corneli et als. #Math #Logic
• Two tools for formalizing mathematical proofs. ~ R.Y. Lewis #PhD_Thesis #Math #ITP #Lean #Mathematica
• Eleven simple algorithms to compute Fibonacci numbers. ~ A. Dasdan #Math #Programming #Python
• Ready, set, verify! Applying hs-to-coq to real-world Haskell code. ~ J. Breitner et als. #Coq #Haskell
• containers-verified: Formally verified drop-in replacement of containers. ~ J. Breitner #Haskell #Coq
• La historia del error de división de los primeros Pentium. ~ M.A. Morales | El Aleph #Matemáticas
• (Haskell) modules for the masses. ~ E. Torreborre #Haskell
• In search of God’s perfect proofs. ~ E. Klarreich #Math
• The incompatibility of Fishburn-Strategyproofness and Pareto-efficiency. ~ F. Brandt, M. Eberl, C. Saile and C. Stricker #ITP #IsabelleHOL
• Efficiently improving test coverage with algebraic data types. #Haskell
• Three layer Haskell cake. ~ Matt Parsons #Haskell
• Replacing type classes with records affects optimisation. #Haskell
• SLC2018: Programación funcional en Coq. #ITP #Coq
• SLC2018: Demostraciones por inducción en Coq. #ITP #Coq
• Techie Delight (Coding made easy): 500+ data structure and algorithms problems. ~ @techie_delight #Programming
• SLC2018: Datos estructurados en Coq. #ITP #Coq
• Everyday Haskell (Haskell for the working programmer). ~ Laurence Emms #Haskell
• Simple comparative benchmarks for CSV parsing libraries. #Haskell
• Automatic refinement to efficient data structures: a comparison of two approaches. ~ P Lammich, A Lochbihler #IsabelleHOL
• Thinking recursively in Python. ~ A. Awasthi #Python
• Computations in number theory using Python: A brief introduction. ~ J. Carlson #Python #Math
• A history of interactions between Logic and Number Theory. ~ A. Macintyre #Logic #NumberTheory
• Philosophy of mathematics and computer science. ~ K. Trzęsicki #Math #Logic #CompSci
• Mathematics for computer scientists (Lecture notes). ~ T. Altenkirch #Math #Haskell
• Goldbach’s function approximation using deep learning. ~ A. Stekel, M. Chkroun, A. Azaria #DeepLearning #Math
• Language-integrated provenance in Haskell. ~ J. Stolarek, J. Cheney #Haskell
• Demystifying functional programming (And what that means for learning & teaching). ~ Manuel M T Chakravarty and Gabriele Keller #Haskell
• L’intelligence artificielle, mythes et réalités. ~ Nicolas Rougier #IA
• Mathematical writing. ~ D,E. Knuth, T. Larrabee, and P.M. Roberts #Math
• Making L-Systems with Haskell and Logo. ~ Laurence Emms #Haskell
• Encyclopedia of Combinatorial Structures (ECS). #Math
• An old and a new library for generic deriving. #Haskell
• Building blocks (a more visual approach to the topic of purely-typed functional programming). ~ Steven Vandevelde #FuncionalProgramming #Haskell
• Scott Aaronson: 30 of my favorite books.
• Understanding contravariance. ~ Julie Moronuki and Chris Martin #Haskell
• Welcome to Type Classes! ~ Julie Moronuki and Chris Martin #Haskell

Abril 2018

• Francia invertirá 1.500 millones de euros en inteligencia artificial. #IA
• Parametricity for Bifunctor. ~ Brent Yorgey #Haskell
• Complexity problems in enumerative combinatorics. ~ Igor Pak #Math #CompSci
• L’algorithme quantique de Shor. ~ André Chailloux #CompSci
• IHaskell on mybinder.org ~ Vaibhav Sagar #Haskell #Jupyter #IHaskell
• Free lenses for higher-kinded data. ~ Sandy Maguire #Haskell
• Coq tactics index. ~ Joe Redmon #ITP #Coq
• Emacs #4: Automated emails to org-mode and org-mode syncing. ~ John Goerzen #Emacs #OrgMode
• Ring theory, via coding theory and cryptography. ~ W. David Joyner #eBook #Math #Sagemath
• Calculus on graphs. ~ W. David Joyner #eBook #Math #Sagemath
• There’s more to mathematics than rigour and proofs. ~ Terence Tao #Math
• Emacs for Data Science. ~ Robert Vesco #Emacs #DataScience
• Emacs for Data Science. ~ Ahsan Ijaz #Emacs #DataScience
• Examples using emacs org mode babel inline source code with different backend languages. ~ Derek Feichtinger #Emacs #OrgMode
• Applying computer algebra systems and SAT solvers to the Williamson conjecture. ~ C. Bright, I. Kotsireas, V. Ganesh #Logic #SAT #Math #CAS
• Emacs para ciencias del dato. #Emacs #OrgMode
• Why teaching FP to undergrads is important. ~ Evan Misshula #FunctionalProgramming #Haskell
• The unreasonable relationship between mathematics and physics. ~ David Tong #Math #Physics
• RStartHere: A guide to some of the most useful R Packages that we know about, organized by their role in data science. #Rstat #DataScience
• OrgMode tutorial. ~ Rainer König #Emacs #OrgMode
• What we talk about when we talk about monads. ~ T. Petricek #Haskell
• Seminario (I+A)A (Inteligencia Artificial + Aprendizaje Automático) #IA #AA
• OpenAI challenges you to beat 1990s classic Sonic the Hedgehog using machine learning. ~ #AI
• Comet.ml wants to do for machine learning what GitHub did for code. ~ F. Lardinois #IA #ML
• Deriving Via (or, how to turn hand-written instances into an anti-pattern). ~ B. Blöndal, A. Löh, R. Scott #Haskell
• Learning to prove with tactics. ~ T. Gauthier, C. Kaliszyk, J. Urban, R. Kumar, M. Norrish #ITP #HOL4 #ML
• Org-mode and reproducible research. ~ Evan Misshula #Emacs #OrgMode
• AI for humanity. #AI
• Here’s how the US needs to prepare for the age of artificial intelligence. ~ Will Knight #AI
• Quel langage pour le secondaire? ~ Laurent Bloch #Programming
• A unified approach to solving seven programming problems (functional pearl). ~ W.E. Byrd, M. Ballantyne, G. Rosenblatt, M. Might #FunctionalProgramming #Racket
• Jupyter notebook for beginners: a tutorial. ~ Benjamin Pryke #Jupyter #Python
• Deep Learning: an introduction for applied mathematicians. ~ C.F. Higham, D.J. Higham #AI #ML #DeepLearning
• Plotting in Haskell. ~ James Church #FunctionalProgramming #Haskell
• The simple essence of automatic differentiation (Differentiable functional programming made easy). ~ Conal Elliott #FunctionalProgramming #Haskell
• Tactics and certificates in Meta Dedukti. ~ R. Cauderlier #ITP #Dedukti
• Toward a tool to verify complex data structure invariants. ~ K.D. Roe #PhD_Thesis #ITP #Coq
• The boolean constraint solver of SWI-Prolog: system description. ~ M. Triska #Prolog #ConstraintProgramming
• Logic-Theorist: The sources of the first theorem prover. #ATP
• IHaskell on CoCalc! ~ Vaibhav Sagar #FunctionalProgramming #Haskell #CoCalc
• Welcome Haskell on CoCalc. #FunctionalProgramming #Haskell #CoCalc
• Deep learning: Why it’s time for AI to get philosophical. ~ Catherine Stinson #AI #Philosophy
• Dynamic programming in Haskell. ~ Laurence Emms #FunctionalProgramming #Haskell
• Voronoi: A Haskell implementation of Fortune’s algorithm. #FunctionalProgramming #Haskell
• ‘Live coding’: desnudando a las máquinas a golpe de música. ~ Álvaro Lorite #Música #Programación
• Getting started with Emacs text editor. ~ Sachin Patil #Emacs #OrgMode #I1M2017
• How to create LaTeX documents with Emacs. ~ Sachin Patil #Emacs #OrgMode #LaTeX #I1M2017
• A footnote to “The crisis in contemporary mathematics”. ~ B. Katz, M.G. Katz, S. Sanders #Logic #Math
• Magit interface walkthrough. #Emacs #Magit
• Using Cloud Haskell to write a type-safe distributed chat. ~ Sebastian Pulido Gomez #Haskell
• Why does “=” mean assignment? ~ Hillel Wayne #Programming
• Ten simple rules for responsible big data research. #BigData
• Over 130 practical recipes for data analysis and machine learning. #Haskell #DataScience
• Introduction to Iltis: An interactive, Web-Based system for teaching logic. ~ G. Geck et als. #Teaching #Logic
• Modal logic playground (A graphical semantic calculator for modal propositional logic). ~ Ross Kirsling #Teaching #Logic
• Data engineers vs. data scientists. ~ Jesse Anderson #DataScience
• Property based integration testing using Haskell! ~ Kristijan Šarić #Haskell
• Twenty-four EU countries sign artificial intelligence pact in bid to compete with US & China. #AI
• Mike Gordon and hardware verification. ~ L. Paulson #ITP
• Evaluating winding numbers through Cauchy indices in Isabelle/HOL. ~ W. Li, L.C. Paulson #ITP #IsabelleHOL #Math
• What we talk about when we talk about monads. ~ T. Petricek #Haskell
• For mathematicians, = does not mean equality. ~ Jeremy Kun #Math #CompSci
• Math, music and imagination. ~ Marcus Miller #Math #Music
• Jupyter is where humans and data science intersect. ~ Paco Nathan #Jupyter #DataScience
• Scientific Python in the browser. ~ M. Droettboom #Python #DataScience
• Introduction to literate programming. ~ Howard Abrams #Emacs #OrgMode
• SLC2018: Soluciones lógicas de problemas lógicos. #Logic #Prolog #CLP
• Talk to Books (Browse passages from books using experimental AI). #AI
• Algorithms from AIMA (Artificial intelligence: a modern approach) in Haskell. ~ Chris Taylor #AI #Haskell
• Python implementation of algorithms from Russell And Norvig’s “Artificial Intelligence: A Modern Approach”. #AI #Python #Jupyter
• pycse - Python3 computations in science and engineering. ~ John Kitchin #eBook #Python
• Scimax: an Emacs starterkit designed for people interested in reproducible research and publishing. ~ John Kitchin #Emacs #OrgMode
• Gallery of named graphs (with tkz-berge.sty). ~ Alain Matthes #LaTeX #Math
• Using Cloud Haskell to write a type-safe distributed chat. ~ Sebastian Pulido Gomez #Haskell
• Why does “=” mean assignment? ~ Hillel Wayne #Programming
• A formal semantics of the core DOM in Isabelle/HOL. ~ A.D. Brucker, M. Herzberg #ITP #IsabelleHOL
• “Python computations in science and engineering” in Org mode ~ John Kitchin #Emacs #OrgMode #Python
• AITP 2018: The Third Conference on Artificial Intelligence and Theorem Proving (Abstracts of the talks). #AI #ATP #ITP
• Axiomatizing category theory in free logic. ~ C. Benzmüller, D.S. Scott #ITP #IsabelleHOL #CategoryTheory
• Safe reinforcement learning via formal methods (Toward safe control through proof and learning). ~ N. Fulton, A. Platzer #AI #ML #ATP
• Let’s make set theory great again! ~ John Harrison #ITP
• If mathematical proof is a game, what are the states and moves? ~ David McAllester #AI #ATP #ML #Math
• Intelligence artificielle: les angles morts du rapport Villani. ~ Hervé Mariton et Cyrille Dalmont #AI
• Very powerful data analysis environment – org mode with ob-ipython. ~ Robert Kozikowski #Emacs #OrgMode #Python #DataScience
• Some tips for learning Org Mode for Emacs. ~ Sacha Chua #Emacs #OrgMode
• Efficient verification of imperative programs using auto2. ~ B. Zhan #IsabelleHOL
• The meaning of = for logic programmers. ~ Markus Triska #LogicProgramming #Prolog
• Boolos’ hardest logic puzzle ever in its purest form. ~ J.J. Colomina-Almiñana, P.R. Stinga #Logic
• A better programming language for Data Science/Machine Learning. #Haskell #DataScience
• Working with lists. ~ Laurence Emms #Haskell
• The best of Python: a collection of my favorite articles from 2017 and 2018 (so far). ~ Gergely Szerovay #Python
• What the history of Math can teach us about the future of AI. ~ Nathan Myhrvold #Math #AI
• Why Haskell is hot for cryptocurrencies. ~ Niklas Hambüchen #Haskell
• Program reduction: a win for recursion schemes. ~ John Wiegley #Haskell
• Why you need Python environments and how to manage them with Conda. ~ Gergely Szerovay #Python
• Peligro: algoritmos al mando en la escuela. ~ Cathy O’Neill
• Armas de destrucción matemática: Cómo el big data aumenta la desigualdad y amenaza la democracia. ~ Cathy O’Neil #Libro #Matemáticas #BigData
• Linear algebra with applications. ~ W. Keith Nicholson #eBook #Math #OpenLibra
• Límites y paradojas de la evaluación científica. ~ Daniel Innerarity
• History of interactive theorem proving. ~ J. Schöpf, S. Widauer #ITP #DAO2018
• Course: Machine learning for theorem proving. ~ C. Kaliszyk #ATP #AI #ML
• Constructive analysis of S1S and Büchi automata. ~ M. Lichter, G. Smolka #ITP #Coq
• Evidence-providing problem solvers in Agda. ~ U. Zalakain #ITP #Agda
• Erlang: The power of functional programming. ~ S. Thompson #FunctionalProgramming #Erlang
• Functional reactive programming. ~ B. Siegel #FunctionalProgramming
• Semantic Web and Machine Learning. ~ F. Železný #ILP
• El resurgir de la programación funcional. #ProgramaciónFuncional #Haskell #Erlang #Elixir #Scala #Clojure #Fsharp
• Why monads? ~ Luca Belli #Haskell
• JupyterLab is ready for users. #Jupyter
• Machine Learning is fun! (The world’s easiest introduction to Machine Learning). ~ Adam Geitgey #AI #MachineLearning
• A quick guide to Emacs Lisp programming. ~ Chris Done #Emacs #Lisp
• Emacs is sexy! #Emacs
• Awesome Emacs: A community driven list of useful Emacs packages, libraries and others. #Emacs
• Here’s why so many data scientists are leaving their jobs. ~ Jonny Brooks-Bartlett #DataScience
• Programming languages commonly used features in a side-by-side format. #Programming
• 10 libros de filosofía imprescindibles. ~ Filosofía&Co #Filosofía
• Org Babel recipes. #Emacs #OrgMode #Babel
• Higher-Kinded Data. ~ Sandy Maguire #Haskell
• Making a text adventure in Haskell (Part 4). ~ Laurence Emms #Haskell #Game
• Verifying local definitions in Coq. ~ J. Breitner #Haskell #Coq
• How to think like a programmer (lessons in problem solving). ~ Richard Reis #Programming
• Using functions for easier programming. ~ N. Savage #FunctionalProgramming #Haskell
• Formalising mathematics in simple type theory. ~ L.C. Paulson #ITP #Math #IsabelleHOL #HOL_Light
• Emacs #5: Documents and presentations with Org-Mode. ~ John Goerzen #Emacs #OrgMode #LaTex #Beamer
• Formal verification of platoon control strategies. ~ A. Rashid, U. Siddique, O. Hasan #ITP #HOL_Light
• Funflow: typed resumable workflows. ~ N. Clarke, A. Hermann, T. Nielsen #Haskell
• Bounded natural functors with covariance and contravariance in Isabelle/HOL. ~ A. Lochbihler, J. Schneider #ITP #IsabelleHOL
• Machine learning evolution (infographic). ~ A. Morrison and A. Rao #AI #MachineLearnig #History
• Best Haskell programming books for functional programming. #Haskell
• Kurt Gödel and the mechanization of mathematics. ~ J. Kennedy #Logic #Math
• Beauty and the beast (Eta Haskell on JVM). ~ Jarek Ratajski #Haskell
• DLV: Evolution and perspectives. ~ M. Alviano et als. #LogicProgramming #ASP #DLV
• New A.I. application can write its own code. ~ J. Boyd-Rice #AI
• The significance of Philosophy to Mathematics. ~ Richard Zach #Math #Philosophy
• Modelling bitcoin in Agda. ~ A. Setzer #ITP #Agda
• Quantifier elimination for reasoning in economics. ~ C.B. Mulligan et als. #Logic
• Asynchronous exception handling in Haskell. ~ M. Snoyman #Haskell
• Smarties: a general purpose behavior tree library written in Haskell. #Haskell #AI
• Iterating squared digit sum. ~ Brent Yorgey #Haskell #Math
• The Software Foundations book, in GHC. ~ Ryan Scott #Haskell
• Introduction to functional programming in Python. ~ Spiro Sideris #Python #FunctionalProgramming
• Proof and other dilemmas: Mathematics and Philosophy (Reviewed by Jeremy Avigad). #Math #Philosophy
• Formalization of a polymorphic subtyping algorithm. ~ J. Zhao, B.C.S. Oliveira, T. Schrijvers #ITP #Abella
• The Babel of languages and the substrate of nature. ~ Philip Thrift #Programming
• Applied category theory course: ordered sets. ~ John Carlos Baez #Math #CategoryTheory
• Developing bug-free machine learning systems with formal mathematics. ~ D. Selsam, P. Liang, D.L. Dill #ITP #Lean #MachineLearnig
• Martin-Löf’s type theory (MLTT). ~ Larry Diehl #Logic
• Org mode syntax example. ~ Fabrice Niessen #Emacs #OrgMode
• Formas de incluir bibliografías en documentos Org. #Emacs #OrgMode #I1M2017
• A formally-proved algorithm to compute the correct average of decimal floating-point numbers. ~ S. Boldo, F. Faissole, V. Tourneur #ITP #Coq #Math
• Decades-old graph problem yields to amateur mathematician. ~ Evelyn Lamb #Math
• Un famoso «gurú» de la vida eterna resuelve un problema matemático de hace 60 años. #Matemáticas
• SBV: SMT Based Verification in Haskell (Released: April 29th, 2018). #Haskell #SMT #SBV
• Communication Artificial Intelligence for Europe. #AI

Mayo 2018

• Mechanising and verifying the WebAssembly specification. ~ C. Watt #IsabelleHOL #WebAssembly
• WebAssembly in Isabelle/HOL. ~ C. Watt #IsabelleHOL #WebAssembly
• Dockerizing our Haskell app. ~ James Bowen #Haskell #Docker
• Indian Supreme Court rules that CS degrees cannot be provided on-line. ~ Mark Guzdial #Education #CompSci
• Using machine learning to improve cylindrical algebraic decomposition. ~ Z. Huang, M. England, D. Wilson, J.H. Davenport, L.C. Paulson #MachineLearning #Logic
• Courses on mathematical thinking now underway. ~ Sue Gee #Math #Logic #CompSci
• The Metamorphosis of Escher through tours.
• Gröbner bases of modules and Faugère’s F4 algorithm in Isabelle/HOL. ~ A. Maletzky, F. Immler #ITP #IsabelleHOL #Math
• Abe-Ohkubo-Suzuki linkable ring signatures. ~ A. Centelles, S. Diehl #Haskell
• Las matemáticas que descifraron la máquina «Enigma» de los nazis. ~ Paz Jiménez Seral y Manuel Vázquez Lapuente #Matemáticas
• Exploiting Answer Set Programming with external sources for meta-interpretive learning. ~ T. Kaminski, T. Eiter, K. Inoue #ASP #ILP
• Using SWISH to realise interactive web based tutorials for logic based languages. ~ J. Wielemaker, F. Riguzzi, R. Kowalski, T. Lager, F. Sadri, M. Calejo. #LogicProgramming #Prolog #SWISH
• Edit-time tactics in Idris. ~ Joomy Korkut. #Idris
• Rosetta Haskell (how abstractions are used by sequentially rewriting a program to do exactly the same thing using different techniques). ~ Chas Leichner #Haskell
• Advanced techniques for reducing Emacs startup time. ~ Joe Schafer #Emacs
• Variations on inductive-recursive definitions. ~ N. Ghani et als. #Agda
• VerifyThis 2018 - Polished Isabelle solutions. ~ P. Lammich and S. Wimmer #IsabelleHOL
• Parametrised unit tests in Haskell. ~ Mark Seemann #Haskell
• Formal process virtual machine for smart contracts verification. ~ Z. Yang, H. Lei #Coq
• Learning logic and proof with an interactive theorem prover. ~ J. Avigad #Logic #ITP #Lean
• Logic and proof (Release 0.1). ~ J. Avigad, R.Y. Lewis, F. van Doorn #Logic #ITP #Lean
• Writing LaTeX with Org Mode. #Emacs #OrgMode #LaTeX
• Sistema de Deep Learning para el reconocimiento de palabras manuscritas implementado en TensorFlow y entrenado con IAM Handwriting Database. ~ Hugo Rubio #DeepLearning
• De resolver ecuaciones a aprendizaje profundo: Un tutorial de TensorFlow Python. ~ Oliver Holloway #DeepLearning
• From solving equations to Deep Learning: A TensorFlow Python tutorial. ~ Oliver Holloway #DeepLearning
• Type-level induction in Haskell. ~ Donnacha Oisín Kidney #Haskell
• The lambda calculus. ~ J. Alama, J. Korbmacher #Logic
• Deep learning comes full circle. ~ N. Collins #DeepLearning
• Formal specification for a Cardano wallet. ~ D. Coutts, E. de Vries #Cardano
• AI researchers allege that machine learning is alchemy. ~ M. Hutson #MachineLearnig
• Making an ecosystem simulation in Haskell (Part 1). ~ Laurence Emms #Haskell
• Dynamic programming in Haskell is just recursion. ~ Travis Athougies #Haskell
• Machine learning tutorial:
  • ML basics and experimenting
  • From text to features and NLP-oriented intro to selected learning algorithms.
  • Mallet in UIMA: experiments with ClearTK and Lab.
  • WEKA API brief and highlight of further topics.
• Procedural generation of polyrhythmic beats. ~ Luke Palmer #Haskell
• Conversations with a six-year-old on functional programming. ~ Brent Yorgey #FunctionalProgramming
• A brief introduction to literate analytics with Org-Babel. ~ Nick Barnwell #Emacs #OrgMode
• Introducción a la programación con Python 3. ~ José Luis Chiquete Valdivieso #Python
• C is not a low-level language (Your computer is not a fast PDP-11). ~ David Chisnall #Programming
• The Humanities of Maths/Computer Science. ~ L.P. Cruz #Math #CompSci
• MagicHaskeller: An inductive functional programming system for casual/beginner Haskell programmers. ~ Susumu Katayama #Haskell
• The Const Applicative and Monoids. ~ Justin Le #Haskell
• From math to machine: translating a function to machine code. ~ Brian Steffens #Programming #Math #Haskell #Imperative_language #Assembly_language #Machine_code #I1M2017
• An Isabelle/HOL formalization of the modular assembly kit for security properties. ~ O. Bračevac et als. #IsabelleHOL
• Vectorization in Haskell. ~ Abhiroop Sarkar #Haskell
• A curated collection of free eBooks about Haskell. #Haskell
• 8 time complexities that every programmer should know. ~ Adrián Mejía #Algorithmic
• Revisiting decision diagrams for SAT. ~ T. van Dijk, R. Ehlers, A. Biere #Logic #ATP #SAT
• Machine learning guidance and proof certification for connection tableau. ~ M. Färber, C. Kaliszyk, J. Urban #MachineLearning #ATP #Prolog
• Explicit memoization can be elegant; a response to “Dynamic programming in Haskell is just recursion”. ~ Dan Burton #Haskell
• Type-level induction in Haskell. ~ Donnacha Oisín Kidney #Haskell
• Follow the denotation. ~ Sandy Maguire #Haskell
• Proof mining with dependent types. ~ E. Komendantskaya, J. Heras #ITP #Coq #MachineLearning
• The HKD pattern and type-level SKI. ~ Tom Ellis #Haskell
• Machine learning: A quick and simple definition. ~ James Furbush #AI #MachineLearning
• La hipótesis de Riemann y el problema P = NP. ~ Juan Arias de Reyna #Matemáticas #Computación
• Functional baby talk: Analysis of code fragments from novice Haskell programmers. ~ J. Singer, B. Archibald #Haskell
• Los puentes de Königsberg: Estudio y resolución con Haskell. ~ Miguel Ibáñez #Hakell #Matemáticas
• Proceedings of the 25th Automated Reasoning Workshop (Bridging the Gap between Theory and Practice). #ATP
• Qué hacer ante la “tecnupidez”. ~ Mario Bunge #Ciencia #Tecnología
• ¿Qué es la tecnología? ~ Dominique Raynaud #Ciencia #Tecnología
• ASP in industrial contexts: applications and toolchain. ~ Francesco Ricca #Logic #Programming #ASP
• Writing bug-free code using theorem provers. ~ Aaron Stump #ITP
• Proof assistants: from symbolic logic to real mathematics? ~ Lawrence C Paulson #ITP #Logic #Math
• Math can’t solve everything: questions we need to be asking before deciding an algorithm is the answer. ~ J. Williams, L. Gunn #Algorithms
• Automatic differentiation in machine learning: a survey. ~ Atılım Güneş Baydin et als. #AD #AutomaticDifferentiation #ML #MachineLearning
• Automatic differentiation. ~ Edward Kmett #Haskell #AD #AutomaticDifferentiation
• La Inteligencia Artificial no es como en las películas. ¿Qué es? #IA
• My Lisp experiences and the development of GNU Emacs. ~ Richard Stallman #Lisp #Emacs
• Intelligence artificielle et pensée humaine. ~ Margarida Romero #IA
• Exercícios resolvidos em Prolog sobre sistemas baseados em conhecimento. ~ Paulo Cortez #Prolog
• A purely functional typed approach to trainable models (Part 1). ~ Justin Le #Haskell #MachineLearning
• The RedPRL proof assistant. ~ C. Angiuli, E. Cavallo, K.B. Hou, R. Harper, J. Sterling. #ITP
• Carnegie Mellon University starts first AI degree program in U.S. ~ K. Johnson. #AI
• Bachelor of Science in Artificial Intelligence (CMU): Curriculum. #AI
• Deductive mathematics (an introduction to proof and discovery for mathematics education). ~ A. Wohlgemuth #eBook #Math
• Pensée informatique et géométrie. ~ A. Busser, P. Debrabant, S. Gonifei #Math #Programming
• Haskell communities and activities report (May 2018). #Haskell
• Verifying code toward trustworthy software. ~ Hyong-Soon Kim and Eunyoung Lee #FormalVerification
• I-MAKS (A framework for information-flow security in Isabelle/HOL). ~ S Grewe, H Mantel, M Tasch, R Gay, H Sudbrock #ITP #IsabelleHOL
• High-level signatures and initial semantics. ~ B. Ahrens, A. Hirschowitz, A. Lafont, M. Maggesi #ITP #Coq
• Emacs tools for writers. #Emacs
• 5 Emacs modes for writers. ~ Scott Nesbit #Emacs
• To build truly intelligent machines, teach them cause and effect. #AI
• The book of why (The new science of cause and effect). ~ Judea Pearl, Dana Mackenzie #Science #AI
• Catamorphisms and F-algebras. ~ Alexey Avramenko #Haskell
• Create Blockchain in Haskell. ~ Gaurav Agrawal #Haskell #Blockchain
• Proof pearl: Magic wand as frame. ~ Qinxiang Cao, Shengyi Wang, Aquinas Hobor, and Andrew W. Appel #ITP #Coq
• Advanced Github: Webhooks and automation. ~ James Bowen #Haskell
• Proof reuse in Coq using existential variables. ~ J. Breitner #ITP #Coq
• A Coq formalization of digital filters. ~ Diane Gallois-Wong, Sylvie Boldo, and Thibault Hilaire #ITP #Coq
• Formalization of the arithmetization of euclidean plane geometry and applications. ~ Pierre Boutry, Gabriel Braun, Julien Narboux #ITP #Coq #Math
• A general formal memory framework in Coq for verifying the properties of programs based on higher-order logic theorem proving with increased automation, consistency, and reusability. ~ Zheng Yang, Hang Lei #ITP #Coq
• Performance and feature case studies in ecstasy. ~ Sandy Maguire #Haskell
• Artificial Intelligence’s ethical challenges. ~ L. Zacharias #AI #Ethics
• Cartography in Haskell. ~ Dominic Steinitz #Haskell
• Revisiting the tree edit distance and its backtracing: A tutorial. ~ B. Paaßen #Algorithms
• First experiments with neural translation of informal to formal mathematics. ~ Q. Wang, C. Kaliszyk, J. Urban #MachineLearning #Math
• Free monoidal functors, categorically! ~ Bartosz Milewski #haskell #CategoryTheory
• Direct interpretation of functional programs for debugging. ~ J. Whitington, T. Ridge #FunctionalProgramming
• Vector Programming using structural recursion (An introduction to vectors for beginners). ~ M.T. Morazán #Racket
• Using Elm to introduce algebraic thinking to K-8 students. ~ C. d’Alves et als. #Elm
• Teaching Erlang through the Internet: an experience report. ~ S. Adams #Erlang
• How I evaluate Haskell packages. ~ G. Gonzalez #Haskell
• Making an ecosystem simulation in Haskell (Part 2). ~ Laurence Emms #Haskell
• DeepLogic: end-to-end logical reasoning. ~ N. Cingillioglu, A. Russo #Logic #MachineLearnig
• Reinforcement learning of theorem proving. ~ C. Kaliszyk, J. Urban, H. Michalewski, M. Olšák #Logic #ATP #MachineLearnig
• Can machine learning identify interesting mathematics? An exploration using empirically observed laws. ~ Chai Wah Wu #MachineLearning #Math
• Formalizing (Web) standards: an application of test and proof. ~ A.D. Brucker, M. Herzberg #ITP #IsabelleHOL
• Number sequence prediction problems and computational powers of neural network models. ~ H. Nam, S. Kim, K. Jung #MachineLearning #Math
• Teaching two programming languages in the first CS course. ~ M. Guzdial #Teaching #Programming
• A classical math problem gets pulled into the modern world. ~ K. Hartnett #Math
• Probabilistic timed automata in Isabelle/HOL. ~ S. Wimmer, J. Hölzl #IsabelleHOL
• Hidden Markov models. ~ S. Wimmer #IsabelleHOL
• QuickCheck vs SmallCheck. ~ R. Cheplyaka #Haskell
• Polinomios contra ordenadores cuánticos. ~ I. Luengo #Matemáticas #Computación
• Technical writing: Learning from Kernighan. ~ Two Wrongs #Programming
• Microsoft is creating an oracle for catching biased AI algorithms. ~ W. Knight #AI
• The US military is funding an effort to catch deepfakes and other AI trickery. ~ W. Knight #AI
• Proving program correctness using the AG semantics: an example with n-Queens. ~ A. Harrison #ASP
• Free AI course from Finland. ~ S. Gee #AI
• Haskell/GHC symbol search cheatsheet. ~ Takenobu Tani #Haskell
• Combinatorics of permutations. ~ M. Bona #Math
• Combinatorics of permutations in Haskell: Introduction. ~ Vinay Madhusudanan #Haskell #Math
• Haskell: an introduction. ~ Sylvain Henry #Haskell
• Extensible ADT (EADT). ~ Sylvain Henry #Haskell
• Fast Haskell coding with cushions. ~ Roman Gonzalez #Haskell
• Irrational rapidly convergent series in Isabelle/HOL. ~ A. Koutsoukou Argyraki, W. Li #ITP #IsabelleHOL #Math
• Haskell Lens Operator Onboarding. ~ Russell Matney #Haskell
• Definitions of mathematics. #Math
• One Monad to prove them all (Functional pearl). ~ J- Christiansen, S. Dylus, F. Teegen #ITP #Coq #Haskell
• One formalization of virtue ethics via learning. ~ N.S. Govindarajulu, S. Bringjsord, R. Ghosh #AI
• A toolchain to produce correct-by-construction OCaml programs. ~ J.C. Filliâtre et als. #FunctionalProgramming #OCaml #Why3
• Axiom systems for category theory in free logic. ~ C. Benzmüller and D. Scott #ITP #IsabelleHOL #Math #Logic
• Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. ~ A Semenov et als. #SAT
• Functional pearl: La tour d’Hanoï. ~ R. Hinze #FuncionalProgramming #Haskell
• Simulation of mathematical games using functional programming. ~ D. Murphy #FuncionalProgramming #Haskell #Math #Games
• LaTeX notes for professionals book. #LaTeX
• Visualizing Cantor’s zig zag. ~ Patrick Honner #Math
• Lisp, Jazz, Aikido (three expressions of a single essence). ~ Didier Verna #FunctionalProgramming #Lisp
• f-strings in emacs-lisp. ~ John Kitchin #Emacs #Elisp
• Automated verification of neural networks: Advances, challenges and perspectives. ~ F. Leofante et als. #AutomatedReasoning #MachineLearning
• Monadification, memoization and dynamic programming in Isabelle/HOL. ~ S. Wimmer, S. Hu and T. Nipkow #ITP #IsabelleHOL #Algorithms
• Block puzzle in Haskell. ~ @__seroron #Haskell
• Computation-as-deduction in Abella: work in progress. ~ K. Chaudhuri, U. Gérard, D. Miller #ITP #Abella
• Announcing the Facebook Testing and Verification request for research proposals.
• ¿Realidad o ficción? Inteligencia artificial que nos engaña como por arte de magia. ~ Cristina Sánchez #IA
• Nix: Haskell concepts for package managment. ~ James Bowen #Haskell #Nix
• Automated proof synthesis for propositional logic with deep neural networks. ~ T. Sekiyama, K. Suenaga #Logic #ATP #DeepLearning
• Purely functional AVL trees in Common Lisp. #CommonLisp
• DeepProbLog: Neural probabilistic logic programming. ~ R. Manhaeve et als. #LogicProgramming #DeepLearning
• How close are we—really—to building a quantum computer? ~ Larry Greenemeier #CompSci
• Constructive Mathematics. ~ D. Bridges #Logic #Math
• Un mainframe IBM 1401 de 1959 compilando Fortran. ~ @Alvy #Programación #Computación
• History of programming languages. #Programming #CompSci
• Timeline of programming languages. #Programming #CompSci

Junio 2018

• Optimal binary search trees in Isabelle/HOL. ~ T. Nipkow and D. Somogyi #ITP #IsabelleHOL #Algorithms
• Functional programming and legacy software (Using PureScript to extend a legacy JavaScript system). ~ C. Fischer #PureScript
• Syntax and semantics for operations with scopes. ~ M. Piróg, T. Schrijvers, N. Wu, M. Jaskelioff #Haskell
• Mathematical essentials of quantum computing. ~ J. Rué, S. Xambó #Math #CompSci
• Learn You a Physics for Great Good! ~ B. Werner, E. Sjöström, J. Johansson, O. Lundström #eBook #Haskell #Physics
• Certified ordered completion in Isabelle/HOL. ~ C. Sternagel, S. Winkler #ITP #IsabelleHOL
• Modular verification of programs with effects and effect handlers in Coq. ~ T. Letan, Y. Régis-Gianas, P. Chifflier, G. Hiet #ITP #Coq
• A more precise, more correct stack and register model for CompCert. ~ G. Barany #ITP #Coq
• Handling recursion in generic programming using closed type families. ~ A. Bolotina, A. Pelenitsyn #FunctionalProgramming #Haskell
• Algorithms notes for professionals. #eBook #Algorithms
• Purely functional and declarative GTK+ programming in Haskell. ~ Oskar Wickström #Haskell
• Domain specific languages of mathematics: lecture notes. ~ Patrik Jansson, Cezar Ionescu. #Haskell #Math
• Semi-formal development: The Cardano wallet. ~ Edsko de Vries #Haskell
• Programming by poking: why MIT stopped teaching SICP (The Structure and Interpretation of Computer Programs). ~ Yarden Katz #Programming
• Course CMU 15-150: Functional programming, summer 2018. #FunctionalProgramming #SML
• Introductory Computer Science Education at Carnegie Mellon University: A Deans’ Perspective. ~ R.E. Bryant, K. Sutner, M.J. Stehlik #Teaching #CompSci
• Some thoughts on teaching functional programming. ~ R. Harper #Teaching #FuncionalProgramming
• Galileo is the genesis of a symbolic and numerical math tool written in Scala; a Computer Algebra System (CAS). #Scala #Math #CAS
• Making an ecosystem simulation in Haskell (Part 3). ~ Laurence Emms #Haskell
• Explaining explanations: an approach to evaluating interpretability of machine learning. ~ L.H. Gilpin et als. #XAI #AI #MachineLearning
• Haskell-based CoinMetrics.io tools. #Haskell
• Codeworld: Haskell as a first programming language. ~ James Bowen #Haskell #Codeworld #Teaching
• You should learn functional programming in 2018. ~ Allan MacGregor #FunctionalProgramming
• Linux notes for professionals. #eBook #Linux
• Bloque de GAP de la asignatura Software Matemáticas. ~ Pedro A. García-Sánchez #CAS #SageMath
• GAP (groups, algorithms, programming) a system for computational discrete algebra. #CAS
• Monad transformers for the easily confused. ~ @TheWizardTower #Haskell
• GitHub alternative top 7 sites to host your open source project. #GitHub
• Top GitHub alternatives to host your open source project. ~ Abhishek Prakash #GitHub
• GamePad: a learning environment for theorem proving. ~ D. Huang, P. Dhariwal, D. Song, I. Sutskever #ITP #Coq #MachineLearning
• A new style of mathematical proof. ~ W.M. Farmer #Logic #Math
• A decision procedure for univariate polynomial systems based on root counting and interval subdivision. ~ C. Munoz, A. Narkawicz, A. Dutle #ITP #PVS #Math
• Calculational verification of reactive programs with reactive relations and Kleene algebra. ~ S. Foster, K. Ye, A. Cavalcanti, J. Woodcock #ITP #IsabelleHOL
• Generating art with Haskell. #Haskell
• Breadth-first traversals in far too much detail. ~ Donnacha Oisín Kidney #Haskell
• Haskell RIP tutorial. ~ @RipTutorial #Haskell
• Deriving via (or, how to turn hand-written instances into an anti-pattern). ~ B. Blöndal, A. Löh, R. Scott #Haskell
• This algorithm can tell which number sequences a human will find interesting. #AI #MachineLearning #Math
• Formalization of the undecidability of the halting problem for a functional language. ~ T. M. Ferreira Ramos et al. #ITP #PVS
• Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. ~ M. Wenzel #ITP #IsabelleHOL
• Essential cheat sheets for machine learning and deep learning engineers. ~ Vivian Chong #MachineLearning #DeepLearning
• Suggesting valid hole fits for typed-holes. ~ Matthías Páll Gissurarson #Haskell
• Category theory proofs in Idris. ~ Jesse Hallett #Idris #CategoryTheory
• How does Idris compare to other dependently-typed programming languages? ~ Edwin Brady #Idris
• Las matemáticas del fútbol y el nuevo ministro de cultura. ~ Juan Arias de Reyna #Matemáticas #Computación
• Formalization of Lerch’s theorem using HOL Light. ~ A. Rashid, O. Hasan #ITP #HOL_Light #Math
• Formal small-step verification of a call-by-value lambda calculus machine. ~ F. Kunze, G. Smolka, Y. Forster #ITP #Coq
• Lenses embody Products, Prisms embody Sums. ~ Justin Le #Haskell
• Formalizing constructive quantifier elimination in Agda. ~ J. Pope #ITP #Agda #Logic
• A dyadic deontic logic in HOL. ~ C. Benzmüller, A. Farjami, X. Parent #ITP #IsabelleHOL #Logic
• A formalization of the LLL basis reduction algorithm. ~ J. Divasón, S. Joosten, R. Thiemann, A. Yamada #ITP #IsabelleHOL
• Machine learning predicts World Cup winner. #MachineLearning
• Prediction of the FIFA World Cup 2018: A random forest approach with an emphasis on estimated team ability parameters. ~ A. Groll et als. #MachineLearning
• LISP: back to the future (a tribute to 60th anniversary). ~ Nikolay Mozgovoy #Programming #Lisp
• The surprising security benefits of end-to-end formal proofs. ~ Adam Chlipala
• Goal-oriented conjecturing for Isabelle/HOL. ~ Y. Nagashima, J. Parsert #ITP #IsabelleHOL
• Mining the Archive of Formal Proofs. ~ J. Blanchette, M. Haslbeck, D. Matichuk, T. Nipkow #ITP #IsabelleHOL
• Mettre l’éthique dans l’algorithme? ~ Catherine Tessier, Vincent Bonnemains, Claire Saurel
• Séquences d’algorithmique en mathématique en Python 3, de la seconde à la terminale. ~ Hubert Raymondaud #Python
• A complete computing environment. #Emacs
• Emacs as a complete computing environment. ~ Ryan Rix #Emacs
• Skolem’s paradox. ~ Timothy Bays #Logic
• 100 years of Zermelo’s axiom of choice: what was the problem with it? ~ Per Martin-Löf #Logic #Math
• Functional Pearl: Theorem Proving for all (Equational reasoning in Liquid Haskell). ~ N. Vazou, J. Breitner, W. Kunkel, D. van Horn, G. Hutton #Hakell #LiquidHaskell
• Foundations of Mathematics: a discussion of sets and types. ~ Dominik Kirst #Logic #Math
• Formal small-step verification of a call-by-value lambda calculus machine. ~ F. Kunze, G. Smolka, Y. Forster #ITP #Coq
• Substitutionless first-order logic: a formal soundness proof. ~ A.H. From, J.B Larsen, A. Schlichtkrull, J. Villadsen #ITP #IsabelleHOL #Logic
• Ghosts for lists: from axiomatic to executable specifications. ~ F. Loulergue, A. Blanchard, N. Kosmatov #ITP #Coq
• Engaging millennials into learning formal methods. ~ N. Cataño #Teaching #FormalMethods
• PaMpeR: a proof method recommendation system for Isabelle/HOL. ~ Y. Nagashima, Y. He #ITP #IsabelleHOL
• Projective geometry in Isabelle/HOL. ~ Anthony Bordg #ITP #IsabelleHOL #Math
• Smart constructors that cannot fail. ~ Mark Karpov #Haskell
• The localization of a commutative ring in Isabelle/HOL. ~ Anthony Bordg #ITP #IsabelleHOL #Math
• International Olympiad in Isabelle? #IsabelleHOL
• Formalizing category theory and presheaf models of type theory in Nuprl. ~ Mark Bickford #ITP #Nuprl #CategoryTheory
• Source Plugins: Four ways to build a typechecked Haskell expression. ~ Matthew Pickering #Haskell
• A promise checked is a promise kept: inspection testing. ~ Joachim Breitner #Haskell
• Python notes for professionals. #Python
• The inside story of how AI got good enough to dominate Silicon Valley. #AI
• Diálogos entre Arquitectura, Ciudad y Computación. ~ F. Sancho #NetLogo
• Hyper natural deduction for Gödel Logic: a natural deduction system for parallel reasoning. ~ A. Beckmann, N. Preinin #Logic
• R language for programmers. ~ John D. Cook #Rstats
• Web Prolog and the programmable Prolog Web (An attempt to revive and rebrand Prolog). ~ Torbjörn Lager #Prolog
• Proof theory. ~ Jeremy Avigad #Logic
• AutoBench: Comparing the time performance of Haskell programs. ~ M.A.T. Handley, G. Hutton #Haskell
• IBM Debater: la primera inteligencia artificial que gana un debate a un ser humano. ~ @Alvy #IA
• Una introducción visual al aprendizaje automático y otra a los sesgos que pueden sufrir sus algoritmos. ~ @Alvy #IA #AprendzajeAutomático
• A visual introduction to machine learning. ~ Stephanie Yee , Tony Chu #AI #MachineLearning
• Model tuning and the bias-variance tradeoff. ~ Stephanie Yee , Tony Chu #AI #MachineLearning
• The P vs NP problem. ~ Anthony Bonato #CompSci
• Seven dogmas of category theory. ~ John D. Cook #CategoryTheory
• Why you don’t need data scientists. ~ Kurt Cagle #DataScience
• Un algoritmo que ha aprendido a resolver el Cubo de Rubik «sin asistencia humana». ~ @Alvy #IA #AprendizajeAutomático
• Solving the Rubik’s cube without human knowledge. ~ S. McAleer et als. #AI #MachineLearning
• La programación funcional en Haskell. ~ R. Peña #ProgramaciónFuncional #Haskell
• Schematic polymorphism in the Abella proof assistant. ~ G. Nadathur, Y. Wang #ITP #Abella
• Fixing 17 space leaks in GHCi, and keeping them fixed. ~ Simon Marlow #Haskell
• Computational algebra system in Haskell (Dependently-typed computational algebra system written in Haskell). ~ Hiromi Ishii #Haskell #CAS
• Functional data structures. ~ Prabhakar Ragde #FunctionalProgramming #Algorithms #OCaml
• Libro de exámenes de programación funcional con Haskell (versión del 22 de junio de 2018). #Haskell #I1M2017
• Introduction to deep learning (What is deep learning and how can I study it?). ~ Tyler Bettilyon #AI #DeepLearning
• Deep neural networks as computational graphs (DNNs don’t need to be a black box). ~ Tyler Bettilyon #AI #DeepLearning
• Computer and human languages. ~ Diéssica Gurskas #Programming
• BP: Formal proofs, the fine print and side effects. ~ T- Murray, P.C. van Oorschot #FormalVerification
• Rethinking static reference tables in GHC. ~ Simon Marlow #Haskell
• What’s the difference? (A functional pearl on subtracting bijections). ~ B.A. Yorgey, K. Foner #Haskell
• Queryparser, an open source tool for parsing and analyzing SQL. ~ Matt Halverson #Haskell
• Lógica práctica y aprendizaje computacional. ~ Jacinto Dávila #Lógica #IA #AprendizajeAutomático
• Computational logic and human thinking: How to be artificially intelligent. ~ Robert Kowalski #eBook #IA #Logic
• Pell’s equation in Isabelle/HOL. ~ Manuel Eberl #ITP #IsabelleHOL #Math
• Making the history of computing. The history of computing in the history of technology and the history of mathematics. ~ L. de Mol, M. Bullynck #History #CompSci #Math
• Notes on discrete mathematics. ~ James Aspnes #eBook #Math
• Fast Sudoku solver in Haskell #1: a simple solution. ~ Abhinav Sarkar #Haskell
• Paradigms of Artificial Intelligence programming: case studies in Common Lisp. ~ Peter Norvig #AI #CommonLisp
• Hasktorch: a library for tensors and neural networks in Haskell. #Haskell #AI #MachineLearning
• The automated-reasoning revolution: from theory to practice and back. ~ Moshe Y. Vardi #ATP
• Literate programming with Org-mode. ~ Gregory J Stein #Emacs #OrgMode
• Logic and proof (Release 0.1). ~ Jeremy Avigad, Robert Y. Lewis, and Floris van Doorn #Logic #LeanTheoremProver
• Coercions and roles for dummies. #Haskell
• Why laziness matters. ~ Ben Lynn #Haskell
• Instalación de “Lean theorem prover”. #ITP #LeanProver
• A web page with resources for teaching with formal methods and tools. ~ Jeremy Avigad #ITP #Logic #Math
• Formal methods in mathematics and the Lean theorem prover. ~ Jeremy Avigad #ITP #Logic #Math
• Machine learning for mathematical software. ~ M. England #MachineLearning #MathematicalSoftware
• Fast verifying proofs of propositional unsatisfiability via window shifting. ~ Jingchao Chen #SAT
• Libro de exámenes de programación funcional con Haskell (versión 9.7 del 30 de junio de 2018). #Haskell #I1M2017
• The Emacs Commune. #Emacs #History
• forall x: Calgary Remix (An introduction to formal logic). ~ P.D. Magnus, T. Button, J. Robert Loftis, Aaron Thomas-Bolduc, R. Zach #eBook #Logic
• The Shamir secret sharing algorithm in Haskell. ~ Sina Habibian #Haskell
• Keep your laziness in check. ~ K. Foner et als. #Haskell

Julio 2018

• Computational reverse mathematics and foundational analysis. ~ Benedict Eastaugh #Logic #Math
• GLC: Resumen de lecturas compartidas (octubre de 2017).
• GLC: Resumen de lecturas compartidas (noviembre de 2017).
• GLC: Resumen de lecturas compartidas (diciembre de 2017).
• GLC: Resumen de lecturas compartidas (enero de 2018).
• GLC: Resumen de lecturas compartidas (febrero de 2018).
• IsaK: A complete semantics of K. ~ L. Li, E.L. Gunter #ITP #IsabelleHOL #Logic
• A real-world application with a comonadic user interface. ~ Arthur Xavier #FunctionalProgramming #Haskell #PureScript
• Google Sheets and Haskell. ~ Laurence Emms #Haskell
• Zamansky 50: Presentations. #Emacs
• GLC: Resumen de lecturas compartidas durante marzo de 2018.
• GLC: Resumen de lecturas compartidas durante abril de 2018.
• GLC: Resumen de lecturas compartidas durante mayo de 2018.
• GLC: Resumen de lecturas compartidas durante junio de 2018.
• GLC: Resumen de lecturas compartidas durante el curso 2017-18.
• Compiling an Haskell EDSL to C (A new C back-end for the Copilot runtime verification framework). ~ Frank Dedden Haskell
• Implementing analytic tableaux for justification logic. ~ N. Steenbergen #Haskell #Logic
• judge: Tableau-based theorem prover for justification logic. ~ N. Steenbergen #Haskell #Logic
• Redis data modeling with rank 2 types. #Haskell
• El problema del cambio de moneda. R. Ibáñez #Matemáticas
• A brief history of AI (An outline of what happened in the last 60 years in AI). ~ Francesco Corea #AI
• The machine that builds itself: how the strengths of Lisp family languages facilitate building complex and flexible bioinformatic models. ~ B.B. Khomtchouk, E. Weitz, C. Wahlestedt #Lisp
• Computational reverse mathematics and foundational analysis. ~ B. Eastaugh #Logic #Math
• Toward a more expressive pattern matching in Haskell. ~ G. Servadei #Haskell
• The 11th conference of PhD students in Computer Science (Volume of short papers).
• Scope of Artificial Intelligence in Law. ~ J. Dabass, B.S. Dabass #AI #MachineLearning #DeepLearning
• PVS embeddings of propositional and quantified modal logic. ~ J. Rushby #ITP #PVS #Logic
• Para qué le sirve a un investigador científico estar en Twitter. ~ Francisco R. Villatoro (#Ciencia
• How the scientific community reacts to newly submitted preprints: article downloads, Twitter mentions, and citations. ~ X. Shuai, A. Pepe, J. Bollen #Science
• Papers on programming languages: ideas from 70’s for today. ~ Mikhail Barash #Programming
• Why I love Haskell. ~ @PLT_cheater #Haskell
• A formalisation of nominal α-equivalence with A, C, and AC function symbols. ~ M. Ayala et als. #ITP #Coq
• A purely functional computer algebra system embedded in Haskell. ~ Hiromi Ishii #Haskell #CAS #Math
• Computational algebra system in Haskell (Dependently-typed computational algebra system written in Haskell). ~ Hiromi Ishii #Haskell #CAS #Math
• Benchmarks on various Fibonacci computation. ~ Hiromi Ishii #Haskell #Algorithms #Math
• Simple proof assistant for LK calculus (First-Order logic). ~ Hiromi Ishii #Haskell #Logic
• Probability 5 ways. ~ Donnacha Oisín Kidney #Haskell
• Formalization in constructive type theory of the standardization theorem for the lambda calculus using multiple substitution. ~ M. Copes, N. Szasz, A. Tasistro #ITP #Agda
• Matemática misteriosa. ~ Juan Arias de Reyna #Matemáticas
• Sharing a library between proof assistants: reaching out to the HOL family. ~ F. Thiré #ITP #OpenTheory # Coq #Matita
• Theory exploration in Hipster (or how to automate an undergraduate AI&CS student). ~ Moa Johansson #IsabelleHOL #Haskell
• From algebra to abstract machine. ~ W. Swierstra, C. Tomé Cortiñas #Haskell
• Specifications in small and large contexts. ~ N. Botta [Slides] #Idris
• Kuifje: Quantified information flow with monads in Haskell. ~ Tom Schrijvers #Haskell
• Static analysis of free monads. #Haskell
• Compiling quantamorphisms for the IBM Q-Experience. ~ J.N. Oliveira, A. Neri, R.S. Barbosa #Haskell
• Examples and results from a BSc-level course on domain specific languages of mathematics. ~ P. Jansson et als. #Haskell #Math
• Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. ~ Lawrence C Paulson #ITP #Biography
• Differentiable functional programming. ~ Noel Welsh #DeepLearning #FunctionalProgramming #Scala
• A thought experiment: category theory and quantum computing. ~ Laurence Emms #Haskell #CategoryTheory #QuantumComputing
• Alan Turing, el genio que descodificó la naturaleza. ~ Núria Jar #Turing #Biografía #Computación
• Inside the paper: Build systems à la carte. ~ Neil Mitchell #Haskell
• Deriving instances with a twist. ~ Xia Li-yao #Haskell
• A constructive formalisation of the modular strong normalisation theorem. ~ FLC de Moura et als. #ITP #Coq
• Using SMT engine to generate symbolic automata. ~ X. Qin et als. #SMT
• Von-Neumann-Morgenstern utility theorem in Isabelle/HOL. ~ J. Parsert, C. Kaliszyk #ITP #IsabelleHOL
• Weakening the requirements of a group. ~ J.D. Cook #Math
• A survey of knowledge representation and retrieval for learning in service robotics. ~ D. Paulius, Y. Sun #KRR
• Scaling-up reasoning and advanced analytics on BigData. ~ T. Condie et als. #LogicProgramming #BigData
• Type is an extensible GADT. ~ Xia Li-yao #Haskell
• Otro millón de dólares te espera: ¿Es P = NP? ~ Alfonso J. Población #Matemáticas #Computación
• Towards certified meta-programming with typed template-Coq. ~ A. Anand et als. #ITP #Coq
• Relating idioms, arrows and monads from monoidal adjunctions. ~ E. Rivas #Haskell
• Backward induction for repeated games. ~ J. Hedges #FunctionalProgramming #Haskell
• Everybody’s got to be somewhere. ~ C. McBride #Agda
• Daily coding puzzles. ~ Ali Spittel #CodingPuzzle
• The coinductive formulation of common knowledge. ~ C. Baston, V. Capretta #ITP #Coq #Agda
• La nacionalización de la estrategia en torno a la inteligencia artificial. (Estado, política y futuro). ~ Juan Luis Suárez #IA
• Fast Sudoku solver in Haskell #2: A 200x faster solution. ~ Abhinav Sarkar #Haskell
• Funflow example: emulating make. ~ Divesh Otwani, Nicholas Clarke #Haskell
• Categories for (Big) Data models and optimization. ~ L. Thiry, H. Zhao, M. Hassenforder #BigData #CategoryTheory #FunctionalProgramming #Haskell
• Verified analysis of random binary tree structures. ~ M. Eberl, M.W. Haslbeck, T. Nipkow #ITP #IsabelleHOL
• A formally verified cryptographic extension to a RISC-V processor. ~ J.R. Kiniry et als. #FormalVerification
• Artificial Intelligence. ~ Selmer Bringsjord #AI
• Reification by parametricity (Fast setup for proof by reflection, in two lines of Ltac). ~ J. Gross, A. Erbsen, A. Chlipala #ITP #Coq
• Mtac2: Typed tactics for backward reasoning in Coq. ~ J. Kaiser et als. #ITP #Coq
• A verified automatic prover based on ordered resolution. ~ A. Schlichtkrull, J.C .Blanchette, D. Traytel #ITP #IsabelleHOL #SML #Logic
• A formal proof in Coq of a control function for the inverted pendulum. ~ D. Rouhling #ITP #Coq
• Verifying the LTL to Büchi automata translation via very weak alternating automata. ~ S. Jantsch, M. Norrish #ITP #HOL4
• Eliminating unstable tests in floating-point programs. ~ L. Titolo, C. Muñoz, M.A. Feliú, M.M. Moscato #ITP #PVS
• Reo2PVS: Formal specification and verification of component connectors. ~ M.S. Nawaz, M. Sun #ITP #PVS
• Differential program semantics. ~ T. Girka #ITP #Coq
• Lisp and Haskell. ~ Mark Karpov #Lisp #Haskell
• Type-safe observable sharing in Haskell. ~ Andy Gill #Haskell
• Algorithms have been around for 4,000 years. ~ Herbert Bruderer #Algorithms
• Fast machine words in Isabelle/HOL. ~ A. Lochbihler #ITP #IsabelleHOL
• Compositional soundness proofs of abstract interpreters. ~ S. Keidel, C.B. Poulsen, S. Erdweg #Haskell
• Relational parametricity and quotient preservation for modular (co)datatypes. ~ A. Lochbihler, J. Schneider #ITP #IsabelleHOL
• First steps towards a formalization of Forcing. ~ E. Gunther, M. Pagano, P. Sánchez #ITP #Isabelle #Logic
• AI reasoning systems: PAC and applied methods. ~ J. Cheng #AI #Logic
• Taming the C monster (Haskell FFI techniques). #Haskell
• Competitive proving for fun. ~ M.P.L Haslbeck, S. Wimmer #ITP #IsabelleHOL
• Computational artifacts: Towards a philosophy of computer science. ~ R. Turner #CompSci
• A formally verified solver for homogeneous linear diophantine equations. ~ F. Meßner et als. #ITP #IsabelleHOL
• Probabilistic functional programming. ~ Donnacha Oisín Kidney #FunctionalProgramming #Haskell
• The consistency of arithmetic. ~ T.Y. Chow #Logic
• SAT encodings for sorting networks, single-exception sorting networks and ε−halvers. ~ J.A.R. Fonollosa #Logic #SAT
• SMCDEL: An implementation of symbolic model checking for dynamic epistemic logic with binary decision diagrams. ~ M. Gattinger #Logic #Haskell
• Type theory. ~ Thierry Coquand #Logic
• Formalizing implicative algebras in Coq. ~ É. Miquey #ITP #Coq
• Building an initial Emacs configuration. #Emacs
• Generic deriving of generic traversals. ~ C. Kiss, M. Pickering, N. Wu #FunctionalProgramming #Haskell
• CodeWorld update — July 14, 2018. ~ Chris Smith #Haskell #CodeWorld
• Teaching algebraic expressions with tracking arithmetic. ~ Chris Smith #Teaching #Math #Haskell #CodeWorld
• Mathematics and computation. ~ A. Bonato #Math #CompSci
• Test automáticos con QuickCheck ¿Cómo analizar nuestro código en busca de bugs?. ~ @__josejuan__ #Programación #QuickCheck
• Functor, Applicative and why. ~ Leo Zhang #FunctionalProgramming #Haskell
• The rise of mixed precision arithmetic. ~ Nick Higham #Programming
• The limits of classical and quantum computing. ~ Scott Aaronson #CompSci
• Intuitive mathematics. ~ Marianne Freiberger #Logic #Math
• Paradise lost and rescued. ~ Marianne Freiberger #Logic #Math
• Mathematics and computation. ~ Anthony Bonato #Math #CompSci
• Boosting the reuse of formal specifications. ~ M.M. Moscato et als. #ITP #PVS
• Closing the gap between correctness and efficiency. ~ G. Hutton #FunctionalProgramming #Haskell
• Towards formal modeling and verification of probabilistic connectors in Coq. ~ X. Zhang, M. Sun #ITP #Coq
• Pricing in discrete financial models. ~ M. Echenim #ITP #IsabelleHOL
• Towards a verified Smith normal form algorithm in Isabelle/HOL. ~ J. Divasón, J. Aransay #ITP #IsabelleHOL #Math
• A bridge too far: E.W. Dijkstra and logic. ~ Maarten van Emden #Logic #CompSci
• A practical introduction to finger trees. ~ Chris Penner #Haskell
• A systematic approach for developing cyber physical systems. ~ X. He, Z. Dong, Y. Fu #ITP #Coq
• Dependent typing and existential (de)serialization. #Haskell
• WebGL, Fragment Shader, GHCJS and reflex-dom. ~ Joachim Breitner #Haskell
• Popularity of Haskell extensions. ~ Anish Tondwalkar #Haskell
• Mathematical reasoning. Writing and proof. ~ Ted Sundstrom #eBook #Math
• Supercompilation: ideas and methods. ~ I. Klyuchnikov, D. Krustev #Haskell
• The remote monad. ~ Justin Dawson #PhD_Thesis #Haskell
• A simple semi-automated proof assistant for first-order modal logics. ~ T. Libal #Logic #ATP #Prolog
• Implementations of natural logics. ~ Lawrence S. Moss #Logic #AutomatedReasoning
• Some thoughts about FOL-translations in Vampire. ~ Giles Reger #AutomatedReasoning #Vampir
• Using the Isabelle Ontology Framework (Linking the formal with the informal). ~ A.D. Brucker et als. #ITP #Isabelle
• Formal reasoning about the security of AWS (Amazon Web Services). ~ Byron Cook #AutomatedReasoning
• Into the infinite-theory exploration for coinduction. ~ S.H. Einarsdóttir, M. Johansson, J.Å. Pohjola #IsabelleHOL
• Interdisciplinary programming language design. ~ Michael Coblenz et als. #Programming
• Constructive Galois connections. ~ D. Darais, D. van Horn #ITP #Agda #Math
• Learning heuristics for automated reasoning through deep reinforcement learning. ~ G. Lederman et als. #MachineLearnig #AutomatedReasoning
• Towards neural theorem proving at scale. ~ P. Minervini et als. #AutomatedReasoning #MachineLearning
• Teaching programming languages. ~ Michael Hicks #Programming #Teaching
• Reference comparing R, Python, and MATLAB syntax. #Python #Rstats #MatLAB
• Using apt-get commands in Linux (complete beginners guide). ~ A. Prakash #Linux
• CoqTL: an internal DSL for model transformation in Coq. ~ M. Tisi, Z. Cheng #ITP #Coq
• Regular language representations in the constructive type theory of Coq. ~ C. Doczkal, G. Smolka #ITP #Coq
• Quadratic reciprocity and (p^2-1)/8. ~ The Xena Project #ITP #Lean #Math
• Automating verification of state machines with reactive designs and Isabelle/UTP. ~ S. Foster et als. #ITP #IsabelleHOL
• DAOconCoq: Demostración Asistida por Ordenador con Coq. #DAO #Coq
• DAOconCoq: Programación funcional y métodos elementales de demostración en Coq. #DAO #Coq
• Patience in K-8 Computer Science. ~ Chris Smith #Teaching #Programming #CodeWorld
• Formally verified Montgomery multiplication. ~ C. Walther #ITP #VeriFun #Math
• Teoría de categorías y programación funcional. ~ Diego Pedraza #Haskell #Matemáticas
• Why purely functional programming is a great idea with a misleading name. ~ Tikhon Jelvis #FunctionalProgramming
• Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. ~ M. Echenim, H. Guiol, N. Peltier #ITP #IsabelleHOL
• Declarative GUIs: simple, consistent, and verified. ~ S. Adelsberger, A. Setzer, E. Walkingshaw #Agda
• Bindings are functors. ~ J.C. Blanchette, L. Gheri, A. Popescu, D. Traytel #ITP #IsabelleHOL
• Novices and motivation when learning to code. ~ Chris Smith #Teaching #CodeWorld
• Gamifying propositional logic: QED, an interactive textbook. ~ Terence Tao #Teaching #Logic
• QED: a short interactive text in propositional logic arranged in the format of a computer game. ~ Terence Tao #Teaching #Logic
• Une histoire de la logique mathématique (de la philosophie à l’informatique). ~ Christian Retoré #Logic
• Course: Data structures and functional programming. ~ Michael Clarkson #FunctionalProgramming #OCaml #ITP #Coq
• Formal reasoning in Coq: a beginner’s guide. ~ Ray Wang #ITP #Coq
• Coq cheatsheet. ~ Eddie Kohler #ITP #Coq
• Python the future of programming? ~ Mike James #Programming #Python
• GHCinception: Running GHCi in GHCi. ~ Michael Sloan #Haskell
• Un error informático envía información confidencial a 1.500 criminales. #Programación
• List of software bugs. ~ Wikipedia #Programming
• Company-coq: A collection of extensions for Proof General’s Coq mode. #Emacs #Coq
• Bridging the gap between programming languages and hardware weak memory models. ~ A. Podkopaev, O. Lahav, V. Vafeiadis #ITP #Coq
• Haskell for JavaScript developers. ~ Anthony N Cipriano #Haskell #JavaScript
• HAMTs (Hash Array Mapped Tries) from scratch. ~ Vaibhav Sagar #Haskell
• Constructivism: An expert’s view. ~ Harvey Friedman #Logic #Math
• Computational logic: artificial intelligence in mathematical reasoning. ~ S. Graham-Lengrand and R. Blanco #Course #Logic #FunctionalProgramming #OCaml #ITP #Coq
• Verifying programs and proofs (Part I. describe algorithms). ~ Yves Bertot #ITP #Coq
• Coq Winter School 2018. ~ Yves Bertot #Course #ITP #Coq
• “The art of computer programming” by Donald Knuth. ~ Carl Tashian #Programming
• DAOconCoq T2: Demostraciones por inducción sobre los números naturales en Coq. #ITP #Coq
• Beyond polynomials and Peano arithmetic: automation of elementary and ordinal interpretations. ~ H. Zankl, S. Winkler, A. Middeldorp #Logic #Math #ATP
• Copying vs. sharing in functional languages. ~ Dan Ghica #FunctionalProgramming
• Verified AVL trees in Haskell and Agda. ~ Donnacha Oisín Kidney #Haskell #Agda
• Haskell: If monads are the solution, what is the problem? ~ Dan Ghica #FunctionalProgramming #Haskell
• Free Monoid from Free Algebra, Part 1: Free Algebras. ~ Bartosz Milewski #Haskell #CategoryTheory
• Free Monoid from Free Algebra, Part 2: Free Monoids. ~ Bartosz Milewski #Haskell #CategoryTheory
• Grain: a strongly-typed functional programming language built for the modern web. #FunctionalProgramming
• Learning Elm in 2018: comprehensive list of resources. #FunctionalProgramming #Elm

Agosto 2018

• Formalization of the arithmetization of Euclidean plane geometry and applications. ~ P. Boutry, G. Braun, J. Narboux #ITP #Coq #Math
• Formal probabilistic analysis of dynamic fault trees in HOL4. ~ Y. Elderhalli, W. Ahmad, O. Hasan, S. Tahar #ITP #HOL4
• Learning statistics with R (A tutorial for psychology students and other beginners). ~ Danielle Navarro #Statistics #Rstats
• Art vs. science in mathematical discovery. ~ J. Polak #Math
• Making Haskell as fast as C: Imperative programming in Haskell. ~ Henri Verroken #Haskell
• Learn functional Python in 10 minutes. ~ Brandon Skerritt #FunctionalProgramming #Python
• Aggregates tables in Org mode. ~ Thierry Banel #Emacs #OrgMode
• Who needs category theory? ~ A. Blass, Y. Gurevich #CategoryTheory
• Tricks in Coq: Some tips, tricks, and features in Coq that are hard to discover. ~ Tej Chajed #ITP #Coq
• An Answer Set Programming environment for high-level specification and visualization of FCA. ~ L. Bourneuf #ASP #FCA
• Make your code easier to read with Functional Programming. ~ Cristi Salcescu #FunctionalProgramming #JavaScript
• Two years of functional programming in JavaScript: lessons learned. ~ Victor Nakoryakov #FunctionalProgramming #JavaScript
• The science behind functional programming. ~ Rafa Paradela #FunctionalProgramming #CategoryTheory
• Pros and cons of functional programming. ~ Iren Korkishko #FunctionalProgramming
• An introduction to functional programming in JavaScript. ~ Matt Banz #FunctionalProgramming #JavaScript
• A Coq mechanised formal semantics for realistic SQL queries * Formally reconciling SQL and bag relational algebra ~ V. Benzaken, É. Contejean #ITP #Coq
• An introduction to artificial intelligence and law. ~ K. Ashley, T. Gordon. #AI
• Top 10 roles in AI and data science. ~ Cassie Kozyrkov #AI #DataScience
• Summarized Slack from Deepspec Summer School 2017. #DSSS17 #ITP #Coq
• Purely functional games. ~ Gil Mizrahi #FunctionalProgramming #Haskell #Game
• Purely functional games (How I built a game in Haskell - pure functional style). Gil Mizrahi [Slides] #FunctionalProgramming #Haskell #Game
• GHC, one compiler to RULE them all. ~ Alexandre Moine #Haskell
• Introduction to the rank-select bit-string. ~ John Ky #FunctionalProgramming #Haskell
• QuickSpec and the quest for good lemmas. ~ Daniel Selsam #Haskell
• Parametric polymorphism and operational improvement. ~ J. Hackett, G. Hutton. #FunctionalProgramming #Haskell
• The simple essence of automatic differentiation. ~ Conal Elliott #FunctionalProgramming #CategoryTheory #Haskell
• Teaching how to program using automated assessment and functional glossy games (experience report). ~ J. Bacelar Almeida et als. #Teaching #FunctionalProgramming #Haskell
• DAOconCoq T3: Datos estructurados en Coq. #ITP #Coq
• Demostración Asistida por Ordenador (3 primeros capítulos). #DAOconCoq #ITP #Coq
• Compositional soundness proofs of abstract interpreters. ~ S. Keidel, C. Bach Poulsen, S. Erdweg. #Haskell
• Elaborating dependent (co)pattern matching. ~ J. Cockx, A. Abel. #Agda
• Capturing the future by replaying the past (functional pearl). ~ J. Koppel, G. Scherer, A. Solar-Lezama. #FunctionalProgramming #SML
• MoSeL: a general, extensible modal framework for interactive proofs in separation logic. ~ R. Krebbers et als. #ITP #Coq
• What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl). ~ G. Boisseau, J. Gibbons. #FunctionalProgramming #Haskell #CategoryTheory
• Relational algebra by way of adjunctions. ~ J. Gibbons et als. #FunctionalProgramming #Haskell #CategoryTheory
• Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). ~ J. Breitner et als. #Haskell #Coq
• A type and scope safe universe of syntaxes with binding: their semantics and proofs. ~ G. Allais et als. #Agda
• DAOconCoq T4: Polimorfismo y funciones de orden superior en Coq. #ITP #Coq
• Demostración Asistida por Ordenador (4 primeros capítulos). #DAOconCoq #ITP #Coq
• Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam. ~ A. Stampoulis, A. Chlipala. #Metaprogramming #Prolog
• Equivalences for free: univalent parametricity for effective transport. ~ N. Tabareau, É. Tanter, M. Sozeau. #Coq #HoTT
• Fault tolerant functional reactive programming (functional pearl). ~ I. Perez #FunctionalProgramming #Haskell #Idris
• Partially-static data as free extension of algebras. ~ J. Yallo et als. #FunctionalProgramming #Haskell
• Boolean constraints in SWI-Prolog: A comprehensive system description. ~ Markus Triska #Prolog #CLP
• Lecture notes on Iris: Higher-order concurrent separation logic. ~ L. Birkedal, A. Bizjak #ITP #Coq #Logic
• A guide to GHC’s extensions. ~ Jannis Limperg #Haskell
• Libro de exámenes de programación funcional con Haskell (versión del 4 de agosto de 2018). #Haskell #I1M2017
• Mathematical olympiad in China (problems and solutions). #Math
• The history and concept of mathematical proof. ~ S. G. Krantz. #Math
• Mathematical proof. ~ Wikipedia #Math
• Suggesting valid hole fits for typed-holes (Experience report). ~ Matthías Páll Gissurarson #Haskell
• hgeometry: A simple geometry library in Haskell. ~ Frank Staals #Haskell #Math
• Composing iterator-returning functions. ~ Manuel Vázquez Acosta #Python #Haskell
• Lidl software disaster another example of Germany’s digital failure. ~ F. Kolf, C. Kerkmann #Sofware #Bug
• OpenStax: openly licensed textbooks. #eBooks
• Computing integer sequences: Filtering vs generation (Functional pearl). ~ I. Salvo, A. Pacifico #FunctionalProgramming #Haskell
• Coherent explicit dictionary application for Haskell: Formalisation and coherence proof. ~ T. Winant, D. Devriese #Haskell
• Demostración asistida por ordenador con Isabelle/HOL. #DAO #IsabelleHOL
• An invitation to functional programming (for mathematicians). ~ Sonat Süer #FunctionalProgramming #Haskell
• Haskell ain’t maths. ~ Dan Ghica #Haskell #Maths
• Monoid homomorphisms (Part 1 of 2). ~ Sonat Süer #CategoryTheory #Haskell
• Categorifying cardinal arithmetic. ~ Emily Riehl #Math #CategoryTheory
• Desperately seeking integers (A few twists on Turing’s proof of undecidability of predicate calculus). ~ R.J. Lipton, K.W. Regan #Logic #Math
• Category theory in PL research. ~ N. Krishnaswami #CategoryTheory #CompSci
• Habits of highly mathematical people. ~ Jeremy Kun #Math
• A short guide to hard problems. ~ Kevin Hartnett #Math #CompSci
• Discover “Unpaywall,” a new (and legal) browser extension that lets you read millions of science articles normally locked up behind paywalls.
• Haskell with only one type family. ~ Xia Li-yao #Haskell
• Keeping it clean: Haskell code formatters. ~ James Bowen #Haskell
• Topological models of arithmetic. ~ A. Enayat, J.D. Hamkins, B. Wcisło #Logic #Math
• Semantics of Mizar as an Isabelle object logic. ~ C. Kaliszyk, K. Pąk #ITP IsabelleHOL #Mizar #Logic
• From algebra to abstract machine: a verified generic construction. ~ C.T. Cortiñas, W. Swierstra #FunctionalProgramming #ITP #Agda
• “Concrete semantics” with Coq and CoqHammer. ~ Ł. Czajka, B. Ekici, C. Kaliszyk #ITP #Coq #IsabelleHOL
• Coq version of (part of) the HOL-IMP theories accompanying the book “Concrete Semantics with Isabelle/HOL”. Formalized using CoqHammer. #ITP #Coq
• Enif-Lang: A specialized language for programming network functions on commodity hardware. ~ N. Bonelli, S. Giordano, G. Procissi #Haskell
• Data-parallel rank-select bit-string construction. ~ John Ky #Haskell
• Monoid homomorphisms (Part 2 of 2). ~ Sonat Süer #CategoryTheory #Haskell
• Learning Haskell: Miscellaneous enlightenments. ~ Sandeep C R #Haskell
• Template Haskell tutorial. ~ Mark Karpov #Haskell
• 100 best websites for mathletes. #Math
• Lambda calculus - step by step. ~ Helmut Brandl #LambdaCalculus #Logic #Math
• An outsider’s guide to statically typed functional programming. ~ Brian Marick #FunctionalProgramming #Elm #PureScript
• DAOconCoq T5: Tácticas básicas de Coq. #ITP #Coq
• Demostración Asistida por Ordenador con Coq (5 primeros capítulos). #DAOconCoq #ITP #Coq
• Currying in calculus, PDEs, programming, and categories. ~ J.D. Cook #Math #FunctionalProgramming #Haskell #CategoryTheory
• Breaking the space-time barrier with Haskell: Time-traveling and debugging in CodeWorld. ~ Krystal Maughan #Haskell #CodeWorld
• Improving typeclass relations by being open. ~ G. Martínez, M. Jaskelioff, G. De Luca #Haskell
• Type-safe data versioning in Haskell. ~ Lorenzo Tabacchini #Haskell
• State of Haskell 2018. ~ Aaron Contorer #Haskell
• Paradox at the heart of mathematics makes physics problem unanswerable. ~ Davide Castelvecch #Logic #Math #Physics
• Fast Sudoku solver in Haskell #3: Picking the right data structures. ~ Abhinav Sarkar #Haskell
• A formal proof of the expressiveness of deep learning. ~ A. Bentkamp, J.C. Blanchette, D. Klakow. #ITP #IsabelleHOL #DeepLearning
• Extensible type-directed editing. ~ J. Korkut, D.T. Christiansen #FunctionalProgramming #Idris
• Approximating compiling to categories using type-level Haskell: Take 2. ~ Philip Zucker #FunctionalProgramming #Haskell
• A formally verified proof of the Mason-Stothers theorem in Lean. ~ J. Wagemaker #ITP #Lean #Math
• Ghosts of departed proofs (Functional pearl). ~ Matt Noonan #Haskell
• Type theory as a framework for modelling and programming. ~ C. Ionescu, P. Jansson, N. Botta. #FunctionalProgramming
• Proof theory. ~ Michael Rathjen #Logic
• Mathematical surprises. ~ Dave Richeson #Math
• A verified SAT solver framework with learn, forget, restart, and incrementality. ~ J.C. Blanchette et als. #ITP #IsabelleHOL #SAT
• Newbie’s guide to Deep Learning (Taking baby steps when starting DL). ~ Arkar Min Aung #DeepLearning
• Minsky machines in Isabelle/HOL. ~ Bertram Felgenhauer #ITP #IsabelleHOL
• Some fundamental theorems in Mathematics. ~ Oliver Knill #Math
• Divide and conquer algorithms. ~ Brandon Skerritt #Algorithms
• Typeclass induction and developing a QuickCheck-like library. ~ Marcelo Zabani #FunctionalProgramming #Haskell
• Folds on lists. ~ Jeremy Gibbons #FunctionalProgramming #Haskell
• Cube composer: A puzzle game inspired by functional programming. ~ David Peter #FunctionalProgramming #PureScript #Game
• Proof simplification and automated theorem proving. ~ Michael Kinyon #ATP #Prover9
• The Boyer-Moore waterfall model revisited. ~ P. Papapanagiotou, J. Fleuriot #ITP #HOL_Light
• A very small SAT solver. ~ Maximilian Algehed #FunctionalProgramming #Haskell #Logic #SAT
• From informal to formal proofs in euclidean geometry. ~ S Stojanovic-Ður #ATP #TPTP #Math
• Pearls of Scala functional programming, Part I (1. Smallest free number: array-based solution). ~ Baseer Al-Obaidy #FunctionalProgramming #Scala
• Functional programming in Python (Creating transformation pipelines in Python). ~ Dennis Vriend #FunctionalProgramming #Python
• Introducing computer science to high school students through logic programming. ~ T.T. Yuen, M. Reyes, Y. Zhang. #LogicProgramming #ASP #Teaching
• Using Erlang in research and education in a technical university. ~ I. Petrov, A. Alexeyenko, G. Ivanova. #FunctionalProgramming #Erlang #Teaching
• Lenses for philosophers. ~ Jules Hedges #CategoryTheory
• Categorical data analysis. ~ John D. Cook #CategoryTheory
• How to turn a Dromedary camel into a Bactrian camel. ~ Alexander Klink #FunctionalProgramming #Haskell
• Exercises and notes from the Coursera Machine Learning Course by Andrew Ng. ~ Michael Chavinda #FunctionalProgramming #Haskell #MachineLearning
• ZuriHac 2018: Haskell hackathon in Rapperswil. ~ Ivan Krišto. #FunctionalProgramming #Haskell
• Solving the mystery behind Abstract Algorithm’s magical optimizations. ~ Victor Maia #Haskell
• Abusing the continuation monad. ~ Jules Hedges #FunctionalProgramming #Haskell
• Programs and proofs in the Coq proof assistant. ~ Arthur Azevedo de Amorim and Robert Rand. #ITP #Coq
• QED version 2.0: an interactive text in first-order logic. ~ Terence Tao #Teaching #Logic
• Demystifying functional programming (in a real company). ~ Caio Oliveira #FunctionalProgramming
• Why referential transparency matters? ~ Stéphane Derosiaux #FunctionalProgramming
• Eliminating unstable tests in floating-point programs. ~ L. Titolo, C.A. Muñoz, M.A. Feliú, and M.M. Moscato. #FormalVerification #PVS
• DAOconCoq T6: Lógica en Coq. #DAO #Coq #Lógica
• Demostración Asistida por Ordenador con Coq (6 primeros capítulos). #DAOconCoq #DAO #Coq #ProgramaciónFuncional #Lógica
• SBVPlugin: Formally prove properties of Haskell programs using SBV/SMT. ~ Levent Erkök #Haskell
• A Haskell compiler. ~ David Tereil #Haskell
• Recursion schemes for higher algebras. ~ Bartosz Milewski #FunctionalProgramming #Haskell #CategoryTheory
• Sobre la ética de los asistentes inteligentes. ~ @Alvy #IA
• Towards an ethics of AI assistants: An initial framework. ~ John Danaher #AI
• From fast exponentiation to square matrices: An adventure in types. ~ Chris Okasaki #FunctionalProgramming #Haskell
• What programming language should a professional mathematician know? #Math #Programming #CompSci
• Esta red neuronal aplica leyes físicas aprendidas de forma automática. #IA #Física
• Discovering physical concepts with neural networks. ~ R. Iten et als. #MachineLearning #Physics
• How to get into Machine Learning for a Haskeller. ~ Dennis Gosnell #Haskell #MachineLearning
• Water jug rewrite with Haskell (Part I). ~ Vignesh Sarma K #Haskell
• A verified simple prover for first-order logic. ~ J. Villadsen, A. Schlichtkrull, A.H. From. #ITP #IsabelleHOL
• Formalisation of a frame stack semantics for a Java-like language. ~ A Schubert, J. Chrząszcz. #ITP #Coq
• The conception, evolution, and application of functional programming languages. ~ Paul Hudak #FunctionalProgramming
• LiquidHaskell: Experience with refinement types in the real world. ~ N. Vazou, E.L. Seidel, R. Jhala #Haskell #LiquidHaskell
• Functional programming for mortals with Scalaz. ~ Sam Halliday #FunctionalProgramming #Scala #Scalaz
• Source and examples to “Functional Programming for Mortals with Scalaz”. ~ Sam Halliday #FunctionalProgramming #Scala #Scalaz
• CoSMed: A confidentiality-verified social media platform. ~ T. Bauereiß et als. #ITP #IsabelleHOL
• Review of: “CoSMed: a confidentiality-verified social media platform”. ~ Simon Thompson #ITP #IsabelleHOL
• Mathematics and programming - the easy languages to learn. ~ A. Egri-Nagy #Math #CompSci
• A new algebraic approach to decision making in a railway interlocking system based on preprocess. A. Hernando, R. Maestre, E. Roanes-Lozano. #Math #CompSci
• Matemáticos y acusmáticos. ~ Lucio Fernando Ruíz #Matemáticas
• The proof: Monad as a monoid in category of endofunctors. ~ Wojtek Pituła #FunctionalProgramming #Scala
• The abstract calculus. ~ Victor Maia #FunctionalProgramming #Haskell
• You should learn functional programming in 2018. ~ Allan MacGregor #FunctionalProgramming
• Using circular programs for higher-order syntax (Functional pearl). ~ E. Axelsson, K. Claessen. #FunctionalProgramming #Haskell
• Writing fast Haskell (Elegance is not an excuse for bad performance). ~ Moritz Kiefer #FunctionalProgramming #Haskell
• Marrying Haskell and Hyper-Threading. ~ Alexander Vershilov #FunctionalProgramming #Haskell
• How functional programming can be awesome: Tail recursion elimination. ~ Luciano Strika #FunctionalProgramming #Python #Haskell
• Bit-manipulation operations for high-performance succinct data-structures and CSV parsing. ~ John Ky #FunctionalProgramming #Haskell
• Exploring folds: A powerful pattern of functional programming. ~ Zaid Ajaj #FunctionalProgramming
• The great power of Newtypes. ~ Hiromi Ishii #FunctionalProgramming #Haskell
• Some lectures on programming languages. ~ Kathleen Fisher #Programming
• Turing goes to Church (What can a computer do?). ~ Steve Poling #CompSci #FunctionalProgramming
• Not-o-matic differentiation. ~ Andrew Knapp #FunctionalProgramming #Haskell
• Examples and results from a BSc-level course on domain specific languages of mathematics ~ P. Jansson et als. #Haskell #Math
• FMS: Functional programming as a modelling language. ~ I. Dasseville, G. Janssens. #ASP
• R para Ciencia de Datos. ~ G. Grolemund, H. Wickham #Rstats #DataScience
• History of Lisp. ~ John McCarthy #Lisp
• Hedwig: a fast, type safe, declarative PureScript library for building web applications. ~ Utkarsh Kukretig#examples #PureScript
• Purely functional solutions to imperative problems (HaskellRank Ep.07). #FunctionalProgramming #Haskell
• Typed transitions, finite state machines and free categories. ~ Marcin Szamotulski #FunctionalProgramming #Haskell
• Towards Mac Lane’s comparison theorem for the (co)Kleisli construction in Coq. ~ Burak Ekici. #ITP #Coq
• Logic as a path to enlightenment (Work in progress report). ~ Wolfgang Schreiner #Logic #CompSci
• Automatic proof-checking of ordinary mathematical texts. ~ S. Frerix, P. Koepke. #ATP #ITP #Math
• IsarMathLib: a formalized mathematics library for Isabelle/ZF. ~ S. Kołodyński. #ITP #IsabelleZF #Math
• Simple high-level code for cryptographic arithmetic (with proofs, without compromises). ~ A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala. #ITP #Coq
• CAP (Categories, Algorithms, and Programming) project. ~ S. Gutsche, S. Posur, M. Barakat, Ø. Skartsæterhagen. #CAS #CategoryTheory
• On the syntax and semantics of CAP (Categories, Algorithms, Programming) project. ~ S. Gutsche, S. Posur, Ø. Skartsæterhagen. #CAS #CategoryTheory
• Automation for proof engineering (Machine-checked proofs at scale). ~ D. Matichuk. #ITP #IsabelleHOL #PhD_Thesis
• Progress in the formalization of Matiyasevich’s theorem in the Mizar system. ~ K. Pąk #ITP #Mizar #Math
• Univalent foundations as a foundation for mathematical practice. ~ H. Crane. #Logic #Math
• A nonlinear guide to Haskell. ~ Daniel Firth #FunctionalProgramming #Haskell
• A road to Common Lisp. ~ Steve Losh #FunctionalProgramming #CommonLisp
• Fun with macros: Gathering. ~ Steve Losh #FunctionalProgramming #CommonLisp
• Fun with macros: If-let and when-let. ~ Steve Losh #FunctionalProgramming #CommonLisp
• The calculus of constructions. ~ T. Coquand, G. Huet #Logic #Math
• An incremental simplex algorithm with unsatisfiable core generation in Isabelle/HOL. ~ Filip Marić #ITP #IsabelleHOL
• Learning proof search in proof assistants. ~ Michael Färber #AutomatedTheoremProving #MachineLearning
• A computational sketch of homology. ~ Thomas Sutton #FunctionalProgramming #Haskell #Math
• A simple methodology for computing families of algorithms. ~ D.N. Parikh et als. #Programming #CompSci
• Formalisation of cryptographic proofs in Agda. ~ A.M. Golov. #ITP #Agda
• CoqHammer: Automation for dependent type theory. ~ Ł. Czajka, C. Kaliszyk. #ITP #ATP #Coq
• CoqHammer: An automated reasoning hammer tool for Coq. ~ Łukasz Czajka #ITP #ATP #Coq
• Backprop as functor: A compositional perspective on supervised learning. ~ B. Fong, D.I. Spivak, R. Tuyéras. #Haskell #MachineLearning
• Unique solutions of contractions, CCS, and their HOL formalisation. ~ C. Tian, D. Sangiorgi. #ITP #HOL4
• Verified tail-recursive folds through dissection. ~ C. Tomé Cortiñas. #FunctionalProgramming #ITP #Agda
• Laws! ~ George Wilson #FunctionalProgramming #Haskell
• Is your research software correct? ~ Mike Croucher #Programming
• Software foundations Volume 4: QuickChick: Property-based testing in Coq. ~ L. Lampropoulos, B.C. Pierce. #ITP #Coq
• Owl: A general-purpose numerical library in OCaml. ~ L. Wang. #FunctionalProgramming #OCaml
• Comparison of two theorem provers: Isabelle/HOL and Coq. ~ A. Yushkovskiy, S. Tripakis. #ITP #IsabelleHOL #Coq
• Appetite for dysfunction. ~ Andrew McMiddlin #FunctionalProgramming #Haskell #WordPress
• Awesome emacs config files. #Emacs
• What is Data Science? ~ Lance Fortnow #DataScience
• Foundations of Data Science Boot Camp. #DataScience
• The role of the Mizar Mathematical Library for interactive proof development in Mizar. ~ G. Bancerek et als. #ITP #Mizar #Math
• Proving program correctness using the AG semantics: An example with n-queens. ~ A. Harrison-18. #LogicProgramming #ASP
• SMT-based constraint answer set solver EZSMT+ for non-tight programs. ~ D. Shen, Y. Lierler #LogicProgramming #ConstraintProgramming #ASP #SMT
• Is Julia the next big programming language? MIT thinks so, as version 1.0 lands. #Programming #Julia
• From neural networks to the Category of composable supervised learning algorithms in Scala. ~ P. Voitot #NeuralNetworks #CategoryTheory #Scala

Septiembre 2018

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

Octubre 2018

• From algebra to abstract machine: a verified generic construction. ~ C. Tomé Cortiñas, W. Swierstra. #FunctionalProgramming #ITP #Agda
• Refinement kinds (A theory of type-safe meta-programming). ~ L. Caires, B. Toninho. #FunctionalProgramming #Haskell
• Typing the wild in Erlang. ~ N. Valliappan, J. Hughes. #FunctionalProgramming #Erlang
• An introduction to probabilistic programming. ~ J.W. van de Meent, B. Paige, H. Yang, F. Wood. #FunctionalProgramming #Lisp #Clojure #FOPPL
• RMSbolt: A supercharged implementation of the godbolt compiler-explorer for Emacs. ~ Jay Kamat. #Programming #Emacs
• Resumen de lecturas compartidas durante septiembre de 2018.
• The transcendence of π in Isabelle/HOL. ~ M. Eberl. #ITP #isabelleHOL #Math
• Proving in the Isabelle proof assistant that the set of real numbers is not countable. ~ J. Villadsen. #ITP #isabelleHOL #Math
• Students’ Proof Assistant (SPA). ~ A. Schlichtkrull, J. Villadsen, A.H. From. #ITP #IsabelleHOL #Logic
• Introduction to Singletons (Part 3). ~ Justin Le. #Haskell
• Introducing Haskell to a company. ~ Brian Jones. #FunctionalProgramming #Haskell
• Formalization of logic in the Isabelle proof assistant. ~ A. Schlichtkrull. #PhD_Thesis #ITP #IsabelleHOL #Logic
• Representation matters: An unexpected property of polynomial rings and its consequences for formalizing abstract field theory. ~ C. Schwarzweller. #ITP #Mizar #Math
• AI benchmark: Running deep neural networks on Android smartphones. ~ A. Ignatov et als. #AI #DeepLearning
• Automatic diagnosis and correction of logical errors for functional programming assignments. ~ J. Lee et als. #FunctionalProgramming #OCaml
• Random testing for language design. ~ L. Lampropoulos. #PhD_Thesis #ITP #Coq #QuickChick
• Productive Haskell in enterprise. ~ Brian Jones. #FunctionalProgramming #Haskell
• Rewrite rules and a specific fold: use optimization techniques from GHC.Base. ~ Alexandre Moine. #FunctionalProgramming #Haskell
• Haskell study plan (an opinionated list of resources for learning Haskell). ~ Gil Mizrahi. #FunctionalProgramming #Haskell
• An application of ASP theories of intentions to understanding restaurant scenarios: insights and narrative corpus. ~ Q. Zhang, C. Benton, D. Inclezan. #LogicProgramming #ASP
• anthem: Transforming gringo programs into first-order theories (preliminary report). ~ V. Lifschitz, P. Lühne, T. Schaub. #LogicProgramming #ASP #ATP
• A review of the Lean theorem prover. ~ Thomas Hales. #ITP #LeanTheoremProver
• Formalizing 100 theorems in Coq. #ITP #Coq #Math
• capability: the ReaderT pattern without boilerplate. ~ A. Herrmann, A. Spiwack. #FunctionalProgramming #Haskell
• A gently curated list of companies using Haskell in industry. ~ Erik Mossberg #FunctionalProgramming #Haskell
• Ten things you should know about Haskell syntax. ~ Bartosz Milewski #FunctionalProgramming #Haskell
• 4 reasons why Python isn’t the programming language for you. ~ Ian Buckley #Programming #Python
• What is the Xena Project? ~ Kevin Buzzard #ITP #LeanTheoremProver #Math
• Counting inversions with monoidal sparks. ~ Brent Yorgey #FunctionalProgramming #Haskell #Math
• Keep your types small … and your bugs smaller. ~ Matt Parsons. #FunctionalProgramming #Haskell
• Monads for functional programming in Scala. ~ Daniel Berg #FunctionalProgramming #Scala
• A new algebraic approach to decision making in a railway interlocking system based on preprocess. ~ A. Hernando, R. Maestre, E. Roanes-Lozano. #Math #CompSci
• Companion webpage to the book “Mathematics for Machine Learning”. ~ Marc Peter Deisenroth, A Aldo Faisal, and Cheng Soon Ong. #eBook #MachineLearning #Math
• Detailed walkthrough for a beginner Haskell program. ~ G. Gonzalez. #FunctionalProgramming #Haskell
• Comprehending Monoids with Class. ~ Lionel Parreaux #FunctionalProgramming #Haskell
• Deeper Stack knowledge. ~ James Bowen. #FunctionalProgramming #Haskell
• Learn Haskell in one video. ~ Derek Banas. #FunctionalProgramming #Haskell
• Division of polynomials in Haskell. ~ Philip Zucker. #FunctionalProgramming #Haskell #Math
• Wikistat 2.0: Educational resources for Artificial Intelligence. ~ P. Besse, B. Guillouet, B. Laurent #AI
• Wikistat 2.0: Tutoriels (calepins jupyter) d’auto-apprentissage en Science des Données & Intelligence artificielle. #DataScience #AI
• Fractals and the Weierstrass-Mandelbrot function. ~ A. Zaleski #Math
• Formal verification of helicopter automatic landing control algorithm in theorem prover Coq. ~ X. Chen, G. Chen. #ITP #Coq
• Suggesting valid hole fits for typed-holes in Haskell. ~ Matthías Páll Gissurarson. #Msc_Thesis #FunctionalProgramming #Haskell
• Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant. ~ J.A. Bergstra, A. Ponse, D.J.C. Staudt. #Logic #ATP #Prover9
• Making a Haskell interface for the Rosie Pattern Language. ~ Laurence Emms. #FunctionalProgramming #Haskell
• The fundamental theorem of algebra in ACL2. ~ R. Gamboa, J. Cowles. #ITP #ACL2 #Math
• Using ACL2 in the design of efficient, verifiable data structures for high-assurance systems. ~ D. Hardin, K. Slind. #ITP #ACL2
• An introduction to linear regression using Haskell. ~ Sam Gardner. #FunctionalProgramming #Haskell
• Why are functional programming languages so popular in the programming languages community? #FunctionalProgramming
• The art of Prolog, second edition (Advanced programming techniques). ~ L.S. Sterling, E.Y. Shapiro. #Open #eBook #LogicProgramming #Prolog
• Real vector spaces and the Cauchy-Schwarz inequality in ACL2(r). ~ C. Kwan, M.R. Greenstreet. #ITP #ACL2 #Math
• IsaK: a complete semantics of K. ~ L. Li, E.L. Gunter. #ITP #IsabelleHOL
• Hask Anything!: a website aimed at collecting and organizing the collective knowledge of the Haskell community. #FunctionalProgramming #Haskell
• Functional programming. #FunctionalProgramming #Haskell
• The US military wants to teach AI some basic common sense. ~ Will Knight. #AI
• An implementation of Homotopy Type Theory in Isabelle/Pure. ~ J. Chen. #Msc_Thesis #ITP #Isabelle #HoTT
• Isabelle/HoTT: An experimental implementation of HoTT in the interactive proof assistant Isabelle. J. Chen. #ITP #Isabelle #HoTT
• A tutorial introduction to CryptHOL. ~ A. Lochbihler, S.R. Sefidgar. #ITP #IsabelleHOL #CryptHOL
• Formalising filesystems in the ACL2 theorem prover: an Application to FAT32. ~ Mihir Parang Mehta. #ITP #ACL2
• Practical Haskell programs from scratch (a quick and easy guide). #FunctionalProgramming #Haskell
• Headfirst into Haskell. ~ Abby Sassel. #FunctionalProgramming #Haskell
• Towards verified, constant-time floating point operations. ~ M. Andrysco et als. #FunctionalProgramming #Haskell #SMT
• Dependent types in Haskell: Binomial heaps 101 (Who put binary numbers in my type system?). ~ Jasper Van der Jeugt. #FunctionalProgramming #Haskell
• Incremental SAT library integration in ACL2 using abstract stobjs. ~ Sol Swords. #ITP #ACL2 #SAT
• #HIW18: Let’s go mainstream with Eta!. ~ Rahul Muttineni. #FunctionalProgramming #Haskell #Eta
• CoreSpec: Verifying GHC with hs-to-coq. ~ Antal Spector-Zabusky et als. #FunctionalProgramming #Haskell #ITP #Coq
• Coercion quantification. ~ N. Xie, R.A. Eisenberg. #FunctionalProgramming #Haskell
• Aelve Guide: Wiki for the Haskell ecosystem. #Haskell
• Enlaces y recursos sobre redes neuronales y deep learning. ~ @ajlopez #AI #NeuralNetworks #DeepLearning
• Convex functions in ACL2(r). ~ C. Kwan, M.R. Greenstreet. #ITP #ACL2 #Math
• ESCRIPT: a human readable language for programming Bitcoin scripts. ~ Rick Klomp. #FunctionalProgramming #Haskell
• SCRIPT Analyser: Symbolic verification of Bitcoin’s output scripts. ~ Rick Klomp. #FunctionalProgramming #Haskell
• Fixpoints in Haskell. ~ Chris Smith. #FunctionalProgramming #Haskell
• A JavaScript WAT and monoidal folds. ~ Julie Moronuki and Chris Martin. #JavaScript #Haskell #FunctionalProgramming
• Orgstat: a statistics visualizer tool for org-mode. ~ Mikhail Volkhov. #Haskell #Emacs #OrgMode
• A Haskell Enigma machine simulator with rich display and machine state details. #FunctionalProgramming #Haskell
• Haskell in industry. #FunctionalProgramming #Haskell
• Learn programming. ~ A. Salonen. #eBook #Programming #OpenLibra
• Learning to reason (Theorem proving at first order via reinforcement learning). ~ Brian Groenke. #Logic #ATP #MachineLearning
• How Lisp became God’s own programming language. ~ Sinclair Target. #Programming #Lisp
• DefunT: A tool for automating termination proofs by using the community books. ~ Matt Kaufmann. #ITP #ACL2
• Cedille-Core: A minimal (600 LOC) programming language capable of proving theorems about its own terms. #ITP #Logic #FunctionalProgramming #Haskell
• Formality: An efficient programming language and proof assistant. #ITP #Cedille
• DBFunctor: Functional data management (type safe ETL/ELT in Haskell). ~ Nikos Karagiannidis. #FunctionalProgramming #Haskell
• Problem solving vs proving. ~ Anthony Bonato #Math
• Upper bounding diameters of state spaces of factored transition systems in Isabelle/HOL. F. Kurz and M. Abdulaziz. #ITP #IsabelleHOL
• Granule: a statically typed functional language with graded modal types for fine-grained program reasoning via types. ~ Dominic Orchard #FunctionalProgramming #Haskell
• Programming language foundations in Agda. ~ P. Wadler. #ITP #Agda #Coq
• Programming language foundations in Agda. ~ P. Wadler, W. Kokke. #eBook #ITP #Agda #Coq
• Temporal properties of smart contracts. ~ I. Sergey, A. Kumar, A. Hobor. #ITP #Coq
• Logics and symbolic Artificial Intelligence. ~ Isabelle Bloch, Natalia Díaz Rodríguez. #AI #Logic
• Randomised binary search trees in Isabelle/HOL. ~ M. Eberl #ITP #IsabelleHOL
• Haskell’s kind system (a primer). ~ D. Castro. #Haskell
• An applicative password list. ~ M. Seemann. #FunctionalProgramming #Haskell
• Sigma, Pi, Sum, Product. ~ Samuel Breese. #FunctionalProgramming #Haskell
• AI today and tomorrow is mostly about curve fitting, not intelligence. ~ Kurt Marko. #AI #DeepLearning
• Máquinas listas, pero sin sentido común. ~ Ramon López de Mántaras. #IA
• Building machines that learn and thinlike people. ~ B.M. Lake, T.D. Ullman, J.B. Tenenbaum, S.J. Gershman. #AI
• Algorithmes: à la recherche de l’universalité perdue. ~ Rachid Guerraoui #CompSci
• Proofs and side effects (Understanding the promise and the fine print of formal methods for security). ~ Toby Murray. #ITP
• BP: Formal proofs, the fine print and side effects. ~ T. Murray, P.C. van Oorscho. #ITP
• Running from the past. ~ Dan Piponi. #FunctionalProgramming #Haskell
• Mark Dominus: I struggle to understand Traversable. #FunctionalProgramming #Haskell
• The Haskell Cookbook. #FunctionalProgramming #Haskell
• Browsing the Web with Common Lisp. #Lisp #CommonLisp #Web #NextBrowser
• Next: a keyboard-oriented, extensible web-browser inspired by Emacs and designed for power users. #Lisp #CommonLisp #Web #NextBrowser
• Formalizing computability theory via partial recursive functions. ~ M. Carneiro. #ITP #Lean
• A denotational semantics for an imperative language. ~ G. Malecha. #ITP #Coq
• Formalization of the embedding path order for lambda-free higher-order terms. ~ A. Bentkamp. #ITP #IsabelleHOL
• REST-ish services in Haskell (Part 1). ~ @vadosware #FunctionalProgramming #Haskell
• Some computer algebra algorithms in Haskell. ~ J. Pellejero. #FunctionalProgramming #Haskell #Math
• An invitation to category theory. ~ Tai-Danae Bradley. #CategoryTheory
• Layer systems for confluence — formalized. ~ B. Felgenhauer, F. Rapp #ITP #IsabelleHOL
• The prime number theorem in Isabelle/HOL. ~ M. Eberl, L. Paulson. #ITP #IsabelleHOL #Math
• Elm: Functional frontend! ~ James Bowen. #FunctionalProgramming #Elm
• Introduction to Singletons (Part 4). ~ Justin Le. #Haskell #FunctionalProgramming
• Evolution of Emacs Lisp. ~ S. Monnier, M. Sperber. #Emacs #Lisp
• Principles of algorithmic problem solving. ~ J. Sannemo. #eBook #Algorithms #Programming #CompSci
• Deriving proved equality tests in Coq-elpi (Stronger induction principles for containers in Coq). ~ E. Tassi. #ITP #Coq
• In computers we trust? (As math grows ever more complex, will computers reign?) #Math #CompSci #ITP
• Alchemy: A Language and Compiler for Homomorphic Encryption Made easY. ~ E. Crockett, C. Peikert, C. Sharp. #Haskell #FunctionalProgramming
• Typed functional programming and software correctness. ~ Marko Dimjašević. #FunctionalProgramming
• Algebraic Data Types in four languages (A comparison). ~ #Haskell #Scala #Rust #TypeScript
• Third wave AI: The coming revolution in Artificial Intelligence. ~ Scott Jones. #AI
• A DARPA perspective on Artificial Intelligence. ~ John Launchbury. #AI
• Can we trust AI if we don’t know how it works? ~ Marianne Lehnis. #AI
• Assuring AI. ~ John Launchbury. #AI
• CodeWorld guide. ~ Chris Smith. #Haskell #CodeWorld #FunctionalProgramming
• Solving russian calendar problems in Haskell (HaskellRank Ep.08). ~ Alexey Kutepov. #FunctionalProgramming #Haskell
• Los cuadrados y la factorización. ~ Juan Arias de Reyna. #Matematicas #Computacion
• A tale of two sieves. ~ C. Pomerance. #Math #CompSci
• AI, explain yourself. ~ Don Monroe. #AI #XAI
• US Department of Defense commits $2B to training AI to have “common sense”. #AI
• AI talent pipeline clogged by education programs slow or unable to change. #AI
• Para qué sirven las matemáticas. ~ Francisco R. Villatoro #Matemáticas
• The unplanned impact of mathematics. ~ P. Rowlett. #Math
• Build your own monads. ~ A. Serrano. #FunctionalProgramming #Haskell
• Wise man’s Haskell (Free book for learning Haskell). ~ Andre Popovitch. #eBook #FunctionalProgramming #Haskell
• Headfirst into Haskell. ~ Abby Sassel. #FunctionalProgramming #Haskell
• Testing in the World of Functional Programming. ~ Luka Jacobowitz. #FunctionalProgramming #Scala
• Statistics and data science degrees: Overhyped or the real deal? ~ P. Richard Hahn #DataScience
• A functional paradigm using the C language for teaching Programming for Engineers. ~ V. Theoktisto. #Teaching #Programming #FunctionalProgramming
• Legal representation and reasoning in practice: a critical comparison. ~ S. Batsakis et als. #KRR #ASP #Logic #AI
• The periodic table of data structures. ~ S. Idreos et als. #Algorithmic
• The internals of the data calculator. ~ S. Idreos et als. #Algorithmic
• Epistemic logic in Isabelle/HOL. ~ Andreas Halkjær From. #ITP #IsabelleHOL #Logic
• Creating a card game in Haskell (part 4). ~ Valentin Robert #FunctionalProgramming #Haskell
• Fourier, Cantor, las series trigonométricas y la teoría de conjuntos. ~ Pedro J. Paúl #Matemáticas
• Typed functional programming and software correctness. ~ Marko Dimjašević. #FunctionalProgramming #Haskell #Agda
• Introduction to state machine testing: part 1. ~ Andrew McMiddlin #FunctionalProgramming #Haskell
• Pragmatic development in Eta. ~ Nick Tchayka. #FunctionalProgramming #Haskell #Eta
• Course CIS 252: Introduction to Computer Science. ~ Susan Older #FunctionalProgramming #Haskell
• A trustworthy mechanized formalization of R. ~ M. Bodin, T. Diaz, É. Tanter. #ITP #Coq #RStat
• Attack trees in Isabelle. ~ F. Kammüller. #ITP #IsabelleHOL
• A generic Coq proof of typical worst-case analysis. ~ P. Fradet, M. Lesourd, J.F. Monin, S. Quinton. #ITP #Coq
• A simple implementation of affine spaces and vector spaces in Haskell. #FunctionalProgramming #Haskell #Math
• The laws of natural deduction in inference by DNA computer. ~ Ł. Rogowski, P. Sosík. #Logic #DNAcomputing

Noviembre 2018

• Resumen de lecturas compartidas durante octubre de 2018. #FunctionalProgramming #Haskell #ITP #IsabelleHOL #Coq #Agda
• Formalisation and evaluation of Alan Gewirth’s proof for the principle of generic consistency in Isabelle/HOL. ~ D. Fuenmayo. #ITP #IsabelleHOL #Logic
• I/O logic in HOL. ~ A. Farjami, P. Meder, X. Parent, C. Benzmüller. #ITP #IsabelleHOL
• Åqvist’s dyadic deontic logic E in HOL. ~ C. Benzmüller, A. Farjami, X. Parent. #ITP #IsabelleHOL #Logic
• Formal proofs of Tarjan’s algorithm in Why3, Coq, and Isabelle. ~ R. Chen, C. Cohen, J.J. Levy, S. Merz, L. Thery. #ITP #Why3 #Coq #IsabelleHOL
• Automated theorem proving in intuitionistic propositional logic by deep reinforcement learning. ~ M. Kusumoto, K. Yahata, M. Sakai. #ATP #DeepLearning
• Haskell by example: The birthday bar. ~ Jan van Brügge #FunctionalProgramming #Haskell
• Haskell: journey from 144 min to 17 min. ~ Denis. #FunctionalProgramming #Haskell
• History of “Structured programming”. ~ Maarten van Emden. #Programming
• Hasktorch: a library for tensors and neural networks in Haskell. ~ Sam Stites. #FunctionalProgramming #Haskell #DeepLearning
• Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL. ~ J.C. Blanchette. #ITP #IsabelleHOL #Logic
• Mechanizing focused linear logic in Coq. ~ B. Xavier, C. Olarte, G. Reis, V. Nigam. #ITP #Coq #Logic
• Formalization of universal algebra in Agda. ~ E. Gunther, A. Gadea, M. Pagano. #ITP #Agda
• Type theory as a framework for modelling and programming. ~ C. Ionescu, P. Jansson, N. Botta. #FunctionalProgramming #TypeTheory
• Proving for Fun: proving competitions and learning material for Interactive Proof Assistants such as Isabelle. #ITP #IsabelleHOL
• Moving towards dialogue. ~ Vaibhav Sagar. #FunctionalProgramming #Haskell #Idris
• Elm III: adding effects. ~ James Bowen. #FunctionalProgramming #Elm
• Graphics programming in Elm develops Math knowledge & social cohesion. ~ J. Zhang et als. #Teaching #Math #FunctionalProgramming #Elm
• A Lisp way to type theory and formal proofs. ~ Frédéric Peschanski. #ITP #LaTTe #Clojure #FunctionalProgramming
• LaTTe: a Laboratory for Type Theory experiments (in Clojure). ~ Frederic Peschanski. #ITP #LaTTe #Clojure #FunctionalProgramming
• Proceedings of the 11 th European Lisp Symposium (April 16-17, 2018). #Lisp #FunctionalProgramming
• Carnap: a new free open-source multi-purpose multi-system logic software. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming
• Carnap: A formal logic framework that runs in the browser. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming
• Carnap.io: A formal logic framework for Haskell. ~ Graham Leach-Krouse. #Logic #Haskell #FunctionalProgramming
• Haskell by example: Utopian tree. ~ Jan van Brügge. #Haskell #FunctionalProgramming
• R and Haskell, meant for each other?. ~ Richard Careaga. #Rstats #Haskell
• HaskellR: Programming R in Haskell. #Rstats #Haskell
• Why is functional programming gaining traction? Why now? ~ Eric Normand. #FunctionalProgramming
• SAT-based explicit LTLf satisfiability checking. ~ J. Li, K.Y. Rozier, G. Pu, Y. Zhang, M.Y. Vardi. #Logic #SAT #ATP
• Hakyll Pt. 1: Setup & initial customization. ~ Robert Pearce. #Haskell #Hakyll #FunctionalProgramming
• Haskell at FINN.no. ~ Sjur Millidahl. #Haskell #FunctionalProgramming
• Signal processing in Haskell. ~ Rinat Stryungis. #Haskell #FunctionalProgramming
• Waargonaut the JSONer. ~ Sean Chalmers. #Haskell #FunctionalProgramming
• So, you want to write a DSL interpreter … H-Calc!. #Haskell #DSL #FunctionalProgramming
• On the naturalness of proofs. ~ V.J. Hellendoorn, P.T. Devanbu, M.A. Alipour. #ITP #HOL_Light #Coq
• Tarski on truth: a thumbnail sketch. ~ Peter Smith. #Logic
• Exploring a shipping puzzle. ~ Kevin Lynagh. #Clojure #Alloy #FunctionalProgramming
• Exceptionally monadic error handling (Looking at bind and squinting really hard). ~ J. Malakhovski. #Haskell #FunctionalProgramming
• A formal proof of Hensel’s lemma over the p-adic integers. ~ R.Y. Lewis. #ITP #Lean #Math
• A very simple prime sieve in Haskell. ~ Donnacha Oisín Kidney #Haskell #FunctionalProgramming
• Existential quantification. ~ Mark Karpov. #Haskell #FunctionalProgramming
• Typeclasses: Show. ~ Daniel J. Harvey #Haskell
• Problemas y algoritmos. ~ Luis Vargas. #Libro #Algoritmos #Programacion #Cpp
• Algoritmos. ~ Pier Paolo Guillen Hernandez. #Algoritmos
• Informática para las Matemáticas, Matemáticas para la Informática, Informática aplicada. ~ J. Aransay et als. #Matematicas #Informatica
• À la recherche du logiciel parfait. ~ Xavier Leroy. #ITP
• Teaching Functional Programming: two big picture approaches. ~ Ed Toro. #FunctionalProgramming
• Elm IV: navigation! ~ James Bowen. #FunctionalProgramming #Elm
• SMCDEL: A symbolic model checker for Dynamic Epistemic Logic. ~ Malvin Gattinger. #Logic #Haskell #FunctionalProgramming
• SMCDEL: an implementation of symbolic model checking for Dynamic Epistemic Logic with Binary Decision Diagrams. ~ Malvin Gattinger. #Logic #Haskell #FunctionalProgramming
• Course: Functional programming for logicians. ~ Malvin Gattinger and Jana Wagemaker. #Logic #Haskell #FunctionalProgramming
• Davis, Putnam, Logemann, Loveland (DPLL) theorem proving in Haskell. ~ Jan van Eijck. #Logic #Haskell #FunctionalProgramming #ATP
• Why IO input types are confusing. ~ Malvin Gattinger. #Haskell #FunctionalProgramming
• UCLID5: Integrating modeling, verification, synthesis, and learning. ~ S.A. Seshia, P. Subramanyam. #FormalVerification #ITP
• Simple proofs of great theorems. #Math
• Simple proofs: The irrationality of pi. #Math
• Simple proofs: The fundamental theorem of algebra. #Math
• Simple proofs: The impossibility of trisection. #Math
• Introduction to state machine testing: part 2. ~ Andrew McMiddlin #Haskell #FunctionalProgramming
• A touch of topological quantum computation in Haskell pt. I. ~ Philip Zucker. #Haskell #FunctionalProgramming
• A SAT+CAS approach to finding good matrices: new examples and counterexamples. ~ C. Bright et als. #SAT #CAS
• Programs as the language of science. ~ G. Pantelis. #CompSci
• Libro de exámenes de programación funcional con Haskell (versión del 14 de noviembre de 2018). #ProgramacionFuncional #Haskell #I1M2018
• An abstract stack based approach to verified compositional compilation to machine code. ~ P. Wilke, Y. Wang, Z. Shao. #ITP #Coq
• Simple high-level code for cryptographic arithmetic (with proofs, without compromises). ~ A. Erbsen, J. Philipoom, J. Gross, R. Sloan, A. Chlipala. #ITP #Coq
• Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). ~ J. Breitner, A. Spector-Zabusky, Y. Li, C. Rizkallah, J. Wiegley, S. Weirich. #ITP #Coq #Haskell
• Termonad: A terminal emulator configurable in Haskell. ~ Dennis Gosnell. #Haskell #FunctionalProgramming
• Great works in programming languages. ~ Benjamin C. Pierce. #CompSci
• Ex-Hack: a Haskell example-based documentation. ~ @ninjatrappeur #Haskell
• GTK+ programming with Haskell. ~ Oskar Wickström. #Haskell
• Typed-holes and valid hole fits. ~ Matthías Páll Gissurarson. #Haskell #FunctionalProgramming
• Suggesting valid hole fits for typed-holes (experience report). ~ Matthías Páll Gissurarson. #Haskell #FunctionalProgramming
• Haskell Weekly 133: News from the Haskell community (November 15 2018). #Haskell
• Isabelle/MMT: export of Isabelle theories and import as OMDoc content. ~ Makarius Wenzel. #ITP #IsabelleHOL #MMT
• Proof-carrying plans. ~ C. Schwaab et als. #ITP #Agda IA #Planning
• On synthetic undecidability in Coq, with an application to the Entscheidungsproblem. ~ Y. Forster, D. Kirst, G. Smolka. #ITP #Coq #Logic
• Breadth-first extraction: lessons from a small exercice in algorithm certification. ~ D. Larchey-Wendling, R. Matthes. #ITP #Coq #Algorithms
• Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines. ~ Y. Forster, D. Larchey-Wendling. #ITP #Coq #Logic
• Practical Web Development with Haskell (Master the essential skills to build fast and scalable Web applications). ~ Ecky Putrady. #Haskell
• Hakyll Pt. 2: Generating a sitemap XML file. ~ Robert Pearce. #Haskell #Hakyll #FunctionalProgramming
• The emergence of first-order logic. ~ William Ewald. #Logic
• Formal verification of control systems properties with theorem proving. ~ D. Araiza-Illan, K. Eder, A. Richards. #ITP
• 2018 state of Haskell survey results. ~ Taylor Fausak. #Haskell
• Pros and cons of functional programming. ~ Iren Korkishko. #FunctionalProgramming
• The tensor product, demystified. ~ Tai-Danae Bradley. #Math
• Matroids in Isabelle/HOL. ~ Jonas Keinholz. #ITP #IsabelleHOL #Math
• Human-competitive patches in automatic program repair with Repairnator. ~ M. Monperrus et als. #Programming
• Creative Maths Challenge. #Math
• Curry-Howard-Lambek correspondence. ~ John D. Cook. #CompSci
• Keeping formal verification in bounds. ~ Donnacha Oisín Kidney. #Haskell #Agda
• Analysis and solution of a collection of algorithmic problems. ~ R.E. López. #Algorithms #Programming #Cpp
• Deriving generic class instances for datatypes in Isabelle/HOL. ~ Jonas Rädle, Lars Hupel. #ITP #IsabelleHOL
• What is elementary geometry? ~ Alfred Tarski #Math #Logic #History
• Programming with Math. ~ Bartosz Milewski. #Logic #Math #Programming #Haskell
• High-performance mathematical paradigms in Python. ~ Harshit Tyagi #Python #Math
• Formalised set theory: well-orderings and the axiom of choice. ~ Dominik Kirst. #ITP #Coq #Math
• Axiomaticl set theory in type theory. ~ Gert Smolka. #ITP #Coq #Math
• Writing a Thesis with Org Mode. #Emacs #OrgMode
• Writing a PhD thesis with Org Mode. ~ Daniel Gómez. #Emacs #OrgMode
• An Emacs Library for frictionless Blogging. ~ Daniel Gómez. #Emacs #OrgMode
• Producto de Euler y ceros. ~ Juan Arias de Reyna. #Matemáticas
• Course: Introduction to computational logic. ~ Gert Smolka. #ITP #Coq #Logic
• Function totality: Abstraction tool in programming. ~ Marko Dimjašević. #Haskell #FunctionalProgramming
• State monad comes to help sequential pattern matching. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
• Holophrasm: a neural automated theorem prover for higher-order logic. ~ D. Whalen. #ITP #NeuralNetworks
• Why functional programming matters. ~ J. Hughes. #FunctionalProgramming
• pLam: command line interpreter for learning and exploring pure λ-calculus. ~ Sandro Lovnički. #Haskell #LambdaCalculus
• New site for Google’s coding competitions. ~ Sue Gee. #CompetitiveProgramming
• An introduction to QuickCheck by example: Number theory and Okasaki’s red-black trees. ~ Matt Might. #Haskell #QuickCheck #FunctionalProgramming
• Category theory for programmers. (Scala edition). ~ B. Milewski, I. Tabachnik. #CategoryTheory #Haskell #Scala #FunctionalProgramming
• Haskell for Scala developers. ~ Claire Neveu. #Haskell #Scala #FunctionalProgramming
• Exploring languages with interpreters and functional programming. ~ H. Conrad Cunningham. #CompSci #Programming #FunctionalProgramming #Haskell
• (Emacs+Org-Mode) Choosing the best writing and publishing software. #Emacs #OrgMode
• Functional programming principles in Javascript. ~ @leandrotk_ #FunctionalProgramming #JavaScript
• Surgery for data types. ~ Xia Li-yao. #Haskell #FunctionalProgramming
• Directory of links on logic and foundations of mathematics. ~ Sylvain Poirier. #Logic #Math
• Getting started with Purescript! ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
• Is Rust functional? ~ M. Snoyman. #Rust #FunctionalProgramming
• Haskell and Rust. ~ Chris Allen. #Haskell #Rust #FunctionalProgramming
• Computer programming as an art. ~ Donald Knuth. #Programming #CompSci
• Counting polynomial roots in Isabelle/HOL: A formal proof of the Budan-Fourier theorem. ~ W.Li, L.C. Paulson. #ITP #IsabelleHOL #Math
• Graph saturation in Isabelle/HOL. ~ S.J.C. Joosten. #ITP #IsabelleHOL
• From C to interaction trees: Specifying, verifying, and testing a networked server. ~ N. Koh et als. #ITP #Coq
• Experience report on formally verifying parts of OpenJDK’s API with KeY. ~ A. Knüppel, T. Thüm, C. Pardylla, I. Schaefer. #ATP #KeY
• Lightweight interactive proving inside an automatic program verifier. ~ S. Dailler, C. Marché, Y. Moy. #ITP #ATP
• Gentle introduction to dependent types with Idris. ~ Boro Sitnikovski. #Idris #FunctionalProgramming #ITP
• Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. ~ M. Wenzel. #ITP #IsabelleHOL
• Some beautiful arguments using mathematical induction. ~ E.W. Dijkstra. #Math #CompSci
• Towards live programming environments for statically verified JavaScript. ~ C. Schuster. #PhD_Thesis #ITP #LeanProver #JavaScript
• Formalism and proofs for esverify. ~ C. Schuster. #IPT #LeanProver #JavaScript
• esverify: Program verification for ECMAScript/JavaScript. ~ C. Schuster. #IPT #LeanProver #JavaScript
• Traf: A proof tree viewer that works with Coq through Proof General. ~ Hideyuki Kawabata. #ITP #Coq
• Synquid: synthesizes programs from refinement types. ~ Nadia Polikarpova. #Haskell #FunctionalProgramming
• Automated synthesis of functional programs with auxiliary functions. ~ S. Eguchi, N. Kobayashi, T. Tsukada. #Haskell #FunctionalProgramming
• Auto2 prover. ~ B. Zhan. #ITP #IsabelleHOL
• A verified functional implementation of Bachmair and Ganzinger’s ordered resolution prover. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel. #ITP #IsabelleHOL
• Simplicity: High-assurance smart contracting. ~ R. Oconnor, A. Poelstra. #Haskell #Coq #ITP #FunctionalProgramming #Blockchain
• Simplicity: a blockchain programming language designed as an alternative to Bitcoin script. ~ R. Oconnor. #Haskell #Coq #ITP #FunctionalProgramming #Blockchain
• Type-driven program synthesis. ~ N. Polikarpova #Haskell #FunctionalProgramming

Diciembre 2018

• |{Math, Philosophy, Programming, Writing}| = 1. ~ Attila Egri-Nagy. #Math #Philosophy #Programming
• Certifying the true error: Machine learning in Coq with verified generalization guarantees. ~ A. Bagnall, G. Stewart. #ITP #Cop #MachineLearnig
• Verification of Casper in the Coq proof assistant. ~ K. Palmskog et als. #ITP #Coq #Blockchain
• Sharing a library between proof assistants: reaching out to the HOL family. ~ F. Thiré. #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS
• Interoperability between arithmetic proofs using Dedukti. ~ F. Thiré #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS
• Logipedia: an arithmetic library that is shared between several proof systems. ~ F. Thiré. #ITP #Dedukti #Coq #Matita #OpenTheory #LeanProver #PVS
• Three Euler’s sieves and a fast prime generator (Functional pearl). ~ I. Salvo, A. Pacifico. #Haskell #FunctionalProgramming #Math
• QuickCheck (a lightweight tool for random testing of Haskell programs). ~ K. Claessen, J. Hughes. #Haskell #QuickCheck
• Tools and techniques for the verification of modular stateful code. ~ M.J. Parreira. #ITP #Why3
• Programming language foundations in Agda. ~ Philip Wadler. #ITP #Agda
• Histoire des mathématiques dans l’humanité. ~ Cedric Villani. #Math
• Programming language foundations in Agda. ~ Philip Wadler, Wen Kokke. #ITP #Agda
• Adventures in formalisation: Financial contracts, modules, and two-level type theory. ~ Danil Annenkov. #PhD_Thesis #ITP #Coq #Agda #Lean
• Introduction to Haskell. ~ Ray Toal #Haskell #FunctionalProgramming
• Course: Programming languages. ~ Ray Toal #Programming
• guanxi: An exploration of relational programming in Haskell. ~ Edward Kmett #Haskell #FunctionalProgramming
• An integrative framework for artificial intelligence education. ~ P. Langley. #Teaching #AI
• Programming with Lenses in Haskell and OCaml. #Haskell #OCaml #FunctionalProgramming
• Laziness Quiz. ~ Matt Parsons. #Haskell #FunctionalProgramming
• Pycategories: Python library implementing ideas from category theory. ~ Daniel Hones. #Python #Haskell #CategoryTheory
• Alchemical groups: Advent of code with free groups and group homomorphisms. ~ Justin Le. #Haskell #FunctionalProgramming
• Fixin’ your automata. ~ François Pottier. #OCaml #FunctionalProgramming
• Dependently typed lambda calculus in Haskell. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming
• Why Clojure? I’ll tell you why … ~ Ertuğrul Çetin. #Clojure #FunctionalProgramming
• A behind the scenes look at Map, Filter, and Reduce in Swift. ~ Boudhayan Biswas. #Swift #FunctionalProgramming
• Functional programming principles in Javascript. ~ @leandrotk_ #FunctionalProgramming #JavaScript
• Verified analysis of random binary tree structures. ~ M. Eberl, M.W. Haslbeck, T. Nipkow. #ITP #IsabelleHOL
• Automated theorem proving in a chat environment. ~ R. Zhumagambetov, M. Sterling. #ITP #Coq
• Automating the diagram method to prove correctness of program transformations. ~ D. Sabel. #Haskell #FunctionalProgramming
• A simple functional presentation and an inductive correctness proof of the Horn algorithm. ~ A. Ravara. #Logic #SAT
• Implementing a proof assistant using focusing and logic programming. ~ T. Libal. #ITP #LogicProgramming #Prolog
• Shaving with Occam’s razor: deriving minimalist theorem provers for minimal logic. ~ P. Tarau. #Logic #ATP #Prolog #LogicProgramming
• Rating of geometric automated theorem provers. ~ N. Baeta, P. Quaresma. #ATP #Geometry
• Introduction to state machine testing: part 3. ~ Andrew McMiddlin. #Haskell #FunctionalProgramming
• Lens by example: Writing traversals. ~ Chris Penner. #Haskell #FunctionalProgramming
• Haskell to Perl 6: nutshell (Learning Perl 6 from Haskell, in a nutshell). #Haskell #Perl
• Certified ACKBO. ~ A. Lochmann, C. Sternagel. #ITP #IsabelleHOL
• Towards intuitive reasoning in axiomatic geometry. ~ M. Doré, K. Broda. #ITP #ELFE #Haskell #Math
• Binding to a C++ CORBA interface in Haskell. ~ Michael Oswald. #Haskell #Cpp
• Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL. ~ J.C. Blanchette. #ITP #IsabelleHOL #Logic #ATP
• IsaFoL: Isabelle Formalization of Logic. #ITP #IsabelleHOL #Logic
• Competitive proving for fun. ~ M.P.L. Haslbeck, S. Wimmer. #ITP #IsabelleHOL
• Towards an encyclopaedia of proof systems. #Logic
• A verified compiler for a linear imperative/functional intermediate language. ~ S. Schneider. #PhD_Thesis #ITP #Coq
• Techniques behind SMT solvers. ~ T. Ehrencron. #SMT #LiquidHaskell #ATP
• <a href=”https://interestingengineering.com/15-of-the-most-important-algorithms-that-helped-define-mathematics-computing-and-physics “>15 of the most important algorithms that helped define Mathematics, Computing, and Physics. ~ C. McFadden. #Algorithms #Math #CompSci #Physics
• 2018 in review: 10 AI failures. #AI
• Formalization of metatheory of the Quipper quantum programming language in a linear logic. ~ M.Y. Mahmoud, A.P. Felty. #ITP #Coq
• Intuitionistic dual tableaux in HOL. ~ Jeremy E. Dawson. #ITP #HOL #Logic
• United monoids. ~ A. Mokhov. #Haskell #FunctionalProgramming #Math
• Shifting the stars: Advent of code with galilean optimization. ~ Justin Le. #Haskell #FunctionalProgramming
• DIY benchmark history with Criterion and Shiny. ~ Théophane Hufschmitt. #Haskell #FunctionalProgramming
• Why not both? (Build Haskell projects with either cabal or stack). ~ Sam Halliday. #Haskell
• A webcam server in 35 lines of Haskell. #Haskell
• Computational mathematics with SageMath. ~ Paul Zimmermann et als. #eBook #SageMath
• A verified implementation of algebraic numbers in Isabelle/HOL. ~ S.J.C. Joosten, R. Thiemann, A. Yamada. #ITP #IsabelleHOL #Haskell #Math
• Applications of foundational proof certificates in theorem proving. ~ M. Roberto. #PhD_Thesis #FPC #ATP
• Tools and techniques for the verification of modular stateful code. ~ M.J. Pereira. #PhD_Thesis #ITP #Why3
• Will machine learning replace mathematicians? ~ Chris Budd. #Math #AI #ITP
• Thinking with types: Type-level programming in Haskell. ~ Sandy Maguire. #Haskell #FunctionalProgramming
• Formalizing probability concepts in a type theory. ~ F. Kachapova. #ITP #Coq #Math
• Can one design a geometry engine? On the (un)decidability of affine Euclidean geometries. ~ J.A. Makowsky. #Logic #Math #ATP
• A verified Timsort C implementation in Isabelle/HOL. ~ Y. Zhang, Y. Zhao, D. Sanan. #ITP #IsabelleHOL #Algorithms
• In praise of sequence (co-)algebra and its implementation in Haskell. ~ K. Clenaghan. #Haskell #FunctionalProgramming #Math
• The Yoda of Silicon Valley. ~ S. Roberts. #CompSci
• Why dependent Haskell is the future of software development. ~ V. Zavialov. #Haskell #FunctionalProgramming
• A Coq mechanised formal semantics for realistic SQL queries (Formally reconciling SQL and bag relational algebra). ~ V. Benzaken, É. Contejean. #ITP #Coq
• Formalizing the semantics of concurrent revisions. ~ R. Overbeek. #Msc_Thesis #ITP #IsabelleHOL
• Properties of orderings and lattices. ~ G. Struth. #ITP #IsabelleHOL #Math
• Constructive cryptography in HOL. ~ A. Lochbihler, S.R. Sefidgar. #ITP #IsabelleHOL
• Constructive and non-constructive proofs in Agda (Part 1): Logical background. ~ Danya Rogozin #ITP #Agda #Logic
• Constructive and non-constructive proofs in Agda (Part 2): Agda in a nutshell. ~ Danya Rogozin. #ITP #Agda #Logic
• Constructive and non-constructive proofs in Agda (Part 3): Playing with negation. ~ Danya Rogozin #ITP #Agda #Logic
• Prime sieves in Agda. ~ Donnacha Oisín Kidney. #ITP #Agda
• Signal processing in Haskell. ~ Rinat Stryungis. #Haskell #FunctionalProgramming
• Pure & lazy breadth-first traversals of graphs in Haskell. ~ Donnacha Oisín Kidney. #Haskell #FunctionalProgramming
• Purescript II: Typeclasses and Monads. ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
• Purescript III: Making a Web Page with Purescript and React! ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
• Purescript IV: Routing and navigation! ~ James Bowen. #Purescript #Haskell #FunctionalProgramming
• Proof pearl: A mechanized proof of GHC’s mergesort. ~ C. Sternagel. #ITP #IsabelleHOL #Haskell #Algorithms
• Classical logic in Haskell. ~ Vladimir Ciobanu. #Haskell #FunctionalProgramming #Logic
• Formally verified quantum programming. ~ R. Rand. #PhD_Thesis #ITP #Coq
• Balancing scans. ~ Donnacha Oisín Kidney. #Haskell #Agda
• Open season on hylomorphisms. ~ B. Milewski. #Haskell #FunctionalProgramming
• Metaprob: A language for probabilistic programming and metaprogramming, embedded in Clojure. #Clojure #FunctionalProgramming
• Clojure & functional programming. ~ @leandrotk_ #Clojure #FunctionalProgramming
• El yin-yang y el número áureo. ~ M.A. Morales. #Matemáticas
• Higher kinded parametricity. ~ Brian McKenna. #Haskell #FunctionalProgramming
• Verified solving and asymptotics of linear recurrences. ~ M. Eberl. #ITP #IsabelleHOL #Math #Algorithmic
• Verifying a security hypervisor model by infinite symbolic execution and invariant strengthening. ~ V. Rusu, G. Grimaud, M. Hauspie. #ITP #Coq
• Décomposer et itérer pour résoudre un problème. ~ G. Legendre, J. Salomon. #Algorithms #Math
• Solving planning problems with Fast Downward and Haskell. ~ @acid2 #Haskell #FunctionalProgramming
• Graphs are to categories as lists are to monoids. ~ Musa Al-hassy. #CategoryTheory #Agda #Haskell
• A listing of common theorems in elementary category theory. ~ Musa Al-hassy. #CategoryTheory #Agda
• Reference sheet for the Coq language. ~ Musa Al-hassy. #ITP #Coq
• Literate Agda with Org-mode. ~ Musa Al-hassy. #ITP #Agda #Emacs #OrgMode
• A verified efficient implementation of the LLL basis reduction algorithm. ~ R. Bottesch, M.W. Haslbeck, R. Thiemann. #ITP #IsabelleHOL
• Compiling to categories 3: A bit cuter. ~ Philip Zucker. #Haskell #FunctionalProgramming
• Essential logic for computer science. ~ R. Page, R. Gamboa. #Logic #ITP #ACL2
• The essence of Datalog. #Haskell #FunctionalProgramming #LogicProgramming
• Functional programming and mathematical objects. ~ J. Karczmarczuk. #Haskell #FunctionalProgramming #Math
• Proving Cantor’s theorem in Clojure using LaTTe. ~ Andrea Amantini. #ITP #LaTTe #Clojure
• How to learn Math and Physics. ~ John Carlos Baez. #Math #Physics
• Gröbner bases and Macaulay matrices in Isabelle/HOL. ~ A. Maletzky. #ITP #IsabelleHOL #Math
• A generic and executable formalization of signature-based Gröbner basis algorithms. A. Maletzky. #ITP #IsabelleHOL #Math
• Algorithms. ~ Jeff Erickson. #eBook #Algorithms
• Building blocks for theoretical computer science. ~ M.M. Fleck. #eBook #CompSci
• Open data structures (An open content textbook). P. Morin. #eBook #Algorithms #CompSci
• Towards a constructive formalization of Perfect Graph Theorems. ~ A.K. Singh, R. Natarajan. #ITP #Coq
• Port of Aleph (an Inductive Logic Programming system) to SWI-Prolog. ~ Fabrizio Riguzzi. #ILP #Prolog
• Groups of order 2019. ~ John D. Cook. #Math #Python
• Resumen de cálculos sobre el año 2019. ~ Antonio Roldán. #Matemáticas
• Nombre 2019, deux-mille-dix-neuf. ~ Gérard Villemin. #Maths
• Learning Lean by example. ~ Kevin Buzzard. #ITP #LeanTheoremProver #Math