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

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. A 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. A 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

Lecturas de Enero de 2014

1. Lecture notes on the lambda calculus LC

2. Turing machines and undecidability Computabilidad

3. The SageMath Cloud: Python and computational mathematics in the cloud Sage Python

4. EasyAI: a pure-Python artificial intelligence framework for two-players abstract games such as Tic Tac Toe IA Python

5. A whirlwind tour of combinatorial games in Haskell Haskell

6. Semantics-directed machine architecture in ReWire Haskell

7. Formal analysis of the Kerberos authentication protocol with PVS PVS

8. Running Makefiles with Shake Haskell

9. Free Sage math cloud – Python and symbolic math Sage Python

10. Typed syntactic meta-programming Agda

11. Modular type-safety proofs in Agda Agda

12. IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment) 1.9.1 released Isabelle

13. Experimental library of univalent formalization of mathematics HoTT Coq

14. A gentle guide to constraint logic programming via ECLiPSe (Third edition, 2014) Libro Prolog

15. Laziness is a virtue: an introduction to functional programming in Haskell Haskell

16. Dijkstra on Haskell and Java Haskell

17. The “ideal” mathematician Divulgación

18. Applications of the Gauss-Jordan algorithm, done right. Isabelle

19. Verifying document confidentiality of a conference management system. Isabelle

20. Coinitial semantics for redecoration of triangular matrices Coq

21. Bidirectional proof search procedure for intuitionistic modal logic IS5 Coq

22. Axiom selection as a machine learning problem Isabelle ML

23. Squiggoling with bialgebras (Recursion schemes from comonads revisited) Haskell

24. aspeed: Solver scheduling via answer set programming ASP

