Lecturas del año 2013

Lecturas de enero de 2013

1. Problemas sobre el 2013 en Haskell. #Haskell
2. La sucesión de Perrin en Haskell. #Haskell
3. Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
4. Computing square roots using the babylonian method. #Isabelle
5. Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
6. Characteristic formulae for mechanized program verification. #Tesis #Coq
7. Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
8. A proof of Bertrand’s postulate. #Matita
9. Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
10. Formal construction of a set theory in Coq. #Tesis #Coq
11. Rank-nullity theorem in linear algebra. #Isabelle #AFP
12. GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
13. Kleene algebra. #AFP #Isabelle
14. Information-theoretic analysis using theorem proving. #Tesis #HOL4
15. Applying formal methods in software development. #Tesis #PVS
16. Formalization and concretization of ordered networks. #Coq
17. The design of a practical proof checker for a lazy functional language. #MProver #Haskell
18. The formalization of syntax-based mathematical algorithms using quotation and evaluation
19. A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
20. Statistical proof-patterns in Coq/SSReflect. #Coq
21. Towards a logic-based unifying framework for computing. #RA
22. Termination tools in automated reasoning. #Tesis #RA

Lecturas de febrero de 2013

1. Matrices à blocs et en forme canonique. #Coq
2. Automated verification of termination certificates. #Coq
3. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
4. Towards self-verification of Isabelle's Sledgehammer. #Isabelle
5. A framework for the verification of certifying computations. #Isabelle
6. A preliminary univalent formalization of the p-adic numbers. #Coq
7. Algunos vínculos entre los teoremas de Gödel y Turing
8. Formal computations and methods. #Tesis #HOL_Light
9. Complex concept lattices for simulating human prediction in sport. #AFC
10. MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
11. Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq. #Tesis #Coq
12. Temas de programación lógica e inteligencia artificial. #Prolog
13. Una curiosa propiedad del 123 en Haskell. #Haskell
14. A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
15. Otra curiosa propiedad del 123 en Haskell. #Haskell
16. Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
17. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle

Lecturas de marzo de 2013

1. ML4PG: proof-mining in Coq. #Coq
2. Concept-forming operators on multilattices. #AFC
3. The gauge integral theory in HOL4. #HOL4
4. The Picard algorithm for ordinary differential equations in Coq. #Coq
5. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
6. Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
7. Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
8. Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
9. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
10. DAO: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
11. DAO: Ejercicios de argumentación proposicional con Isabelle/HOL. #Isabelle
12. Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
13. DAO: Deducción natural en lógica de primer orden con Isabelle/HOL. #Isabelle
14. DAO: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL. #Isabelle
15. A hierarchy of mathematical structures in ACL2. #ACL2
16. DAO: Argumentación en lógica de primer orden con Isabelle/HOL (1). #Isabelle
17. DAO: Argumentación en lógica de primer orden con Isabelle/HOL (2). #Isabelle
18. Programming and reasonning with powerlists in Coq. #Coq
19. Formalization of the complex number theory in HOL4. #HOL4

Lecturas de abril de 2013

1. Formalizing the confluence of orthogonal rewriting systems. #PVS
2. Homotopy limits in Coq. #Coq
3. Data refinement in Isabelle/HOL. #Isabelle_HOL
4. Formalization of real analysis: A survey of proof assistants and libraries. #ITP
5. AI over large formal knowledge bases: The first decade. #Mizar
6. ForMaRE-formal mathematical reasoning in economics. #RA
7. A fully verified executable LTL model checker. #Isabelle
8. Automating inductive proofs using theory exploration. #Haskell #HipSpec
9. One logic to use them all. #CADE24 #Why3
10. Square root and division elimination in PVS. #PVS #ITP2013
11. Experience report: Teaching Haskell to the masses. #Haskell
12. Coinductive pearl: Modular first-order logic completeness. #Isabelle
13. Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
14. Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
15. Developing an auction theory toolbox. #Isabelle
16. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
17. A formal proof of Kruskal's tree theorem in Isabelle/HOL. #Isabelle
18. A constructive theory of regular languages in Coq. #Coq

Lecturas de mayo de 2013

