Lecturas del año 2014

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

• The power algorithm Haskell PHP

1. Modeling and verification of distributed algorithms in theorem proving environments Isabelle
2. Directed security policies: A stateful network implementation Isabelle
3. John McCarthy – Father of Artificial Intelligence Historia
4. What it’s like to use Haskell Haskell
5. Brutal [metaintroduction to dependent types in Agda] Agda

• Estructurando y consultando información en grafos. ~ Fernando Sancho http://bit.ly/1g1y6It Grafos Redes_complejas

1. Résolution dichotomique de f(x)=0 Haskell
2. Colección de problemas sobre inteligencia artificial Libro IA
3. Monaris: A tetris clone written in Haskell using free-game Haskell
4. Formal proof of the fundamental theorem of decorated interval arithmetic Tesis Coq
5. Library to calculate Gröbner basis written in Haskell Haskell
6. Introduction à l’algorithmique et à la programmation avec Python Python
7. Algorithmic problem solving with Python Libro Python
8. Computational discrete mathematics with Python Libro Python
9. Formally verified mathematics Divulgación
10. Towards a formally verified proof assistant Coq Nuprl
11. Formalization of a dynamic logic for graph transformation in the Coq proof assistant Coq
12. Interactive simplifier tracing and debugging in Isabelle Isabelle