Lecturas del año 2014

De WikiGLC
Revisión del 17:19 30 mar 2014 de Jalonso (discusión | contribuciones)
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)
Saltar a: navegación, buscar

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