1. Graph theory (in Isabelle/HOL) Isabelle
2. A macro for reusing abstract functions and theorems ACL2
3. Reseña: Light-weight containers for Isabelle: efficient, extensible, nestable Isabelle
4. Formalizing Turing machines (in Matita) Matita
5. HLearn: A machine learning library for Haskell Haskell IA
6. Computer science concepts in Scratch Libro Scratch
7. Introduction to the OCaml programming language OCaml
8. Introduction to the Coq proof assistant Coq
9. An introduction to quantum programming in Quipper Haskell
10. A certified reduction strategy for homological image processin Coq
11. On the formalization of continuous-time Markov chains in HO HOL4
12. Asynchronous functional reactive programming for GUIs Haskell
13. How computers work: Computational thinking for everyone Libro
14. A Web interface for Isabelle: The next generatio Isabelle
15. The four colour theorem: Engineering of a formal proof Coq
16. Discrete structures via circuits, BDD, SAT, SMT, and functional programming in Python Libro Python
17. Modeling and reasoning about computation Libro Python
18. Understanding Yoneda's lemma with Haskell examples Haskell
19. Game of life in Haskell Haskell
20. Functional game of life (part 3) Haskell
21. Haskell for kids Haskell Gloss
22. Practical SAT solving (Course slides) SAT
23. Verifying refutations with extended resolution ACL2 SAT
24. Homotopy theory in type theory: Progress report Agda
25. Type classes and filters for mathematical analysis in Isabelle/HO Isabelle
26. Parallel and concurrent programming in Haskell Libro Haskell
27. The complete correctness of sorting Agda
28. Discrete mathematics with algorithms (Downloadable version) Libro
29. Certifying Network Calculus in a proof assistant Isabelle
30. Mechanical verification of SAT refutations with extended resolution ACL2 SAT
31. Solving the snake cube puzzle in Haskell Haskell
32. The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups) Coq
33. Automatic data refinement Isabelle
34. Data analysis with monoids Haskell
35. Understanding continuations Haskell
36. The functional programming elevator pitch Haskell
37. The seven bridges of Königsberg Haskell

Lecturas de junio de 2013

1. Representing game dialogue as expressions in first-order logic Tesis Clojure
2. Haskell string calculator kata Haskell
3. Algebra lineal con aplicaciones y Python Libro Python
4. Haskell from C: Where are the for Loops Haskell
5. Speeding through Haskell Libro Haskell
6. Arithmetic algorithms for hereditarily binary natural numbers Haskell
7. Answer-set programming: Motivation and introduction ASP
8. Structural induction principles for functional programmers Haskell
9. Automating theorem proving with SMT Dafny
10. Racket Functional programming to elementary mathematic teachers Racket
11. Certified HLints with Isabelle/HOLCF-Prelude Haskell Isabelle
12. Formalization of basic linear algebra Tesis Isabelle
13. Theorem of three circles in Coq Coq
14. A Prolog specification of giant number arithmetic Prolog
15. Formalizing bounded increase Isabelle
16. Formal verification of language-based concurrent noninterference Isabelle
17. Arithmetic algorithms for hereditarily binary natural numbers Haskell
18. A Haskell library for term rewriting Haskell
19. Understanding algebras Haskell
20. Miller-Rabin primality test Python
21. Data flow fusion with series expressions in Haskell Haskell
22. De Bruijn's ideas on the Formalization of Mathematics Historia
23. Formal mathematics on display: A wiki for Flyspec Flyspec
24. Proofs, upside down (A functional correspondence between natural deduction and the sequent calculus) OCaml
25. Solveurs CP(FD) vérifiés formellemen Coq
26. Formalizing bounded increas Isabelle
27. Certified symbolic manipulation: Bivariate simplicial polynomial ACL2
28. Quipper: a quantum programming language Haskell
29. Distributed data structures with Coq: PN-Counters Coq
30. Computational verification of network programs in Coq Coq
31. The HoTT Book (Homotopy type theory: Univalent foundations of mathematics) Libro HoTT
32. Certifying homological algorithms to study biomedical image Coq SSReflect Haskell QuickCheck

Lecturas de julio de 2013

