Lecturas del Grupo de Lógica Computacional (de julio de 2013 a marzo de 2014)
Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional o en mi página de twitter desde la anterior recopilación.
La recopilación está ordenada por la fecha de su publicación en la lista o en twitter. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.
Lecturas de Julio de 2013
-
Automated proof checking in introductory discrete mathematics classes. ITP Coq
-
On the formal verification of Maple programs. Maple Why3
-
N.G. de Bruijn’s contribution to the formalization of mathematics.
-
Towards certified program logics for the verification of imperative programs. Tesis Coq
-
Bishop-style constructive mathematics in type theory – a tutorial.
-
Why the world needs Haskell. Haskell
-
I/O is pure. Haskell
-
Functoriality. ML
-
Dependent types for an adequate programming of algebra. Haskell Agda
-
Reading an algebra textbook. Isabelle
-
Computer algebra implemented in Isabelle’s function package under Lucas-interpretation: a case study. Isabelle
-
Lurch: a word processor that can grade students’ proofs. Lurch
-
Theorem proving in large formal mathematics as an emerging AI field. ATP
-
Proof pearl: A verified bignum implementation in x86-64 machine code. HOL4
-
Desafíos y oportunidades de la investigación en métodos formales. MF
-
Proofs you can believe in: Proving equivalences between Prolog semantics in Coq. Coq Prolog
-
El uso de los demostradores automáticos de teoremas para la enseñanza de la programación Krakatoa
-
Tackling Fibonacci words puzzles by finite countermodels Mace4
-
Course: Functional problem solving Scheme Racket
-
El lenguaje Python Libro Phyton
-
Inteligencia artificial avanzada Libro IA
-
Program verification based on Kleene algebra in Isabelle/HOL Isabelle
-
Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁ HOL4
-
Exploiting vector instructions with generalized stream fusion Haskell
-
Course: “Functional programming I” Curso PF SML
-
Re-proving theorems, and the trouble with incorrect proofs of true statements Filosofía
-
Measuring the Haskell gap Haskell
-
Why Haskell at school matters Haskell
-
Course: Introduction to Haskell Curso Haskell
-
Pratt’s primality certificates Isabelle
-
Reflections on “A computationally-discovered simplification of the ontological argument Prover9
-
El uso de los demostradores automáticos de teoremas para la enseñanza de la programación. Krakatoa
-
Program verification based on Kleene algebra in Isabelle/HOL. Isabelle
-
Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. HOL4
-
Certified, efficient and sharp univariate Taylor models in Coq. Coq
-
Proofs you can believe in: Proving equivalences between Prolog semantics in Coq. Coq
Lecturas de Agosto de 2013
-
A tutorial on the universality and expressiveness of fold Haskell
-
Matemática discreta y álgebra Lineal Libro Maxima
-
Programming in Martin-Löf’s type theory (an introduction) Libro
-
Type inference, Haskell and dependent types Tesis Haskell
-
A quick tour of Haskell syntax Haskell
-
Generalising monads to arrows Haskell
-
Reasoning about higher-order relational specifications. Abella
-
Probabilistic programming & bayesian methods for hackers IA Python
-
Exámenes de programación funcional con Haskell Libro Haskell
-
Pratt’s primality certificates. Isabelle
-
Formal verification of a proof procedure for the description logic ALC. Isabelle
-
The Königsberg bridge problem and the friendship theorem. Isabelle
-
Formalization of basic linear algebra. Tesis Isabelle
-
A computer-assisted proof of correctness of a marching cubes algorithm Coq
-
Why Lisp is a big hack (and Haskell is doomed to succeed) Haskell Lisp
-
Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. ACL2
-
A computer-assisted proof of correctness of a marching cubes algorithm Coq
-
Proving soundness of combinatorial Vickrey auctions and generating verified executable code. Isabelle
-
20 famous software disasters Divulgación
-
On writing proofs Enseñanza
-
Matemática discreta Libro
-
Mechanized metatheory for a λ λ-calculus with trust types. Coq
-
Proof pearl: A verified bignum implementation in x86-64 machine code. HOL4
-
Automated mathematics Divulgación
-
The Lisp bookshelf Lisp
-
Husk λ scheme: A dialect of R5RS Scheme written in Haskell Haskell Scheme
-
Los números de Ulam en Haskell Haskell
-
Introducción a la teoría de números: ejemplos y algoritmos Libro
-
Cellular automata Haskell
-
Introducción a la demostración asistida por ordenador con Isabelle/HOL Libro Isabelle
-
Steps towards verified implementations of HOL Light. Hol_Light
-
Functional flocks Vida_artificial Haskell Gloss
-
Course: Advanced functional programming Curso Haskell
-
Planetary simulation with excursions in symplectic manifolds Haskell
-
Hacq: A circuit description language for quantum circuits Haskell
-
Lenses from scratch Haskell
-
Comparing Python and Haskell Haskell Python
-
Lens/Aeson traversals/prisms Haskell
Lecturas de Septiembre de 2013
-
Call-by-need supercompilation Tesis Haskell
-
Controlling Chromium in Haskell Haskell
-
A 10 minute tutorial for solving Math problems with Maxima Maxima
-
The nature of code Libro
-
A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle. Isabelle
-
Computational logic and the quest for greater automation Divulgación
-
Cellular automata. Part II: PNGs and Moore in Haskell Haskell
-
ML-TID: A type inference debugger for ML in education ML Educación
-
Polygonal numbers. Mizar
-
Formal verification of cryptographic security proofs. Tesis Isabelle
-
A duality of sorts Haskell
-
An introduction to functional programming PF Haskell Erlang Clojure Scala OCaml
-
Formal verification of language-based concurrent noninterference. Isabelle
-
Conquering folds Haskell
-
Catamorphisms (generalizations of the concept of a fold in functional programming) Haskell
-
On-line lowest common ancestor Haskell
-
Generation of labelled transition systems for Alvis models using Haskell model representation Haskell
-
Modeling uncertain data using monads and an application to the sequence alignment problem Haskell
-
Theory exploration for interactive theorem proving. Isabelle HipSpec Haskell
-
Combining memoisation and change propagation for automatic incremental evaluation of Haskell arrow programs Tesis Haskell
-
Extensible effects: An alternative to monad transformers Haskell
-
Causality of optimized Haskell: What is burning our cycles Haskell
-
Using circular programs for higher-order syntax: Functional pearl Haskell
-
Fun with semirings: A functional pearl on the abuse of linear algebra Haskell
-
MagicHaskeller on the Web: Automated programming as a service Haskell
-
Random testing of purely functional abstract datatypes Haskell
-
Data parallelism in Haskell Haskell
-
A dictionary for reading proofs Divulgación
-
Basic lensing Haskell
-
Automation of mathematical induction as part of the history of logic Historia
-
The future role of computers in mathematics Divulgación
-
Some example MVar, IVar, and LVar programs in Haskell Haskell
Lecturas de Octubre de 2013
-
Formalizing Moessner’s theorem and generalizations in Nuprl Nuprl
-
Clojure’s core.typed vs Haskell Clojure Haskell
-
Zippers and comonads in Haskell Haskell
-
An abstract description method of Map-Reduce-Merge using Haskell Haskell
-
Functional programming in Scheme (With Web programming examples) Scheme
-
A formal model and correctness proof for an access control policy framework. Isabelle
-
Programación, niños y escuelas: el reto del momento Enseñanza
-
Forget foreign languages and music. Teach our kids to code Enseñanza
-
Coin change Haskell
-
An all-atom protein search engine powered by Haskell Haskell
-
A little lens starter tutorial Haskell
-
Introduction to Agda Agda
-
Proving correctness of compilers using structured graphs Haskell
-
Haskell/concurrency braindump Haskell
-
Sorting and searching by distribution: From generic discrimination to generic tries Haskell
-
A gentle introduction to Parsec Haskell
-
Beautiful code, compelling evidence Libro Haskell
Lecturas de Noviembre de 2013
-
Operational semantics of Ltac (A formal study of the tactic language of the Coq proof assistant) Coq
-
Solving sudoku in Racket Racket
-
Teaching induction with functional programming and a proof assistant Educación
-
Nested sequent calculi and theorem proving for normal conditional logics Prolog
-
The social machine of mathematics Filosofía
-
plaimi’s introduction to Haskell for the Haskell-curious game programmer Haskell
-
Qualitative modelling of biological signalling pathways using SAT-solving in Prolog Prolog
-
An introduction to program verification with the Coq proof assistant Coq
-
Real world OCaml: Functional programming for the masses Libro OCaml
-
Formalizing NIST cryptographic standards Divulgación
-
A survey of security research for operating systems Divulgación
-
Haskell, the language most likely to change the way you think about programming Haskell
-
Haskell fast & hard Haskell Tutorial
-
Improving performance of simulation software using Haskell’s concurrency & parallelism Haskell
-
List of long proofs: a list of unusually long mathematical proofs Divulgación
-
Cryptographic protocols formal and computational proofs Verificación
-
Test stream programming using Haskell’s ‘QuickCheck’ Haskell
-
Real world OCaml: Functional programming for the masses Libro OCaml
-
HaskinTeX: A program to evaluate Haskell code within LaTeX Haskell
-
The hereditarily finite sets. Isabelle
-
Gödel’s incompleteness theorems. Isabelle
-
Functional programming for domain-specific languages Haskell
-
Applying formal methods to networking: Theory, techniques and applications MF
-
Compiling DNA strand displacement reactions using a functional programming language ML
-
Recovering intuition from automated formal proofs using tableaux with superdeduction AR
-
A graph library for Isabelle. Isabelle
-
Ensino de Lógica através de estratégias de demonstração e refutação Educación
-
hPDB-Haskell library for processing atomic biomolecular structures in Protein Data Bank format Haskell
-
Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem. Isabelle
-
Haskell as an introduction to parallel computing for undergraduates Haskell
Lecturas de Diciembre de 2013
-
Formal modeling and verification of multi-agent system architecture. PVS
-
SICP (Structure and Interpretation of Computer Programs) in Clojure Clojure
-
Certified Kruskal’s tree theorem. Isabelle
-
CTFP13: Category theory and functional programming 2013 Curso PF
-
Implementation of a library for declarative, resolution-independent 2D graphics in Haskell Haskell
-
Knowledge representation, reasoning, and the design of intelligent agents Libro IA Prolog
-
Concrete semantics (A proof assistant approach) Libro Isabelle
-
Functional programming Haskell
-
Trustworthy embedded systems: formal, code-level proofs for systems over 1 million lines of code Isabelle Haskell
-
The L4.verified project: A formally correct operating system kernel Isabelle Haskell
-
Applications of interactive proof to data flow analysis and security. Isabelle
-
First-order logic completeness for the lazy programmer. Isabelle
-
Using Isabelle/HOL to verify first-order relativity theory. Isabelle
-
Querying an existing database Haskell
-
Moessner’s theorem: an exercise in coinductive reasoning in Coq. Coq
-
Mechanical verification of parameterized real-time systems. Isabelle
-
An application of Answer Set Programming to the field of second language acquisition ASP Prolog
-
Certified programming with dependent types. (December 5, 2013) Libro Coq
-
Course: Foundations of program analysis Haskell Coq
-
Common pitfalls of functional programming and how to avoid them: A mobile gaming platform case study Haskell
-
An IP microscope in Haskell Haskell
-
Simple unique IP system script Haskell
-
10 ways to incorporate Haskell into a modern, functional, CS curriculum Haskell
-
Reliable massively parallel symbolic computing: Fault tolerance for a distributed Haskell Tesis Haskell
-
Structural induction principles for functional programmers. Haskell
-
Exámenes de programación funcional con Haskell (2009-2014). Haskell
-
Introduction to Haskell Haskell
-
Data is evidence Haskell
-
Misfortunes of a mathematicians’ trio using Computer Algebra Systems: Can we trust Divulgación
-
Computabilidad, complejidad computacional y verificación de programas Libro
-
Asteroids in Netwire and Haskell Haskell
-
Formally verified certificate checkers for hardest-to-round computation Coq
-
Development and verification of probability logics and logical frameworks Tesis Coq
-
Formal kinematic analysis of the two-link planar manipulator. HOL_Light
-
Strictness/Unboxed explained Haskell
-
Understanding free monoids and universal constructions Haskell
-
Prolog for programmers Libro Prolog
-
El problema de Josefo en Haskell. Haskell
-
Equational reasoning Haskell
-
El desafío matemático “Un número curioso” en Haskell Haskell
-
Software horror stories (Famous software failures) Verificación
-
Decision procedures for Presburger arithmetic in Haskell Haskell
-
Deboggler: a small project to play with Haskell and data structures Haskell
-
FP Complete’s guide to GHC extensions – a gentler documentation than the GHC docs Haskell
-
The list MonadPlus – Practical fun with monads (Part 2 of 3 Haskell
-
Wolf, goat, cabbage: The list MonadPlus & logic problems Haskell
-
Fallos informáticos y verificación de programas. Verificación
-
Why is formal methods necessary? (Famous software failures) Verificación
-
Illustrative risks to the public in the use of computer systems and related technology Verificación
-
El problema del granjero, la cabra y la col en Haskell Haskell
-
Enseñanza de lógica en la universidad: experiencias en el uso de herramientas informáticas Enseñanza
-
Algoritmos e inducción Algorítmica
-
Máquinas de Turing y otros artilugios Computabilidad
-
Análisis de algoritmos Algorítmica
Lecturas de Enero de 2014
-
Turing machines and undecidability Computabilidad
-
The SageMath Cloud: Python and computational mathematics in the cloud Sage Python
-
Formal analysis of the Kerberos authentication protocol with PVS PVS
-
Running Makefiles with Shake Haskell
-
Free Sage math cloud – Python and symbolic math Sage Python
-
Experimental library of univalent formalization of mathematics HoTT Coq
-
A gentle guide to constraint logic programming via ECLiPSe (Third edition, 2014) Libro Prolog
-
Laziness is a virtue: an introduction to functional programming in Haskell Haskell
-
Dijkstra on Haskell and Java Haskell
-
The “ideal” mathematician Divulgación
-
Applications of the Gauss-Jordan algorithm, done right. Isabelle
-
Verifying document confidentiality of a conference management system. Isabelle
-
Coinitial semantics for redecoration of triangular matrices Coq
-
Bidirectional proof search procedure for intuitionistic modal logic IS5 Coq
-
Axiom selection as a machine learning problem Isabelle ML
-
Squiggoling with bialgebras (Recursion schemes from comonads revisited) Haskell
-
Principles of imperative computation (and methods for ensuring the correctness of programs Curso Algorítmica
-
Proof-by-instance for embedded network design (From prototype to tool roadmap) Isabelle
-
Verifying weight biased leftist heaps using dependent types Agda
-
Abstract interpretation using laziness: Proving Conway’s lost cosmological theorem Haskell
-
Recurrence and induction Divulgación
-
Combining proofs and programs in a dependently typed language Coq
-
Probabilistic relational verification for cryptographic implementations Coq
-
Freeze after writing (Quasi-deterministic parallel programming with LVars) Haskell
-
Modular, higher-order cardinality analysis in theory and practice Haskell
-
Profiling for laziness Racket
-
Modular reasoning about heap paths via effectively propositional formulas SMT Z3
-
Monadic combinators for “putback” style bidirectional programming Haskell
-
The HERMIT in the stream (Fusing stream fusion’s concatMap) Haskell
-
Haskell applicative tutorial: a small tutorial, showing how you can use functors and applicatives Haskell
-
MuCheck : An extensible tool for mutation testing of Haskell programs Haskell
-
A DSL for describing the artificial intelligence in real-time video games Haskell
-
Shortcut fusion for pipes Haskell
-
La sucesión de Kolakoski Haskell
-
Verifying chinese train control system under a combined scenario by theorem proving Isabelle
-
Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5 Isabelle
-
Certifying algorithms Verificación
-
Sucesión de Fibonacci, evaluación perezosa y números construibles Haskell
-
Memorabilia Mathematica (or the philomath’s quotation-book) Libro
-
Two case studies in proving with side-effects: Gödel’s and Kripke’s completeness theorems Agda Coq
-
Formal verification, interactive theorem proving, and automated reasoning Divulgación
-
Specification and verification of concurrent programs through refinements ACL2
-
A formally verified generic branching algorithm for global optimization PVS
-
Twenty years of theorem proving for HOLs (Past, present and future) Historia
-
El juego de Oslo en Haskell Haskell
-
Inductive triple graphs: A purely functional approach to represent RDF Haskell Scala
-
Mathematics in the age of the Turing machine Divulgación
-
A new type of Mathematics? New discoveries expand the scope of computer-assisted proofs of theorems Divulgación
-
Algorithms Libro Algorítmica
-
Balancing lists: a proof pearl. Isabelle
Lecturas de Febrero de 2014
-
On Turing’s legacy in mathematical logic and the foundations of mathematics Historia
-
A survey of axiom selection as a machine learning problem Isabelle
-
Interactive SICP (Structure and Interpretation of Computer Programs) Libro Scheme
-
Arbitrary fun: Generating user profiles with QuickCheck Haskell QuickCheck
-
A little lens starter tutorial Haskell
-
El triángulo de Floyd en Haskell. http://bit.ly/1nRULh Haskell
-
Solving a regular expression crossword with Haskell, Part 2: Representation. Haskell
-
Verification of certifying computations through AutoCorres and Simpl Isabelle
-
Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems SAT SMT
-
Laplace’s equation in Haskell: Using a DSL for stencils Haskell
-
A test driven haskell course Curso Haskell
-
Logic, languages and programming Haskell
-
New draft of Haskell School of Music (PDF) Libro Haskell
-
Properties of random graphs – subgraph containment. Isabelle
-
Monad transformers for backtracking search Haskell SAT
-
A survey of axiom selection as a machine learning problem. Isabelle
-
Proof-by-instance for embedded network design (From prototype to tool roadmap). Isabelle
-
A mathematical proof too long to check – The Erdos discrepancy conjecture SAT
-
Coinitial semantics for redecoration of triangular matrices. Coq
-
A brief intro to QuickCheck Haskell QuickCheck
-
Complexity & verification: The history of programming as problem solving Tesis Historia
-
A denotational semantics for natural language query interfaces to semantic web triplestores Haskell
-
Learning-assisted theorem proving with millions of lemmas IA AR ML
-
Thesis: formal study of efficient algorithms in linear algebra Tesis Coq
-
A tutorial on using the Aeson packaged to parse JSON data Haskell
-
Comprehensive formal verification of an OS microkernel Isabelle Haskell
-
Comparing Haskell Web frameworks Haskell
-
What is formalized Mathematics Divulgación
-
Random numbers in Haskell Haskell
-
Coin change Haskell
-
Simple examples. Haskell Haskell
-
Solution counting Haskell
-
Root finding Haskell
-
Simple interpolation Haskell
-
Automated and (formally) certified proofs of summation formulae Coq
-
Proof assistant based on didactic considerations. Enseñanza ANDY
-
Formalizing Moessner’s theorem and generalizations in Nuprl. Nuprl
-
Preservation of Lyapunov-theoretic proofs: From real to floating-point arithmetic Coq
-
A mechanized proof of loop freedom of the (untimed) AODV routing protocol Isabelle
-
Showing invariance compositionally for a process algebra of network protocols Isabelle
Lecturas de Marzo de 2014
-
Interaction entre algèbre linéaire et analyse en formalisation des mathématiques Tesis Coq
-
A Haskell-implementation of STM Haskell with early conflict detection Haskell
-
Mutation testing of functional programming languages Haskell
-
Harnessing constraint programming for poetry composition ASP
-
Formalization of binary fields and n-dimensional binary vector spaces using the Mizar proof checker Mizar
-
Content development for distance education in advanced university mathematics using Mizar Mizar
-
Learning Agda to be a better Haskell programmer Haskell Agda
-
Learning Prolog to be a better Haskell programmer Haskell Prolog
-
Fun with functional dependencies (or (draft) types as values in static computations in Haskell) Haskell
-
Data.Map vs Data.IntMap Haskell
-
Multi-line strings in Haskell Haskell
-
Implementing a JIT compiled language with Haskell and LLVM Haskell
-
The power of lazy evaluation Haskell
-
Using string literal for symbols Haskell
-
An ACL2 mechanization of an axiomatic weak memory model ACL2
-
From zipper to lens Haskell
-
Lógica de enunciados Libro Lógica
-
Lógica de predicados Libro Lógica
-
Teoría de conjuntos básica (Conjuntos, relaciones y funciones) Libro Lógica
-
Haskell cheat sheets (Part 1) Haskell
-
Hspec: Behavior-driven development for Haskell Haskell BDD
-
Free applicative functors Haskell
-
Algebraic and analytic programming Haskell Math
-
Lógica y álgebra de Boole Libro Lógica
-
LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration Haskell
-
Transparencias del curso “Algoritmia básica” Algorítmica
-
Transparencias del curso “Algoritmia para problemas difíciles” Algorítmica
-
A hybrid TM for Haskell Haskell
-
Tiled polymorphic temporal media. (A functional pearl) Haskell
-
A seamless, client-centric programming model for type safe web applications Haskell
-
Defunctionalizing push arrays Haskell
-
Natural language reasoning using proof-assistant technology: Rich typing and beyond Coq
-
Intro to Haskell for Erlangers Haskell
-
Haskell for OCaml programmers Haskell OCaml
-
Créatúr: Framework for artificial life and other evolutionary algorithms Haskell
-
Improving readability with the Maybe Foldable instance Haskell
-
Probabilistic noninterference Isabelle
-
Mechanization of the Algebra for Wireless Networks (AWN) Isabelle
-
Haskell for Coq programmers Haskell Coq
-
Formal analysis of optical systems HOL_Light
-
Formally verified computation of enclosures of solutions of ordinary differential equations Isabelle
-
Bayesian analysis: A conjugate prior and Markov chain Monte Carlo Haskell
-
Teach yourself logic: A study guide. Version 10.0 (20 March 2014 Libro
-
What’s wrong with the for loop Haskell
-
Why learn Haskell Haskell
-
Algorithme de Babylone : une boucle sous toutes ses formes Haskell
-
Au delà des réels: méthodes numériques en informatique Haskell
-
Méthode de Briggs et de Héron avec MPFR via Haskell et Sage Haskell Sage
-
Gauss par tête et queue Haskell
-
Algèbre et informatique Haskell
-
Poker en Haskell Haskell
-
Mathématique discrète et informatique Libro Haskell
-
Calcul mathématique avec Sage Libro Sage
-
The power algorithm Haskell PHP
-
Modeling and verification of distributed algorithms in theorem proving environments Isabelle
-
Directed security policies: A stateful network implementation Isabelle
-
What it’s like to use Haskell Haskell
-
Colección de problemas sobre inteligencia artificial Libro IA
-
Monaris: A tetris clone written in Haskell using free-game Haskell
-
Formal proof of the fundamental theorem of decorated interval arithmetic Tesis Coq
-
Library to calculate Gröbner basis written in Haskell Haskell
-
Introduction à l’algorithmique et à la programmation avec Python Python
-
Algorithmic problem solving with Python Libro Python
-
Computational discrete mathematics with Python Libro Python
-
Formally verified mathematics Divulgación
-
Formalization of a dynamic logic for graph transformation in the Coq proof assistant Coq
-
Interactive simplifier tracing and debugging in Isabelle Isabelle
Una recopilación de todas las lecturas se encuentra aquí.