Lecturas del año 2013
De WikiGLC
Lecturas de enero de 2013
- Problemas sobre el 2013 en Haskell. #Haskell
- La sucesión de Perrin en Haskell. #Haskell
- Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
- Computing square roots using the babylonian method. #Isabelle
- Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
- Characteristic formulae for mechanized program verification. #Tesis #Coq
- Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
- A proof of Bertrand’s postulate. #Matita
- Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
- Formal construction of a set theory in Coq. #Tesis #Coq
- Rank-nullity theorem in linear algebra. #Isabelle #AFP
- GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
- Kleene algebra. #AFP #Isabelle
- Information-theoretic analysis using theorem proving. #Tesis #HOL4
- Applying formal methods in software development. #Tesis #PVS
- Formalization and concretization of ordered networks. #Coq
- The design of a practical proof checker for a lazy functional language. #MProver #Haskell
- The formalization of syntax-based mathematical algorithms using quotation and evaluation
- A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
- Statistical proof-patterns in Coq/SSReflect. #Coq
- Towards a logic-based unifying framework for computing. #RA
- Termination tools in automated reasoning. #Tesis #RA
Lecturas de febrero de 2013
- Matrices à blocs et en forme canonique. #Coq
- Automated verification of termination certificates. #Coq
- Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
- Towards self-verification of Isabelle's Sledgehammer. #Isabelle
- A framework for the verification of certifying computations. #Isabelle
- A preliminary univalent formalization of the p-adic numbers. #Coq
- Algunos vínculos entre los teoremas de Gödel y Turing
- Formal computations and methods. #Tesis #HOL_Light
- Complex concept lattices for simulating human prediction in sport. #AFC
- MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
- Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq. #Tesis #Coq
- Temas de programación lógica e inteligencia artificial. #Prolog
- Una curiosa propiedad del 123 en Haskell. #Haskell
- A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
- Otra curiosa propiedad del 123 en Haskell. #Haskell
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
- Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle
Lecturas de marzo de 2013
- ML4PG: proof-mining in Coq. #Coq
- Concept-forming operators on multilattices. #AFC
- The gauge integral theory in HOL4. #HOL4
- The Picard algorithm for ordinary differential equations in Coq. #Coq
- Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
- Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
- Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
- Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
- Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
- DAO: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
- DAO: Ejercicios de argumentación proposicional con Isabelle/HOL. #Isabelle
- Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
- DAO: Deducción natural en lógica de primer orden con Isabelle/HOL. #Isabelle
- DAO: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL. #Isabelle
- A hierarchy of mathematical structures in ACL2. #ACL2
- DAO: Argumentación en lógica de primer orden con Isabelle/HOL (1). #Isabelle
- DAO: Argumentación en lógica de primer orden con Isabelle/HOL (2). #Isabelle
- Programming and reasonning with powerlists in Coq. #Coq
- Formalization of the complex number theory in HOL4. #HOL4
Lecturas de abril de 2013
- Formalizing the confluence of orthogonal rewriting systems. #PVS
- Homotopy limits in Coq. #Coq
- Data refinement in Isabelle/HOL. #Isabelle_HOL
- Formalization of real analysis: A survey of proof assistants and libraries. #ITP
- AI over large formal knowledge bases: The first decade. #Mizar
- ForMaRE-formal mathematical reasoning in economics. #RA
- A fully verified executable LTL model checker. #Isabelle
- Automating inductive proofs using theory exploration. #Haskell #HipSpec
- One logic to use them all. #CADE24 #Why3
- Square root and division elimination in PVS. #PVS #ITP2013
- Experience report: Teaching Haskell to the masses. #Haskell
- Coinductive pearl: Modular first-order logic completeness. #Isabelle
- Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
- Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
- Developing an auction theory toolbox. #Isabelle
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
- A formal proof of Kruskal's tree theorem in Isabelle/HOL. #Isabelle
- A constructive theory of regular languages in Coq. #Coq
Lecturas de mayo de 2013
- Graph theory (in Isabelle/HOL) Isabelle
- A macro for reusing abstract functions and theorems ACL2
- Reseña: Light-weight containers for Isabelle: efficient, extensible, nestable Isabelle
- Formalizing Turing machines (in Matita) Matita
- HLearn: A machine learning library for Haskell Haskell IA
- Computer science concepts in Scratch Libro Scratch
- Introduction to the OCaml programming language OCaml
- Introduction to the Coq proof assistant Coq
- An introduction to quantum programming in Quipper Haskell
- A certified reduction strategy for homological image processin Coq
- On the formalization of continuous-time Markov chains in HO HOL4
- Asynchronous functional reactive programming for GUIs Haskell
- How computers work: Computational thinking for everyone Libro
- A Web interface for Isabelle: The next generatio Isabelle
- The four colour theorem: Engineering of a formal proof Coq
- Discrete structures via circuits, BDD, SAT, SMT, and functional programming in Python Libro Python
- Modeling and reasoning about computation Libro Python
- Understanding Yoneda's lemma with Haskell examples Haskell
- Game of life in Haskell Haskell
- Functional game of life (part 3) Haskell
- Haskell for kids Haskell Gloss
- Practical SAT solving (Course slides) SAT
- Verifying refutations with extended resolution ACL2 SAT
- Homotopy theory in type theory: Progress report Agda
- Type classes and filters for mathematical analysis in Isabelle/HO Isabelle
- Parallel and concurrent programming in Haskell Libro Haskell
- The complete correctness of sorting Agda
- Discrete mathematics with algorithms (Downloadable version) Libro
- Certifying Network Calculus in a proof assistant Isabelle
- Mechanical verification of SAT refutations with extended resolution ACL2 SAT
- Solving the snake cube puzzle in Haskell Haskell
- The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups) Coq
- Automatic data refinement Isabelle
- Data analysis with monoids Haskell
- Understanding continuations Haskell
- The functional programming elevator pitch Haskell
- The seven bridges of Königsberg Haskell
Lecturas de junio de 2013
- Representing game dialogue as expressions in first-order logic Tesis Clojure
- Haskell string calculator kata Haskell
- Algebra lineal con aplicaciones y Python Libro Python
- Haskell from C: Where are the for Loops Haskell
- Speeding through Haskell Libro Haskell
- Arithmetic algorithms for hereditarily binary natural numbers Haskell
- Answer-set programming: Motivation and introduction ASP
- Structural induction principles for functional programmers Haskell
- Automating theorem proving with SMT Dafny
- Racket Functional programming to elementary mathematic teachers Racket
- Certified HLints with Isabelle/HOLCF-Prelude Haskell Isabelle
- Formalization of basic linear algebra Tesis Isabelle
- Theorem of three circles in Coq Coq
- A Prolog specification of giant number arithmetic Prolog
- Formalizing bounded increase Isabelle
- Formal verification of language-based concurrent noninterference Isabelle
- Arithmetic algorithms for hereditarily binary natural numbers Haskell
- A Haskell library for term rewriting Haskell
- Understanding algebras Haskell
- Miller-Rabin primality test Python
- Data flow fusion with series expressions in Haskell Haskell
- De Bruijn's ideas on the Formalization of Mathematics Historia
- Formal mathematics on display: A wiki for Flyspec Flyspec
- Proofs, upside down (A functional correspondence between natural deduction and the sequent calculus) OCaml
- Solveurs CP(FD) vérifiés formellemen Coq
- Formalizing bounded increas Isabelle
- Certified symbolic manipulation: Bivariate simplicial polynomial ACL2
- Quipper: a quantum programming language Haskell
- Distributed data structures with Coq: PN-Counters Coq
- Computational verification of network programs in Coq Coq
- The HoTT Book (Homotopy type theory: Univalent foundations of mathematics) Libro HoTT
- Certifying homological algorithms to study biomedical image Coq SSReflect Haskell QuickCheck
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.
- Proof of impossibility.
- Why the world needs Haskell. Haskell
- SMT theory and DPLL(T). SMT
- I/O is pure. Haskell
- Gödel's incompleteness theorems formally verified. Isabelle
- 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
- What, if anything, is a declarative language. PD
- 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
- Parallel and concurrent programming in Haskell Haskell
- Analizadores sintácticos funcionales Haskell
- A taste of the λ calculus LC
- Course: Functional problem solving Scheme Racket
- A short tutorial on the internals of a theorem prover ZOL
- 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
- IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment) 1.9.0 released Isabelle
- 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
- Automatic SIMD vectorization for Haskell Haskell
- Reflections on “A computationally-discovered simplification of the ontological argument Prover9
- Computational verification of network programs in Coq. Coq
- 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
- Discrete mathematics and functional programming Libro ML
- Programming in Martin-Löf’s type theory (an introduction) Libro
- A silent revolution in mathematics (The rise of applications, numerical methods, and computational approaches) Divulgación
- Type inference, Haskell and dependent types Tesis Haskell
- A quick tour of Haskell syntax Haskell
- Unifying structured recursion schemes Haskell
- GPU programming in functional languages (A comparison of Haskell GPU embedded domain specific languages) Haskell
- Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar Mizar
- 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
- Proof-pattern recognition in ACL2 ACL2 ML
- 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
- Two monoids for approximating NP-complete problems Haskell
- Automated mathematics Divulgación
- The Lisp bookshelf Lisp
- Counting lattice paths Lisp
- Binary search & Newton-Raphson root finding Lisp
- La Lógica en las ciencias computacionales Enseñanza
- Generic datatypes à la carte. Coq
- Introducción al cálculo simbólico con Maxima. Maxima
- 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
- Do extraterrestrials use functional programming Haskell
- The bowling game kata in functional common lisp Lisp
- 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
- The programming language zoo OCaml
- Planetary simulation with excursions in symplectic manifolds Haskell
- Computational category theory ML
- Pretext by experiments and guesses 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
- An introduction to language processing 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
- [mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle]. Isabelle
- Computational logic and the quest for greater automation Divulgación
- Supercompiling Haskell to hardware Haskell
- 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 TCAS-II resolution advisory algorithm. PVS
- Números y hoja de cálculo V Libro
- A duality of sorts Haskell
- Learn Common Lisp in Y minutes Lisp
- An introduction to functional programming PF Haskell Erlang Clojure Scala OCaml
- Formal verification of language-based concurrent noninterference. Isabelle
- Advanced functional programming for fun and profit Haskell
- Mathematical logic for mathematicians, Part I Libro
- Sobre la Inteligencia Artificial IA
- Quark: A web browser with a formally verified kernel Coq
- Computer theorem proving and HoTT. HoTT
- From Tarski to Hilbert. Coq
- 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
- El problema de las sucesiones llenas en Haskell 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
- System FC with explicit kind equality 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
- Computational mathematics in the cloud with Sagemath Sage
- Sistemas multiagente y simulación IA
- A dictionary for reading proofs Divulgación
- Mathematical logic (Lecture notes) Libro
- 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
- Revisiting examples of computer assisted mathematics Sage
Lecturas de octubre de 2013
- Formalizing Moessner’s theorem and generalizations in Nuprl Nuprl
- Clojure's core.typed vs Haskell Clojure Haskell
- The ontological argument in PVS. PVS
- Zippers and comonads in Haskell Haskell
- Voevodsky’s mathematical revolution HoTT
- Quantum artificial intelligence: A survey of application of quantum physics in artificial intelligence IA
- 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
- Verified AIG algorithms in ACL2. ACL2
- 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
- Haskell optimization and the game of life Haskell
- Beautiful code, compelling evidence Libro Haskell
- Course: Language-oriented programming Lisp
Lecturas de noviembre de 2013
- Trimming while checking clausal proofs SAT
- Efficiently computing Kendall's tau Clojure
- Lambda calculus LC
- Modular monadic meta-theory Coq
- 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
- [machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets]. Isabelle
- Proof verification within set theory
- A Description Logics Tableau Reasoner in Prolog Prolog
- Nested sequent calculi and theorem proving for normal conditional logics Prolog
- Martin-Löf and an introduction to Agda Agda
- The social machine of mathematics Filosofía
- Applications of real number theorem proving in PVS. PVS
- 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
- Partial type signatures for Haskell Haskell
- 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
- Philosophy of computer science Libro
- 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
- Sucesión con radicales en Haskell Haskell
- Profiling for laziness
- Leaking space (Eliminating memory hogs) 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
- Experience report: The next 600 Haskell programmers Haskell
- Ensino de Lógica através de estratégias de demonstração e refutação Educación
- Sistemas complejos, sistemas dinámicos y redes complejas IA
- Sistemas complejos, caos y vida artificial IA
- 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
- Algoritmos genéticos y computación evolutiva IA
- Sistemas colectivos. Inteligencia colectiva IA
- Autómatas celulares IA
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
- Category theory for scientists Curso
- CTFP13: Category theory and functional programming 2013 Curso PF
- Program design by calculation Libro
- Implementation of a library for declarative, resolution-independent 2D graphics in Haskell Haskell
- Functioning hardware from functional programs Haskell
- Refinements for free!. Coq
- Knowledge representation, reasoning, and the design of intelligent agents Libro IA Prolog
- Formalizing probabilistic noninterference. Isabelle
- Concrete semantics (A proof assistant approach) Libro Isabelle
- Functional programming Haskell
- Aliasing restrictions of C11 formalized in Coq. Coq
- 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
- Popularizing Haskell through easy web deployment Haskell
- À la croisée des fondements des mathématiques, de l’informatique et de la topologie. (Théorie homotopique des types) HoTT
- Haskell, Ising, Markov & Metropolis Haskell
- A domain-specific language for discrete mathematics Haskell
- Using Isabelle/HOL to verify first-order relativity theory. Isabelle
- Homotopy type theory and univalent foundations HoTT
- An introduction to Homotopy Type Theory HoTT
- Querying an existing database Haskell
- Moessner’s theorem: an exercise in coinductive reasoning in Coq. Coq
- Mechanical verification of parameterized real-time systems. Isabelle
- Fun with PolyKinds - PolyKinded folds Haskell
- 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
- The space-saving algorithm in Haskell 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
- Why functional programming matters Haskell
- Reliable massively parallel symbolic computing: Fault tolerance for a distributed Haskell Tesis Haskell
- Structural induction principles for functional programmers. Haskell
- Linked data, logic programming and black risotto Prolog
- 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
- Artificial intelligence: The machines with alien minds IA
- An exercise on streams: convergence acceleration Haskell
- A functional approach to standard binary heaps Scala
- 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
- Type theory and applications Libro
- Strictness/Unboxed explained Haskell
- How Haskell can solve the integration problem Haskell
- Modeling and optimizing MapReduce programs Haskell
- Understanding free monoids and universal constructions Haskell
- Curso: Programación funcional avanzada Haskell
- Prolog for programmers Libro Prolog
- El problema de Josefo en Haskell. Haskell
- Evaluación en Haskell con tiempo acotado. Haskell
- El juego de “tres en raya” 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
- Practical fun with monads - Introducing: MonadPlus! Haskell
- The list MonadPlus - Practical fun with monads (Part 2 of 3 Haskell
- Wolf, goat, cabbage: The list MonadPlus & logic problems Haskell
- The heart and soul of computability Libro
- 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