1. Automated proof checking in introductory discrete mathematics classes. ITP Coq
2. On the formal verification of Maple programs. Maple Why3
3. N.G. de Bruijn's contribution to the formalization of mathematics.
4. Towards certified program logics for the verification of imperative programs. Tesis Coq
5. Bishop-style constructive mathematics in type theory - a tutorial.
6. Proof of impossibility.
7. Why the world needs Haskell. Haskell
8. SMT theory and DPLL(T). SMT
9. I/O is pure. Haskell
10. Gödel's incompleteness theorems formally verified. Isabelle
11. Functoriality. ML
12. Dependent types for an adequate programming of algebra. Haskell Agda
13. Reading an algebra textbook. Isabelle
14. Computer algebra implemented in Isabelle’s function package under Lucas-interpretation: a case study. Isabelle
15. Lurch: a word processor that can grade students' proofs. Lurch
16. Theorem proving in large formal mathematics as an emerging AI field. ATP
17. What, if anything, is a declarative language. PD
18. Proof pearl: A verified bignum implementation in x86-64 machine code. HOL4
19. Desafíos y oportunidades de la investigación en métodos formales. MF
20. Proofs you can believe in: Proving equivalences between Prolog semantics in Coq. Coq Prolog
21. El uso de los demostradores automáticos de teoremas para la enseñanza de la programación Krakatoa
22. Tackling Fibonacci words puzzles by finite countermodels Mace4
23. Parallel and concurrent programming in Haskell Haskell
24. Analizadores sintácticos funcionales Haskell
25. A taste of the λ calculus LC
26. Course: Functional problem solving Scheme Racket
27. A short tutorial on the internals of a theorem prover ZOL
28. El lenguaje Python Libro Phyton
29. Inteligencia artificial avanzada Libro IA
30. Program verification based on Kleene algebra in Isabelle/HOL Isabelle
31. Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁ HOL4
32. Exploiting vector instructions with generalized stream fusion Haskell
33. IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment) 1.9.0 released Isabelle
34. Course: "Functional programming I" Curso PF SML
35. Re-proving theorems, and the trouble with incorrect proofs of true statements Filosofía
36. Measuring the Haskell gap Haskell
37. Why Haskell at school matters Haskell
38. Course: Introduction to Haskell Curso Haskell
39. Pratt's primality certificates Isabelle
40. Automatic SIMD vectorization for Haskell Haskell
41. Reflections on “A computationally-discovered simplification of the ontological argument Prover9
42. Computational verification of network programs in Coq. Coq
43. El uso de los demostradores automáticos de teoremas para la enseñanza de la programación. Krakatoa
44. Program verification based on Kleene algebra in Isabelle/HOL. Isabelle
45. Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁. HOL4
46. Certified, efficient and sharp univariate Taylor models in Coq. Coq
47. Proofs you can believe in: Proving equivalences between Prolog semantics in Coq. Coq

Lecturas de agosto de 2013

1. A tutorial on the universality and expressiveness of fold Haskell
2. Matemática discreta y álgebra Lineal Libro Maxima
3. Discrete mathematics and functional programming Libro ML
4. Programming in Martin-Löf’s type theory (an introduction) Libro
5. A silent revolution in mathematics (The rise of applications, numerical methods, and computational approaches) Divulgación
6. Type inference, Haskell and dependent types Tesis Haskell
7. A quick tour of Haskell syntax Haskell
8. Unifying structured recursion schemes Haskell
9. GPU programming in functional languages (A comparison of Haskell GPU embedded domain specific languages) Haskell
10. Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar Mizar
11. Generalising monads to arrows Haskell
12. Reasoning about higher-order relational specifications. Abella
13. Probabilistic programming & bayesian methods for hackers IA Python
14. Exámenes de programación funcional con Haskell Libro Haskell
15. Pratt's primality certificates. Isabelle
16. Formal verification of a proof procedure for the description logic ALC. Isabelle
17. The Königsberg bridge problem and the friendship theorem. Isabelle
18. Formalization of basic linear algebra. Tesis Isabelle
19. A computer-assisted proof of correctness of a marching cubes algorithm Coq
20. Why Lisp is a big hack (and Haskell is doomed to succeed) Haskell Lisp
21. Proof-pattern recognition in ACL2 ACL2 ML
22. Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm. ACL2
23. A computer-assisted proof of correctness of a marching cubes algorithm Coq
24. Proving soundness of combinatorial Vickrey auctions and generating verified executable code. Isabelle
25. 20 famous software disasters Divulgación
26. On writing proofs Enseñanza
27. Matemática discreta Libro
28. Mechanized metatheory for a λ λ-calculus with trust types. Coq
29. Proof pearl: A verified bignum implementation in x86-64 machine code. HOL4
30. Two monoids for approximating NP-complete problems Haskell
31. Automated mathematics Divulgación
32. The Lisp bookshelf Lisp
33. Counting lattice paths Lisp
34. Binary search & Newton-Raphson root finding Lisp
35. La Lógica en las ciencias computacionales Enseñanza
36. Generic datatypes à la carte. Coq
37. Introducción al cálculo simbólico con Maxima. Maxima
38. Husk λ scheme: A dialect of R5RS Scheme written in Haskell Haskell Scheme
39. Los números de Ulam en Haskell Haskell
40. Introducción a la teoría de números: ejemplos y algoritmos Libro
41. Do extraterrestrials use functional programming Haskell
42. The bowling game kata in functional common lisp Lisp
43. Cellular automata Haskell
44. Introducción a la demostración asistida por ordenador con Isabelle/HOL Libro Isabelle
45. Steps towards verified implementations of HOL Light. Hol_Light
46. Functional flocks Vida_artificial Haskell Gloss
47. Course: Advanced functional programming Curso Haskell
48. The programming language zoo OCaml
49. Planetary simulation with excursions in symplectic manifolds Haskell
50. Computational category theory ML
51. Pretext by experiments and guesses Haskell
52. Hacq: A circuit description language for quantum circuits Haskell
53. Lenses from scratch Haskell
54. Comparing Python and Haskell Haskell Python
55. Lens/Aeson traversals/prisms Haskell
56. An introduction to language processing Haskell