25. Principles of imperative computation (and methods for ensuring the correctness of programs Curso Algorítmica

26. Automatic functional harmonic analysis Haskell

27. Proof-by-instance for embedded network design (From prototype to tool roadmap) Isabelle

28. Verifying weight biased leftist heaps using dependent types Agda

29. Abstract interpretation using laziness: Proving Conway’s lost cosmological theorem Haskell

30. Recurrence and induction Divulgación

31. Backpack: Retrofitting Haskell with interfaces Haskell

32. Combining proofs and programs in a dependently typed language Coq

33. A trusted mechanised JavaScript specification Coq

34. A verified information-flow architecture Coq

35. CakeML: A verified implementation of ML HOL4

36. Probabilistic relational verification for cryptographic implementations Coq

37. Freeze after writing (Quasi-deterministic parallel programming with LVars) Haskell

38. Modular, higher-order cardinality analysis in theory and practice Haskell

39. Profiling for laziness Racket

40. Modular reasoning about heap paths via effectively propositional formulas SMT Z3

41. Monadic combinators for “putback” style bidirectional programming Haskell

42. The HERMIT in the stream (Fusing stream fusion’s concatMap) Haskell

43. Haskell applicative tutorial: a small tutorial, showing how you can use functors and applicatives Haskell

44. MuCheck : An extensible tool for mutation testing of Haskell programs Haskell

45. A DSL for describing the artificial intelligence in real-time video games Haskell

46. Shortcut fusion for pipes Haskell

47. La sucesión de Kolakoski Haskell

48. Verifying chinese train control system under a combined scenario by theorem proving Isabelle

49. Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5 Isabelle

50. La conjetura de Gilbreath en Haskell Haskell

51. Certifying algorithms Verificación

52. Codificación por longitud en Haskell Haskell

53. El triángulo de Pascal en Haskell Haskell

54. Lista de factoriales perezosa en Haskell Haskell

55. Sucesión de Fibonacci, evaluación perezosa y números construibles Haskell

56. Memorabilia Mathematica (or the philomath’s quotation-book) Libro

57. Codificación por longitud en Haskell Haskell

58. Two case studies in proving with side-effects: Gödel’s and Kripke’s completeness theorems Agda Coq

59. Fixing bugs in “Computing Homology” Python

60. Formal verification, interactive theorem proving, and automated reasoning Divulgación

61. Specification and verification of concurrent programs through refinements ACL2

62. A formally verified generic branching algorithm for global optimization PVS

63. Distributed call-by-value machines Agda

64. Twenty years of theorem proving for HOLs (Past, present and future) Historia

65. Clasificación supervisada y no supervisada IA AA

66. El juego de Oslo en Haskell Haskell

67. Inductive triple graphs: A purely functional approach to represent RDF Haskell Scala

68. Formalizing the Kleene star for square matrices Isabelle

69. Números triangulares y sus propiedades en Haskell Haskell

70. Mathematics in the age of the Turing machine Divulgación

71. Lecture notes on type theory Libro

72. A new type of Mathematics? New discoveries expand the scope of computer-assisted proofs of theorems Divulgación

73. Algorithms Libro Algorítmica

74. Balancing lists: a proof pearl. Isabelle

75. Bases de datos en grafo IA

Lecturas de Febrero de 2014

1. Alan Turing and the origins of complexity Historia

2. On Turing’s legacy in mathematical logic and the foundations of mathematics Historia

3. A survey of axiom selection as a machine learning problem Isabelle

4. Eilenberg-MacLane spaces in homotopy type theory Agda

5. Interactive SICP (Structure and Interpretation of Computer Programs) Libro Scheme

6. A heuristic prover for real inequalities AR

7. Arbitrary fun: Generating user profiles with QuickCheck Haskell QuickCheck

8. A little lens starter tutorial Haskell

9. Números poligonales y sus propiedades en Haskell Haskell

10. El triángulo de Floyd en Haskell. http://bit.ly/1nRULh Haskell

11. Solving a regular expression crossword with Haskell, Part 2: Representation. Haskell

12. Basics of λ-calculus LC

13. Verification of certifying computations through AutoCorres and Simpl Isabelle

14. Implementing, and understanding type classes Haskell

15. Survey of Satisfiability Modulo Theories (SMT) SAT SMT

16. OTTER proofs of theorems in Tarskian geometry OTTER

17. Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems SAT SMT

18. Laplace’s equation in Haskell: Using a DSL for stencils Haskell

19. A test driven haskell course Curso Haskell

20. Logic, languages and programming Haskell

21. New draft of Haskell School of Music (PDF) Libro Haskell

22. Properties of random graphs – subgraph containment. Isabelle

23. Monad transformers for backtracking search Haskell SAT

24. A survey of axiom selection as a machine learning problem. Isabelle

25. Proof-by-instance for embedded network design (From prototype to tool roadmap). Isabelle

26. A mathematical proof too long to check – The Erdos discrepancy conjecture SAT

27. Formalised mathematics Agda

28. Coinitial semantics for redecoration of triangular matrices. Coq

29. Rank nullity theorem of linear algebra Isabelle

30. A brief intro to QuickCheck Haskell QuickCheck

31. Complexity & verification: The history of programming as problem solving Tesis Historia

32. A denotational semantics for natural language query interfaces to semantic web triplestores Haskell

33. Learning-assisted theorem proving with millions of lemmas IA AR ML

34. Thesis: formal study of efficient algorithms in linear algebra Tesis Coq

35. A tutorial on using the Aeson packaged to parse JSON data Haskell

36. A tutorial on the attoparsec parsing package Haskell

37. Ejercicios sobre definiciones con unfoldr Haskell

38. Haskell: A whirlwind tour (Part 1) Haskell

39. Comprehensive formal verification of an OS microkernel Isabelle Haskell

40. A Cretan maze using Haskell Diagrams Haskell

41. Comparing Haskell Web frameworks Haskell

42. What is formalized Mathematics Divulgación

43. Random numbers in Haskell Haskell

44. Coin change Haskell

45. Simple examples. Haskell Haskell

46. Example of why to use monads – what they can do Haskell

47. Solution counting Haskell

48. Polynomials: Library for polynomials Haskell

49. Root finding Haskell

50. Simple interpolation Haskell

51. Infinite subsets of natural numbers Haskell

52. An introduction to QuickCheck testing Haskell

53. Shortest path: Floyd-Warshall algorithm in Haskell Haskell

54. Knapsack – Brute force in Haskell Haskell

55. Automated and (formally) certified proofs of summation formulae Coq

56. Induction and logical relations Agda

57. Problema de Ramanujan de radicales anidados. Haskell

58. Sucesiones auto descriptivas en Haskell. Haskell

59. Proof assistant based on didactic considerations. Enseñanza ANDY

60. A fully automatic problem solver with human-style output

61. Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. PVS

62. Formalizing Moessner’s theorem and generalizations in Nuprl. Nuprl

63. Preservation of Lyapunov-theoretic proofs: From real to floating-point arithmetic Coq

64. A mechanized proof of loop freedom of the (untimed) AODV routing protocol Isabelle

65. Showing invariance compositionally for a process algebra of network protocols Isabelle

Lecturas de Marzo de 2014

1. Interaction entre algèbre linéaire et analyse en formalisation des mathématiques Tesis Coq

2. A Haskell-implementation of STM Haskell with early conflict detection Haskell

3. Mutation testing of functional programming languages Haskell

4. Harnessing constraint programming for poetry composition ASP

5. Formalization of binary fields and n-dimensional binary vector spaces using the Mizar proof checker Mizar

6. Content development for distance education in advanced university mathematics using Mizar Mizar

7. Computers, maths and minds

8. Learning Agda to be a better Haskell programmer Haskell Agda

9. Learning Prolog to be a better Haskell programmer Haskell Prolog

10. Fun with functional dependencies (or (draft) types as values in static computations in Haskell) Haskell

11. Fun with type functions (version 3) Haskell

12. Data.Map vs Data.IntMap Haskell

13. Multi-line strings in Haskell Haskell

14. Data.Typeable and Data.Dynamic in Haskell Haskell

15. Implementing Union-Find algorithms in Haskell Haskell

16. Calling C library functions dynamically in Haskell Haskell

17. Implementing a JIT compiled language with Haskell and LLVM Haskell

18. Switching from monads to applicative functors Haskell

19. The power of lazy evaluation Haskell

20. How to replace failure by a list of successes Haskell

21. Using string literal for symbols Haskell

22. Parsing arithmetic expressions with Parsec Haskell

23. An ACL2 mechanization of an axiomatic weak memory model ACL2

24. From zipper to lens Haskell

25. Auto in Agda (Programming proof search) Agda

26. Introducción a las redes complejas IA

27. Lógica de enunciados Libro Lógica

28. Lógica de predicados Libro Lógica

29. Teoría de conjuntos básica (Conjuntos, relaciones y funciones) Libro Lógica

30. A brief introduction to Haskell, and why it matters Haskell

31. Haskell cheat sheets (Part 1) Haskell

32. Hspec: Behavior-driven development for Haskell Haskell BDD

33. Free applicative functors Haskell

34. Algebraic and analytic programming Haskell Math

35. Lógica y álgebra de Boole Libro Lógica

36. LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration Haskell

37. Transparencias del curso “Algoritmia básica” Algorítmica

38. Transparencias del curso “Algoritmia para problemas difíciles” Algorítmica

39. Formalizing and verifying a modern build language Coq

40. A hybrid TM for Haskell Haskell

41. Tiled polymorphic temporal media. (A functional pearl) Haskell

42. A seamless, client-centric programming model for type safe web applications Haskell

43. Defunctionalizing push arrays Haskell

44. Natural language reasoning using proof-assistant technology: Rich typing and beyond Coq

45. Intro to Haskell for Erlangers Haskell

46. Haskell for OCaml programmers Haskell OCaml

47. Programming and reasoning with side-effects in Idris Idris

48. Créatúr: Framework for artificial life and other evolutionary algorithms Haskell

49. Why Haskell is important for research, Part 1 of n Haskell

50. Programming with finite fields Python

51. Improving readability with the Maybe Foldable instance Haskell

52. Probabilistic noninterference Isabelle

53. Mechanization of the Algebra for Wireless Networks (AWN) Isabelle

54. Haskell for Coq programmers Haskell Coq

55. An introduction to recursion schemes and codata Haskell

56. Formal analysis of optical systems HOL_Light

57. Formally verified computation of enclosures of solutions of ordinary differential equations Isabelle

58. Verifying security policies using host attributes Isabelle

59. aspeed: Solver scheduling via Answer Set Programming ASP

60. A brief introduction to Haskell, and why it matters Haskell

61. Monoid morphisms, products, and coproducts Scala

62. Interactive tutorial of the sequent calculus Enseñanza

63. Bayesian analysis: A conjugate prior and Markov chain Monte Carlo Haskell

64. Cantor’s diagonal argument in Agda Agda

65. H2048: A Haskell implementation of game 2048 Haskell

66. Haskell in the browser: setting up Yesod and Fay Haskell

67. Presentation of Haskell in the Hackerspace Trento Haskell

68. Teach yourself logic: A study guide. Version 10.0 (20 March 2014 Libro

69. Haskell from C: Where are the for Loops Haskell

70. What’s wrong with the for loop Haskell

71. Why learn Haskell Haskell

72. Algorithme de Babylone : une boucle sous toutes ses formes Haskell

73. Discrétisation d’équations différentielles Haskell

74. Au delà des réels: méthodes numériques en informatique Haskell

75. Polynômes de Taylor: graphiques et animations Haskell

76. Méthode de Briggs et de Héron avec MPFR via Haskell et Sage Haskell Sage

77. Gauss par tête et queue Haskell

78. Z/nZ sans arithmétique modulaire … Haskell

79. Algèbre et informatique Haskell

80. Programmation fonctionnelle et Haskell for dummies Haskell

81. Relations binaires et fonctions avec Haskell Haskell

82. Poker en Haskell Haskell

83. Logique des propositions en Haskell part I Haskell

84. Mathématique discrète et informatique Libro Haskell

85. Calcul mathématique avec Sage Libro Sage

86. The power algorithm Haskell PHP

87. Modeling and verification of distributed algorithms in theorem proving environments Isabelle

88. Directed security policies: A stateful network implementation Isabelle

89. John McCarthy – Father of Artificial Intelligence Historia

90. What it’s like to use Haskell Haskell

91. Résolution dichotomique de f(x)=0 Haskell

92. Colección de problemas sobre inteligencia artificial Libro IA

93. Monaris: A tetris clone written in Haskell using free-game Haskell

94. Formal proof of the fundamental theorem of decorated interval arithmetic Tesis Coq

95. Library to calculate Gröbner basis written in Haskell Haskell

96. Introduction à l’algorithmique et à la programmation avec Python Python

97. Algorithmic problem solving with Python Libro Python

98. Computational discrete mathematics with Python Libro Python

99. Formally verified mathematics Divulgación

100. Towards a formally verified proof assistant Coq Nuprl

101. Formalization of a dynamic logic for graph transformation in the Coq proof assistant Coq

102. Interactive simplifier tracing and debugging in Isabelle Isabelle

Una recopilación de todas las lecturas se encuentra aquí.