Lecturas de septiembre de 2013

1. Call-by-need supercompilation Tesis Haskell
2. Controlling Chromium in Haskell Haskell
3. A 10 minute tutorial for solving Math problems with Maxima Maxima
4. The nature of code Libro
5. [mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle]. Isabelle
6. Computational logic and the quest for greater automation Divulgación
7. Supercompiling Haskell to hardware Haskell
8. Cellular automata. Part II: PNGs and Moore in Haskell Haskell
9. ML-TID: A type inference debugger for ML in education ML Educación
10. Polygonal numbers. Mizar
11. Formal verification of cryptographic security proofs. Tesis Isabelle
12. A TCAS-II resolution advisory algorithm. PVS
13. Números y hoja de cálculo V Libro
14. A duality of sorts Haskell
15. Learn Common Lisp in Y minutes Lisp
16. An introduction to functional programming PF Haskell Erlang Clojure Scala OCaml
17. Formal verification of language-based concurrent noninterference. Isabelle
18. Advanced functional programming for fun and profit Haskell
19. Mathematical logic for mathematicians, Part I Libro
20. Sobre la Inteligencia Artificial IA
21. Quark: A web browser with a formally verified kernel Coq
22. Computer theorem proving and HoTT. HoTT
23. From Tarski to Hilbert. Coq
24. Conquering folds Haskell
25. Catamorphisms (generalizations of the concept of a fold in functional programming) Haskell
26. On-line lowest common ancestor Haskell
27. Generation of labelled transition systems for Alvis models using Haskell model representation Haskell
28. Modeling uncertain data using monads and an application to the sequence alignment problem Haskell
29. El problema de las sucesiones llenas en Haskell Haskell
30. Theory exploration for interactive theorem proving. Isabelle HipSpec Haskell
31. Combining memoisation and change propagation for automatic incremental evaluation of Haskell arrow programs Tesis Haskell
32. Extensible effects: An alternative to monad transformers Haskell
33. System FC with explicit kind equality Haskell
34. Causality of optimized Haskell: What is burning our cycles Haskell
35. Using circular programs for higher-order syntax: Functional pearl Haskell
36. Fun with semirings: A functional pearl on the abuse of linear algebra Haskell
37. MagicHaskeller on the Web: Automated programming as a service Haskell
38. Random testing of purely functional abstract datatypes Haskell
39. Data parallelism in Haskell Haskell
40. Computational mathematics in the cloud with Sagemath Sage
41. Sistemas multiagente y simulación IA
42. A dictionary for reading proofs Divulgación
43. Mathematical logic (Lecture notes) Libro
44. Basic lensing Haskell
45. Automation of mathematical induction as part of the history of logic Historia
46. The future role of computers in mathematics Divulgación
47. Some example MVar, IVar, and LVar programs in Haskell Haskell
48. Revisiting examples of computer assisted mathematics Sage

Lecturas de octubre de 2013

1. Formalizing Moessner’s theorem and generalizations in Nuprl Nuprl
2. Clojure's core.typed vs Haskell Clojure Haskell
3. The ontological argument in PVS. PVS
4. Zippers and comonads in Haskell Haskell
5. Voevodsky’s mathematical revolution HoTT
6. Quantum artificial intelligence: A survey of application of quantum physics in artificial intelligence IA
7. An abstract description method of Map-Reduce-Merge using Haskell Haskell
8. Functional programming in Scheme (With Web programming examples) Scheme
9. A formal model and correctness proof for an access control policy framework. Isabelle
10. Verified AIG algorithms in ACL2. ACL2
11. Programación, niños y escuelas: el reto del momento Enseñanza
12. Forget foreign languages and music. Teach our kids to code Enseñanza
13. Coin change Haskell
14. An all-atom protein search engine powered by Haskell Haskell
15. A little lens starter tutorial Haskell
16. Introduction to Agda Agda
17. Proving correctness of compilers using structured graphs Haskell
18. Haskell/concurrency braindump Haskell
19. Sorting and searching by distribution: From generic discrimination to generic tries Haskell
20. A gentle introduction to Parsec Haskell
21. Haskell optimization and the game of life Haskell
22. Beautiful code, compelling evidence Libro Haskell
23. Course: Language-oriented programming Lisp

Lecturas de noviembre de 2013

1. Trimming while checking clausal proofs SAT
2. Efficiently computing Kendall's tau Clojure
3. Lambda calculus LC
4. Modular monadic meta-theory Coq
5. Operational semantics of Ltac (A formal study of the tactic language of the Coq proof assistant) Coq
6. Solving sudoku in Racket Racket
7. Teaching induction with functional programming and a proof assistant Educación
8. [machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets]. Isabelle
9. Proof verification within set theory
10. A Description Logics Tableau Reasoner in Prolog Prolog
11. Nested sequent calculi and theorem proving for normal conditional logics Prolog
12. Martin-Löf and an introduction to Agda Agda
13. The social machine of mathematics Filosofía
14. Applications of real number theorem proving in PVS. PVS
15. plaimi’s introduction to Haskell for the Haskell-curious game programmer Haskell
16. Qualitative modelling of biological signalling pathways using SAT-solving in Prolog Prolog
17. An introduction to program verification with the Coq proof assistant Coq
18. Real world OCaml: Functional programming for the masses Libro OCaml
19. Formalizing NIST cryptographic standards Divulgación
20. Partial type signatures for Haskell Haskell
21. A survey of security research for operating systems Divulgación
22. Haskell, the language most likely to change the way you think about programming Haskell
23. Haskell fast & hard Haskell Tutorial
24. Philosophy of computer science Libro
25. Improving performance of simulation software using Haskell’s concurrency & parallelism Haskell
26. List of long proofs: a list of unusually long mathematical proofs Divulgación
27. Cryptographic protocols formal and computational proofs Verificación
28. Test stream programming using Haskell's 'QuickCheck' Haskell
29. Real world OCaml: Functional programming for the masses Libro OCaml
30. HaskinTeX: A program to evaluate Haskell code within LaTeX Haskell
31. Sucesión con radicales en Haskell Haskell
32. Profiling for laziness
33. Leaking space (Eliminating memory hogs) Haskell
34. The hereditarily finite sets. Isabelle
35. Gödel's incompleteness theorems. Isabelle
36. Functional programming for domain-specific languages Haskell
37. Applying formal methods to networking: Theory, techniques and applications MF
38. Compiling DNA strand displacement reactions using a functional programming language ML
39. Recovering intuition from automated formal proofs using tableaux with superdeduction AR
40. A graph library for Isabelle. Isabelle
41. Experience report: The next 600 Haskell programmers Haskell
42. Ensino de Lógica através de estratégias de demonstração e refutação Educación
43. Sistemas complejos, sistemas dinámicos y redes complejas IA
44. Sistemas complejos, caos y vida artificial IA
45. hPDB-Haskell library for processing atomic biomolecular structures in Protein Data Bank format Haskell
46. Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem. Isabelle
47. Haskell as an introduction to parallel computing for undergraduates Haskell
48. Algoritmos genéticos y computación evolutiva IA
49. Sistemas colectivos. Inteligencia colectiva IA
50. Autómatas celulares IA

Lecturas de diciembre de 2013

1. Formal modeling and verification of multi-agent system architecture. PVS
2. SICP (Structure and Interpretation of Computer Programs) in Clojure Clojure
3. Certified Kruskal’s tree theorem. Isabelle
4. Category theory for scientists Curso
5. CTFP13: Category theory and functional programming 2013 Curso PF
6. Program design by calculation Libro
7. Implementation of a library for declarative, resolution-independent 2D graphics in Haskell Haskell
8. Functioning hardware from functional programs Haskell
9. Refinements for free!. Coq
10. Knowledge representation, reasoning, and the design of intelligent agents Libro IA Prolog
11. Formalizing probabilistic noninterference. Isabelle
12. Concrete semantics (A proof assistant approach) Libro Isabelle
13. Functional programming Haskell
14. Aliasing restrictions of C11 formalized in Coq. Coq
15. Trustworthy embedded systems: formal, code-level proofs for systems over 1 million lines of code Isabelle Haskell
16. The L4.verified project: A formally correct operating system kernel Isabelle Haskell
17. Applications of interactive proof to data flow analysis and security. Isabelle
18. First-order logic completeness for the lazy programmer. Isabelle
19. Popularizing Haskell through easy web deployment Haskell
20. À la croisée des fondements des mathématiques, de l’informatique et de la topologie. (Théorie homotopique des types) HoTT
21. Haskell, Ising, Markov & Metropolis Haskell
22. A domain-specific language for discrete mathematics Haskell
23. Using Isabelle/HOL to verify first-order relativity theory. Isabelle
24. Homotopy type theory and univalent foundations HoTT
25. An introduction to Homotopy Type Theory HoTT
26. Querying an existing database Haskell
27. Moessner’s theorem: an exercise in coinductive reasoning in Coq. Coq
28. Mechanical verification of parameterized real-time systems. Isabelle
29. Fun with PolyKinds - PolyKinded folds Haskell
30. An application of Answer Set Programming to the field of second language acquisition ASP Prolog
31. Certified programming with dependent types. (December 5, 2013) Libro Coq
32. Course: Foundations of program analysis Haskell Coq
33. Common pitfalls of functional programming and how to avoid them: A mobile gaming platform case study Haskell
34. The space-saving algorithm in Haskell Haskell
35. An IP microscope in Haskell Haskell
36. Simple unique IP system script Haskell
37. 10 ways to incorporate Haskell into a modern, functional, CS curriculum Haskell
38. Why functional programming matters Haskell
39. Reliable massively parallel symbolic computing: Fault tolerance for a distributed Haskell Tesis Haskell
40. Structural induction principles for functional programmers. Haskell
41. Linked data, logic programming and black risotto Prolog
42. Exámenes de programación funcional con Haskell (2009-2014). Haskell
43. Introduction to Haskell Haskell
44. Data is evidence Haskell
45. Misfortunes of a mathematicians' trio using Computer Algebra Systems: Can we trust Divulgación
46. Artificial intelligence: The machines with alien minds IA
47. An exercise on streams: convergence acceleration Haskell
48. A functional approach to standard binary heaps Scala
49. Computabilidad, complejidad computacional y verificación de programas Libro
50. Asteroids in Netwire and Haskell Haskell
51. Formally verified certificate checkers for hardest-to-round computation Coq
52. Development and verification of probability logics and logical frameworks Tesis Coq
53. Formal kinematic analysis of the two-link planar manipulator. HOL_Light
54. Type theory and applications Libro
55. Strictness/Unboxed explained Haskell
56. How Haskell can solve the integration problem Haskell
57. Modeling and optimizing MapReduce programs Haskell
58. Understanding free monoids and universal constructions Haskell
59. Curso: Programación funcional avanzada Haskell
60. Prolog for programmers Libro Prolog
61. El problema de Josefo en Haskell. Haskell
62. Evaluación en Haskell con tiempo acotado. Haskell
63. El juego de “tres en raya” en Haskell Haskell
64. Equational reasoning Haskell
65. El desafío matemático “Un número curioso” en Haskell Haskell
66. Software horror stories (Famous software failures) Verificación
67. Decision procedures for Presburger arithmetic in Haskell Haskell
68. Deboggler: a small project to play with Haskell and data structures Haskell
69. FP Complete's guide to GHC extensions - a gentler documentation than the GHC docs Haskell
70. Practical fun with monads - Introducing: MonadPlus! Haskell
71. The list MonadPlus - Practical fun with monads (Part 2 of 3 Haskell
72. Wolf, goat, cabbage: The list MonadPlus & logic problems Haskell
73. The heart and soul of computability Libro
74. Fallos informáticos y verificación de programas. Verificación
75. Why is formal methods necessary? (Famous software failures) Verificación
76. Illustrative risks to the public in the use of computer systems and related technology Verificación
77. El problema del granjero, la cabra y la col en Haskell Haskell
78. Enseñanza de lógica en la universidad: experiencias en el uso de herramientas informáticas Enseñanza
79. Algoritmos e inducción Algorítmica
80. Máquinas de Turing y otros artilugios Computabilidad
81. Análisis de algoritmos Algorítmica