{"id":4226,"date":"2014-03-30T19:32:50","date_gmt":"2014-03-30T17:32:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4226"},"modified":"2014-03-30T21:28:34","modified_gmt":"2014-03-30T19:28:34","slug":"lecturas-del-grupo-de-logica-computacional-de-julio-de-2013-a-marzo-de-2014","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-del-grupo-de-logica-computacional-de-julio-de-2013-a-marzo-de-2014\/","title":{"rendered":"Lecturas del Grupo de L\u00f3gica Computacional (de julio de 2013 a marzo de 2014)"},"content":{"rendered":"

Esta entrada es una recopilaci\u00f3n de lecturas compartidas en la lista de correo del grupo de l\u00f3gica computacional<\/a> o en mi p\u00e1gina de twitter<\/a> desde la anterior recopilaci\u00f3n<\/a>.<\/p>\n

La recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista o en twitter. Al final de cada art\u00edculo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n

<\/p>\n

Lecturas de Julio de 2013<\/h3>\n
    \n
  1. \n

    Automated proof checking in introductory discrete mathematics classes<\/a>. ITP Coq<\/p>\n<\/li>\n

  2. \n

    On the formal verification of Maple programs<\/a>. Maple Why3<\/p>\n<\/li>\n

  3. \n

    N.G. de Bruijn\u2019s contribution to the formalization of mathematics<\/a>.<\/p>\n<\/li>\n

  4. \n

    Towards certified program logics for the verification of imperative programs<\/a>. Tesis Coq<\/p>\n<\/li>\n

  5. \n

    Bishop-style constructive mathematics in type theory – a tutorial<\/a>.<\/p>\n<\/li>\n

  6. \n

    Proof of impossibility<\/a>.<\/p>\n<\/li>\n

  7. \n

    Why the world needs Haskell<\/a>. Haskell<\/p>\n<\/li>\n

  8. \n

    SMT theory and DPLL(T)<\/a>. SMT<\/p>\n<\/li>\n

  9. \n

    I\/O is pure<\/a>. Haskell<\/p>\n<\/li>\n

  10. \n

    G\u00f6del\u2019s incompleteness theorems formally verified<\/a>. Isabelle<\/p>\n<\/li>\n

  11. \n

    Functoriality<\/a>. ML<\/p>\n<\/li>\n

  12. \n

    Dependent types for an adequate programming of algebra<\/a>. Haskell Agda<\/p>\n<\/li>\n

  13. \n

    Reading an algebra textbook<\/a>. Isabelle<\/p>\n<\/li>\n

  14. \n

    Computer algebra implemented in Isabelle\u2019s function package under Lucas-interpretation: a case study<\/a>. Isabelle<\/p>\n<\/li>\n

  15. \n

    Lurch: a word processor that can grade students\u2019 proofs<\/a>. Lurch<\/p>\n<\/li>\n

  16. \n

    Theorem proving in large formal mathematics as an emerging AI field<\/a>. ATP<\/p>\n<\/li>\n

  17. \n

    What, if anything, is a declarative language<\/a>. PD<\/p>\n<\/li>\n

  18. \n

    Proof pearl: A verified bignum implementation in x86-64 machine code<\/a>. HOL4<\/p>\n<\/li>\n

  19. \n

    Desaf\u00edos y oportunidades de la investigaci\u00f3n en m\u00e9todos formales<\/a>. MF<\/p>\n<\/li>\n

  20. \n

    Proofs you can believe in: Proving equivalences between Prolog semantics in Coq<\/a>. Coq Prolog<\/p>\n<\/li>\n

  21. \n

    El uso de los demostradores autom\u00e1ticos de teoremas para la ense\u00f1anza de la programaci\u00f3n<\/a> Krakatoa<\/p>\n<\/li>\n

  22. \n

    Tackling Fibonacci words puzzles by finite countermodels<\/a> Mace4<\/p>\n<\/li>\n

  23. \n

    Parallel and concurrent programming in Haskell<\/a> Haskell<\/p>\n<\/li>\n

  24. \n

    Analizadores sint\u00e1cticos funcionales<\/a> Haskell<\/p>\n<\/li>\n

  25. \n

    A taste of the \u03bb calculus<\/a> LC<\/p>\n<\/li>\n

  26. \n

    Course: Functional problem solving<\/a> Scheme Racket<\/p>\n<\/li>\n

  27. \n

    A short tutorial on the internals of a theorem prover<\/a> ZOL<\/p>\n<\/li>\n

  28. \n

    El lenguaje Python<\/a> Libro Phyton<\/p>\n<\/li>\n

  29. \n

    Inteligencia artificial avanzada<\/a> Libro IA<\/p>\n<\/li>\n

  30. \n

    Program verification based on Kleene algebra in Isabelle\/HOL<\/a> Isabelle<\/p>\n<\/li>\n

  31. \n

    Ordinals in HOL: Transfinite arithmetic up to (and beyond) \u03c9\u2081<\/a> HOL4<\/p>\n<\/li>\n

  32. \n

    Exploiting vector instructions with generalized stream fusion<\/a> Haskell<\/p>\n<\/li>\n

  33. \n

    IsarMathLib (A library of formalized mathematics for Isabelle\/ZF theorem proving environment) 1.9.0 released<\/a> Isabelle<\/p>\n<\/li>\n

  34. \n

    Course: \u201cFunctional programming I\u201d<\/a> Curso PF SML<\/p>\n<\/li>\n

  35. \n

    Re-proving theorems, and the trouble with incorrect proofs of true statements<\/a> Filosof\u00eda<\/p>\n<\/li>\n

  36. \n

    Measuring the Haskell gap<\/a> Haskell<\/p>\n<\/li>\n

  37. \n

    Why Haskell at school matters<\/a> Haskell<\/p>\n<\/li>\n

  38. \n

    Course: Introduction to Haskell<\/a> Curso Haskell<\/p>\n<\/li>\n

  39. \n

    Pratt\u2019s primality certificates<\/a> Isabelle<\/p>\n<\/li>\n

  40. \n

    Automatic SIMD vectorization for Haskell<\/a> Haskell<\/p>\n<\/li>\n

  41. \n

    Reflections on \u201cA computationally-discovered simplification of the ontological argument<\/a> Prover9<\/p>\n<\/li>\n

  42. \n

    Computational verification of network programs in Coq<\/a>. Coq<\/p>\n<\/li>\n

  43. \n

    El uso de los demostradores autom\u00e1ticos de teoremas para la ense\u00f1anza de la programaci\u00f3n<\/a>. Krakatoa<\/p>\n<\/li>\n

  44. \n

    Program verification based on Kleene algebra in Isabelle\/HOL<\/a>. Isabelle<\/p>\n<\/li>\n

  45. \n

    Ordinals in HOL: Transfinite arithmetic up to (and beyond) \u03c9\u2081<\/a>. HOL4<\/p>\n<\/li>\n

  46. \n

    Certified, efficient and sharp univariate Taylor models in Coq<\/a>. Coq<\/p>\n<\/li>\n

  47. \n

    Proofs you can believe in: Proving equivalences between Prolog semantics in Coq<\/a>. Coq<\/p>\n<\/li>\n<\/ol>\n

    Lecturas de Agosto de 2013<\/h3>\n
      \n
    1. \n

      A tutorial on the universality and expressiveness of fold<\/a> Haskell<\/p>\n<\/li>\n

    2. \n

      Matem\u00e1tica discreta y \u00e1lgebra Lineal<\/a> Libro Maxima<\/p>\n<\/li>\n

    3. \n

      Discrete mathematics and functional programming<\/a> Libro ML<\/p>\n<\/li>\n

    4. \n

      Programming in Martin-L\u00f6f\u2019s type theory (an introduction)<\/a> Libro<\/p>\n<\/li>\n

    5. \n

      A silent revolution in mathematics (The rise of applications, numerical methods, and computational approaches)<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

    6. \n

      Type inference, Haskell and dependent types<\/a> Tesis Haskell<\/p>\n<\/li>\n

    7. \n

      A quick tour of Haskell syntax<\/a> Haskell<\/p>\n<\/li>\n

    8. \n

      Unifying structured recursion schemes<\/a> Haskell<\/p>\n<\/li>\n

    9. \n

      GPU programming in functional languages (A comparison of Haskell GPU embedded domain specific languages)<\/a> Haskell<\/p>\n<\/li>\n

    10. \n

      Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar<\/a> Mizar<\/p>\n<\/li>\n

    11. \n

      Generalising monads to arrows<\/a> Haskell<\/p>\n<\/li>\n

    12. \n

      Reasoning about higher-order relational specifications<\/a>. Abella<\/p>\n<\/li>\n

    13. \n

      Probabilistic programming & bayesian methods for hackers<\/a> IA Python<\/p>\n<\/li>\n

    14. \n

      Ex\u00e1menes de programaci\u00f3n funcional con Haskell<\/a> Libro Haskell<\/p>\n<\/li>\n

    15. \n

      Pratt\u2019s primality certificates<\/a>. Isabelle<\/p>\n<\/li>\n

    16. \n

      Formal verification of a proof procedure for the description logic ALC<\/a>. Isabelle<\/p>\n<\/li>\n

    17. \n

      The K\u00f6nigsberg bridge problem and the friendship theorem<\/a>. Isabelle<\/p>\n<\/li>\n

    18. \n

      Formalization of basic linear algebra<\/a>. Tesis Isabelle<\/p>\n<\/li>\n

    19. \n

      A computer-assisted proof of correctness of a marching cubes algorithm<\/a> Coq<\/p>\n<\/li>\n

    20. \n

      Why Lisp is a big hack (and Haskell is doomed to succeed)<\/a> Haskell Lisp<\/p>\n<\/li>\n

    21. \n

      Proof-pattern recognition in ACL2<\/a> ACL2 ML<\/p>\n<\/li>\n

    22. \n

      Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm<\/a>. ACL2<\/p>\n<\/li>\n

    23. \n

      A computer-assisted proof of correctness of a marching cubes algorithm<\/a> Coq<\/p>\n<\/li>\n

    24. \n

      Proving soundness of combinatorial Vickrey auctions and generating verified executable code<\/a>. Isabelle<\/p>\n<\/li>\n

    25. \n

      20 famous software disasters<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

    26. \n

      On writing proofs<\/a> Ense\u00f1anza<\/p>\n<\/li>\n

    27. \n

      Matem\u00e1tica discreta<\/a> Libro<\/p>\n<\/li>\n

    28. \n

      Mechanized metatheory for a \u03bb \u03bb-calculus with trust types<\/a>. Coq<\/p>\n<\/li>\n

    29. \n

      Proof pearl: A verified bignum implementation in x86-64 machine code<\/a>. HOL4<\/p>\n<\/li>\n

    30. \n

      Two monoids for approximating NP-complete problems<\/a> Haskell<\/p>\n<\/li>\n

    31. \n

      Automated mathematics<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

    32. \n

      The Lisp bookshelf<\/a> Lisp<\/p>\n<\/li>\n

    33. \n

      Counting lattice paths<\/a> Lisp<\/p>\n<\/li>\n

    34. \n

      Binary search & Newton-Raphson root finding<\/a> Lisp<\/p>\n<\/li>\n

    35. \n

      La L\u00f3gica en las ciencias computacionales<\/a> Ense\u00f1anza<\/p>\n<\/li>\n

    36. \n

      Generic datatypes \u00e0 la carte<\/a>. Coq<\/p>\n<\/li>\n

    37. \n

      Introducci\u00f3n al c\u00e1lculo simb\u00f3lico con Maxima<\/a>. Maxima<\/p>\n<\/li>\n

    38. \n

      Husk \u03bb scheme: A dialect of R5RS Scheme written in Haskell<\/a> Haskell Scheme<\/p>\n<\/li>\n

    39. \n

      Los n\u00fameros de Ulam en Haskell<\/a> Haskell<\/p>\n<\/li>\n

    40. \n

      Introducci\u00f3n a la teor\u00eda de n\u00fameros: ejemplos y algoritmos<\/a> Libro<\/p>\n<\/li>\n

    41. \n

      Do extraterrestrials use functional programming<\/a> Haskell<\/p>\n<\/li>\n

    42. \n

      The bowling game kata in functional common lisp<\/a> Lisp<\/p>\n<\/li>\n

    43. \n

      Cellular automata<\/a> Haskell<\/p>\n<\/li>\n

    44. \n

      Introducci\u00f3n a la demostraci\u00f3n asistida por ordenador con Isabelle\/HOL<\/a> Libro Isabelle<\/p>\n<\/li>\n

    45. \n

      Steps towards verified implementations of HOL Light<\/a>. Hol_Light<\/p>\n<\/li>\n

    46. \n

      Functional flocks<\/a> Vida_artificial Haskell Gloss<\/p>\n<\/li>\n

    47. \n

      Course: Advanced functional programming<\/a> Curso Haskell<\/p>\n<\/li>\n

    48. \n

      The programming language zoo<\/a> OCaml<\/p>\n<\/li>\n

    49. \n

      Planetary simulation with excursions in symplectic manifolds<\/a> Haskell<\/p>\n<\/li>\n

    50. \n

      Computational category theory<\/a> ML<\/p>\n<\/li>\n

    51. \n

      Pretext by experiments and guesses<\/a> Haskell<\/p>\n<\/li>\n

    52. \n

      Hacq: A circuit description language for quantum circuits<\/a> Haskell<\/p>\n<\/li>\n

    53. \n

      Lenses from scratch<\/a> Haskell<\/p>\n<\/li>\n

    54. \n

      Comparing Python and Haskell<\/a> Haskell Python<\/p>\n<\/li>\n

    55. \n

      Lens\/Aeson traversals\/prisms<\/a> Haskell<\/p>\n<\/li>\n

    56. \n

      An introduction to language processing<\/a> Haskell<\/p>\n<\/li>\n<\/ol>\n

      Lecturas de Septiembre de 2013<\/h3>\n
        \n
      1. \n

        Call-by-need supercompilation<\/a> Tesis Haskell<\/p>\n<\/li>\n

      2. \n

        Controlling Chromium in Haskell<\/a> Haskell<\/p>\n<\/li>\n

      3. \n

        A 10 minute tutorial for solving Math problems with Maxima<\/a> Maxima<\/p>\n<\/li>\n

      4. \n

        The nature of code<\/a> Libro<\/p>\n<\/li>\n

      5. \n

        A mechanised proof of G\u00f6del\u2019s incompleteness theorems using Nominal Isabelle<\/a>. Isabelle<\/p>\n<\/li>\n

      6. \n

        Computational logic and the quest for greater automation<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

      7. \n

        Supercompiling Haskell to hardware<\/a> Haskell<\/p>\n<\/li>\n

      8. \n

        Cellular automata. Part II: PNGs and Moore in Haskell<\/a> Haskell<\/p>\n<\/li>\n

      9. \n

        ML-TID: A type inference debugger for ML in education<\/a> ML Educaci\u00f3n<\/p>\n<\/li>\n

      10. \n

        Polygonal numbers<\/a>. Mizar<\/p>\n<\/li>\n

      11. \n

        Formal verification of cryptographic security proofs<\/a>. Tesis Isabelle<\/p>\n<\/li>\n

      12. \n

        A TCAS-II resolution advisory algorithm<\/a>. PVS<\/p>\n<\/li>\n

      13. \n

        N\u00fameros y hoja de c\u00e1lculo V<\/a> Libro<\/p>\n<\/li>\n

      14. \n

        A duality of sorts<\/a> Haskell<\/p>\n<\/li>\n

      15. \n

        Learn Common Lisp in Y minutes<\/a> Lisp<\/p>\n<\/li>\n

      16. \n

        An introduction to functional programming<\/a> PF Haskell Erlang Clojure Scala OCaml<\/p>\n<\/li>\n

      17. \n

        Formal verification of language-based concurrent noninterference<\/a>. Isabelle<\/p>\n<\/li>\n

      18. \n

        Advanced functional programming for fun and profit<\/a> Haskell<\/p>\n<\/li>\n

      19. \n

        Mathematical logic for mathematicians, Part I<\/a> Libro<\/p>\n<\/li>\n

      20. \n

        Sobre la Inteligencia Artificial<\/a> IA<\/p>\n<\/li>\n

      21. \n

        Quark: A web browser with a formally verified kernel<\/a> Coq<\/p>\n<\/li>\n

      22. \n

        Computer theorem proving and HoTT<\/a>. HoTT<\/p>\n<\/li>\n

      23. \n

        From Tarski to Hilbert<\/a>. Coq<\/p>\n<\/li>\n

      24. \n

        Conquering folds<\/a> Haskell<\/p>\n<\/li>\n

      25. \n

        Catamorphisms (generalizations of the concept of a fold in functional programming)<\/a> Haskell<\/p>\n<\/li>\n

      26. \n

        On-line lowest common ancestor<\/a> Haskell<\/p>\n<\/li>\n

      27. \n

        Generation of labelled transition systems for Alvis models using Haskell model representation<\/a> Haskell<\/p>\n<\/li>\n

      28. \n

        Modeling uncertain data using monads and an application to the sequence alignment problem<\/a> Haskell<\/p>\n<\/li>\n

      29. \n

        El problema de las sucesiones llenas en Haskell<\/a> Haskell<\/p>\n<\/li>\n

      30. \n

        Theory exploration for interactive theorem proving<\/a>. Isabelle HipSpec Haskell<\/p>\n<\/li>\n

      31. \n

        Combining memoisation and change propagation for automatic incremental evaluation of Haskell arrow programs<\/a> Tesis Haskell<\/p>\n<\/li>\n

      32. \n

        Extensible effects: An alternative to monad transformers<\/a> Haskell<\/p>\n<\/li>\n

      33. \n

        System FC with explicit kind equality<\/a> Haskell<\/p>\n<\/li>\n

      34. \n

        Causality of optimized Haskell: What is burning our cycles<\/a> Haskell<\/p>\n<\/li>\n

      35. \n

        Using circular programs for higher-order syntax: Functional pearl<\/a> Haskell<\/p>\n<\/li>\n

      36. \n

        Fun with semirings: A functional pearl on the abuse of linear algebra<\/a> Haskell<\/p>\n<\/li>\n

      37. \n

        MagicHaskeller on the Web: Automated programming as a service<\/a> Haskell<\/p>\n<\/li>\n

      38. \n

        Random testing of purely functional abstract datatypes<\/a> Haskell<\/p>\n<\/li>\n

      39. \n

        Data parallelism in Haskell<\/a> Haskell<\/p>\n<\/li>\n

      40. \n

        Computational mathematics in the cloud with Sagemath<\/a> Sage<\/p>\n<\/li>\n

      41. \n

        Sistemas multiagente y simulaci\u00f3n<\/a> IA<\/p>\n<\/li>\n

      42. \n

        A dictionary for reading proofs<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

      43. \n

        Mathematical logic (Lecture notes)<\/a> Libro<\/p>\n<\/li>\n

      44. \n

        Basic lensing<\/a> Haskell<\/p>\n<\/li>\n

      45. \n

        Automation of mathematical induction as part of the history of logic<\/a> Historia<\/p>\n<\/li>\n

      46. \n

        The future role of computers in mathematics<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

      47. \n

        Some example MVar, IVar, and LVar programs in Haskell<\/a> Haskell<\/p>\n<\/li>\n

      48. \n

        Revisiting examples of computer assisted mathematics<\/a> Sage<\/p>\n<\/li>\n<\/ol>\n

        Lecturas de Octubre de 2013<\/h3>\n
          \n
        1. \n

          Formalizing Moessner\u2019s theorem and generalizations in Nuprl<\/a> Nuprl<\/p>\n<\/li>\n

        2. \n

          Clojure\u2019s core.typed vs Haskell<\/a> Clojure Haskell<\/p>\n<\/li>\n

        3. \n

          The ontological argument in PVS<\/a>. PVS<\/p>\n<\/li>\n

        4. \n

          Zippers and comonads in Haskell<\/a> Haskell<\/p>\n<\/li>\n

        5. \n

          Voevodsky\u2019s mathematical revolution<\/a> HoTT<\/p>\n<\/li>\n

        6. \n

          Quantum artificial intelligence: A survey of application of quantum physics in artificial intelligence<\/a> IA<\/p>\n<\/li>\n

        7. \n

          An abstract description method of Map-Reduce-Merge using Haskell<\/a> Haskell<\/p>\n<\/li>\n

        8. \n

          Functional programming in Scheme (With Web programming examples)<\/a> Scheme<\/p>\n<\/li>\n

        9. \n

          A formal model and correctness proof for an access control policy framework<\/a>. Isabelle<\/p>\n<\/li>\n

        10. \n

          Verified AIG algorithms in ACL2<\/a>. ACL2<\/p>\n<\/li>\n

        11. \n

          Programaci\u00f3n, ni\u00f1os y escuelas: el reto del momento<\/a> Ense\u00f1anza<\/p>\n<\/li>\n

        12. \n

          Forget foreign languages and music. Teach our kids to code<\/a> Ense\u00f1anza<\/p>\n<\/li>\n

        13. \n

          Coin change<\/a> Haskell<\/p>\n<\/li>\n

        14. \n

          An all-atom protein search engine powered by Haskell<\/a> Haskell<\/p>\n<\/li>\n

        15. \n

          A little lens starter tutorial<\/a> Haskell<\/p>\n<\/li>\n

        16. \n

          Introduction to Agda<\/a> Agda<\/p>\n<\/li>\n

        17. \n

          Proving correctness of compilers using structured graphs<\/a> Haskell<\/p>\n<\/li>\n

        18. \n

          Haskell\/concurrency braindump<\/a> Haskell<\/p>\n<\/li>\n

        19. \n

          Sorting and searching by distribution: From generic discrimination to generic tries<\/a> Haskell<\/p>\n<\/li>\n

        20. \n

          A gentle introduction to Parsec<\/a> Haskell<\/p>\n<\/li>\n

        21. \n

          Haskell optimization and the game of life<\/a> Haskell<\/p>\n<\/li>\n

        22. \n

          Beautiful code, compelling evidence<\/a> Libro Haskell<\/p>\n<\/li>\n

        23. \n

          Course: Language-oriented programming<\/a> Lisp<\/p>\n<\/li>\n<\/ol>\n

          Lecturas de Noviembre de 2013<\/h3>\n
            \n
          1. \n

            Trimming while checking clausal proofs<\/a> SAT<\/p>\n<\/li>\n

          2. \n

            Efficiently computing Kendall\u2019s tau<\/a> Clojure<\/p>\n<\/li>\n

          3. \n

            Lambda calculus<\/a> LC<\/p>\n<\/li>\n

          4. \n

            Modular monadic meta-theory<\/a> Coq<\/p>\n<\/li>\n

          5. \n

            Operational semantics of Ltac (A formal study of the tactic language of the Coq proof assistant)<\/a> Coq<\/p>\n<\/li>\n

          6. \n

            Solving sudoku in Racket<\/a> Racket<\/p>\n<\/li>\n

          7. \n

            Teaching induction with functional programming and a proof assistant<\/a> Educaci\u00f3n<\/p>\n<\/li>\n

          8. \n

            A machine-assisted proof of G\u00f6del\u2019s incompleteness theorems for the theory of hereditarily finite sets<\/a>. Isabelle<\/p>\n<\/li>\n

          9. \n

            Proof verification within set theory<\/a><\/p>\n<\/li>\n

          10. \n

            A Description Logics Tableau Reasoner in Prolog<\/a> Prolog<\/p>\n<\/li>\n

          11. \n

            Nested sequent calculi and theorem proving for normal conditional logics<\/a> Prolog<\/p>\n<\/li>\n

          12. \n

            Martin-L\u00f6f and an introduction to Agda<\/a> Agda<\/p>\n<\/li>\n

          13. \n

            The social machine of mathematics<\/a> Filosof\u00eda<\/p>\n<\/li>\n

          14. \n

            Applications of real number theorem proving in PVS<\/a>. PVS<\/p>\n<\/li>\n

          15. \n

            plaimi\u2019s introduction to Haskell for the Haskell-curious game programmer<\/a> Haskell<\/p>\n<\/li>\n

          16. \n

            Qualitative modelling of biological signalling pathways using SAT-solving in Prolog<\/a> Prolog<\/p>\n<\/li>\n

          17. \n

            An introduction to program verification with the Coq proof assistant<\/a> Coq<\/p>\n<\/li>\n

          18. \n

            Real world OCaml: Functional programming for the masses<\/a> Libro OCaml<\/p>\n<\/li>\n

          19. \n

            Formalizing NIST cryptographic standards<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

          20. \n

            Partial type signatures for Haskell<\/a> Haskell<\/p>\n<\/li>\n

          21. \n

            A survey of security research for operating systems<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

          22. \n

            Haskell, the language most likely to change the way you think about programming<\/a> Haskell<\/p>\n<\/li>\n

          23. \n

            Haskell fast & hard<\/a> Haskell Tutorial<\/p>\n<\/li>\n

          24. \n

            Philosophy of computer science<\/a> Libro<\/p>\n<\/li>\n

          25. \n

            Improving performance of simulation software using Haskell\u2019s concurrency & parallelism<\/a> Haskell<\/p>\n<\/li>\n

          26. \n

            List of long proofs: a list of unusually long mathematical proofs<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

          27. \n

            Cryptographic protocols formal and computational proofs<\/a> Verificaci\u00f3n<\/p>\n<\/li>\n

          28. \n

            Test stream programming using Haskell\u2019s \u2018QuickCheck\u2019<\/a> Haskell<\/p>\n<\/li>\n

          29. \n

            Real world OCaml: Functional programming for the masses<\/a> Libro OCaml<\/p>\n<\/li>\n

          30. \n

            HaskinTeX: A program to evaluate Haskell code within LaTeX<\/a> Haskell<\/p>\n<\/li>\n

          31. \n

            Sucesi\u00f3n con radicales en Haskell<\/a> Haskell<\/p>\n<\/li>\n

          32. \n

            Profiling for laziness<\/a><\/p>\n<\/li>\n

          33. \n

            Leaking space (Eliminating memory hogs)<\/a> Haskell<\/p>\n<\/li>\n

          34. \n

            The hereditarily finite sets<\/a>. Isabelle<\/p>\n<\/li>\n

          35. \n

            G\u00f6del\u2019s incompleteness theorems<\/a>. Isabelle<\/p>\n<\/li>\n

          36. \n

            Functional programming for domain-specific languages<\/a> Haskell<\/p>\n<\/li>\n

          37. \n

            Applying formal methods to networking: Theory, techniques and applications<\/a> MF<\/p>\n<\/li>\n

          38. \n

            Compiling DNA strand displacement reactions using a functional programming language<\/a> ML<\/p>\n<\/li>\n

          39. \n

            Recovering intuition from automated formal proofs using tableaux with superdeduction<\/a> AR<\/p>\n<\/li>\n

          40. \n

            A graph library for Isabelle<\/a>. Isabelle<\/p>\n<\/li>\n

          41. \n

            Experience report: The next 600 Haskell programmers<\/a> Haskell<\/p>\n<\/li>\n

          42. \n

            Ensino de L\u00f3gica atrav\u00e9s de estrat\u00e9gias de demonstra\u00e7\u00e3o e refuta\u00e7\u00e3o<\/a> Educaci\u00f3n<\/p>\n<\/li>\n

          43. \n

            Sistemas complejos, sistemas din\u00e1micos y redes complejas<\/a> IA<\/p>\n<\/li>\n

          44. \n

            Sistemas complejos, caos y vida artificial<\/a> IA<\/p>\n<\/li>\n

          45. \n

            hPDB-Haskell library for processing atomic biomolecular structures in Protein Data Bank format<\/a> Haskell<\/p>\n<\/li>\n

          46. \n

            Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem<\/a>. Isabelle<\/p>\n<\/li>\n

          47. \n

            Haskell as an introduction to parallel computing for undergraduates<\/a> Haskell<\/p>\n<\/li>\n

          48. \n

            Algoritmos gen\u00e9ticos y computaci\u00f3n evolutiva<\/a> IA<\/p>\n<\/li>\n

          49. \n

            Sistemas colectivos. Inteligencia colectiva<\/a> IA<\/p>\n<\/li>\n

          50. \n

            Aut\u00f3matas celulares<\/a> IA<\/p>\n<\/li>\n<\/ol>\n

            Lecturas de Diciembre de 2013<\/h3>\n
              \n
            1. \n

              Formal modeling and verification of multi-agent system architecture<\/a>. PVS<\/p>\n<\/li>\n

            2. \n

              SICP (Structure and Interpretation of Computer Programs) in Clojure<\/a> Clojure<\/p>\n<\/li>\n

            3. \n

              Certified Kruskal\u2019s tree theorem<\/a>. Isabelle<\/p>\n<\/li>\n

            4. \n

              Category theory for scientists<\/a> Curso<\/p>\n<\/li>\n

            5. \n

              CTFP13: Category theory and functional programming 2013<\/a> Curso PF<\/p>\n<\/li>\n

            6. \n

              Program design by calculation<\/a> Libro<\/p>\n<\/li>\n

            7. \n

              Implementation of a library for declarative, resolution-independent 2D graphics in Haskell<\/a> Haskell<\/p>\n<\/li>\n

            8. \n

              Functioning hardware from functional programs<\/a> Haskell<\/p>\n<\/li>\n

            9. \n

              Refinements for free!<\/a>. Coq<\/p>\n<\/li>\n

            10. \n

              Knowledge representation, reasoning, and the design of intelligent agents<\/a> Libro IA Prolog<\/p>\n<\/li>\n

            11. \n

              Formalizing probabilistic noninterference<\/a>. Isabelle<\/p>\n<\/li>\n

            12. \n

              Concrete semantics (A proof assistant approach)<\/a> Libro Isabelle<\/p>\n<\/li>\n

            13. \n

              Functional programming<\/a> Haskell<\/p>\n<\/li>\n

            14. \n

              Aliasing restrictions of C11 formalized in Coq<\/a>. Coq<\/p>\n<\/li>\n

            15. \n

              Trustworthy embedded systems: formal, code-level proofs for systems over 1 million lines of code<\/a> Isabelle Haskell<\/p>\n<\/li>\n

            16. \n

              The L4.verified project: A formally correct operating system kernel<\/a> Isabelle Haskell<\/p>\n<\/li>\n

            17. \n

              Applications of interactive proof to data flow analysis and security<\/a>. Isabelle<\/p>\n<\/li>\n

            18. \n

              First-order logic completeness for the lazy programmer<\/a>. Isabelle<\/p>\n<\/li>\n

            19. \n

              Popularizing Haskell through easy web deployment<\/a> Haskell<\/p>\n<\/li>\n

            20. \n

              \u00c0 la crois\u00e9e des fondements des math\u00e9matiques, de l\u2019informatique et de la topologie. (Th\u00e9orie homotopique des types)<\/a> HoTT<\/p>\n<\/li>\n

            21. \n

              Haskell, Ising, Markov & Metropolis<\/a> Haskell<\/p>\n<\/li>\n

            22. \n

              A domain-specific language for discrete mathematics<\/a> Haskell<\/p>\n<\/li>\n

            23. \n

              Using Isabelle\/HOL to verify first-order relativity theory<\/a>. Isabelle<\/p>\n<\/li>\n

            24. \n

              Homotopy type theory and univalent foundations<\/a> HoTT<\/p>\n<\/li>\n

            25. \n

              An introduction to Homotopy Type Theory<\/a> HoTT<\/p>\n<\/li>\n

            26. \n

              Querying an existing database<\/a> Haskell<\/p>\n<\/li>\n

            27. \n

              Moessner\u2019s theorem: an exercise in coinductive reasoning in Coq<\/a>. Coq<\/p>\n<\/li>\n

            28. \n

              Mechanical verification of parameterized real-time systems<\/a>. Isabelle<\/p>\n<\/li>\n

            29. \n

              Fun with PolyKinds – PolyKinded folds<\/a> Haskell<\/p>\n<\/li>\n

            30. \n

              An application of Answer Set Programming to the field of second language acquisition<\/a> ASP Prolog<\/p>\n<\/li>\n

            31. \n

              Certified programming with dependent types. (December 5, 2013)<\/a> Libro Coq<\/p>\n<\/li>\n

            32. \n

              Course: Foundations of program analysis<\/a> Haskell Coq<\/p>\n<\/li>\n

            33. \n

              Common pitfalls of functional programming and how to avoid them: A mobile gaming platform case study<\/a> Haskell<\/p>\n<\/li>\n

            34. \n

              The space-saving algorithm in Haskell<\/a> Haskell<\/p>\n<\/li>\n

            35. \n

              An IP microscope in Haskell<\/a> Haskell<\/p>\n<\/li>\n

            36. \n

              Simple unique IP system script<\/a> Haskell<\/p>\n<\/li>\n

            37. \n

              10 ways to incorporate Haskell into a modern, functional, CS curriculum<\/a> Haskell<\/p>\n<\/li>\n

            38. \n

              Why functional programming matters<\/a> Haskell<\/p>\n<\/li>\n

            39. \n

              Reliable massively parallel symbolic computing: Fault tolerance for a distributed Haskell<\/a> Tesis Haskell<\/p>\n<\/li>\n

            40. \n

              Structural induction principles for functional programmers<\/a>. Haskell<\/p>\n<\/li>\n

            41. \n

              Linked data, logic programming and black risotto<\/a> Prolog<\/p>\n<\/li>\n

            42. \n

              Ex\u00e1menes de programaci\u00f3n funcional con Haskell (2009-2014)<\/a>. Haskell<\/p>\n<\/li>\n

            43. \n

              Introduction to Haskell<\/a> Haskell<\/p>\n<\/li>\n

            44. \n

              Data is evidence<\/a> Haskell<\/p>\n<\/li>\n

            45. \n

              Misfortunes of a mathematicians\u2019 trio using Computer Algebra Systems: Can we trust<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

            46. \n

              Artificial intelligence: The machines with alien minds<\/a> IA<\/p>\n<\/li>\n

            47. \n

              An exercise on streams: convergence acceleration<\/a> Haskell<\/p>\n<\/li>\n

            48. \n

              A functional approach to standard binary heaps<\/a> Scala<\/p>\n<\/li>\n

            49. \n

              Computabilidad, complejidad computacional y verificaci\u00f3n de programas<\/a> Libro<\/p>\n<\/li>\n

            50. \n

              Asteroids in Netwire and Haskell<\/a> Haskell<\/p>\n<\/li>\n

            51. \n

              Formally verified certificate checkers for hardest-to-round computation<\/a> Coq<\/p>\n<\/li>\n

            52. \n

              Development and verification of probability logics and logical frameworks<\/a> Tesis Coq<\/p>\n<\/li>\n

            53. \n

              Formal kinematic analysis of the two-link planar manipulator<\/a>. HOL_Light<\/p>\n<\/li>\n

            54. \n

              Type theory and applications<\/a> Libro<\/p>\n<\/li>\n

            55. \n

              Strictness\/Unboxed explained<\/a> Haskell<\/p>\n<\/li>\n

            56. \n

              How Haskell can solve the integration problem<\/a> Haskell<\/p>\n<\/li>\n

            57. \n

              Modeling and optimizing MapReduce programs<\/a> Haskell<\/p>\n<\/li>\n

            58. \n

              Understanding free monoids and universal constructions<\/a> Haskell<\/p>\n<\/li>\n

            59. \n

              Curso: Programaci\u00f3n funcional avanzada<\/a> Haskell<\/p>\n<\/li>\n

            60. \n

              Prolog for programmers<\/a> Libro Prolog<\/p>\n<\/li>\n

            61. \n

              El problema de Josefo en Haskell<\/a>. Haskell<\/p>\n<\/li>\n

            62. \n

              Evaluaci\u00f3n en Haskell con tiempo acotado.<\/a> Haskell<\/p>\n<\/li>\n

            63. \n

              El juego de \u201ctres en raya\u201d en Haskell<\/a> Haskell<\/p>\n<\/li>\n

            64. \n

              Equational reasoning<\/a> Haskell<\/p>\n<\/li>\n

            65. \n

              El desaf\u00edo matem\u00e1tico \u201cUn n\u00famero curioso\u201d en Haskell<\/a> Haskell<\/p>\n<\/li>\n

            66. \n

              Software horror stories (Famous software failures)<\/a> Verificaci\u00f3n<\/p>\n<\/li>\n

            67. \n

              Decision procedures for Presburger arithmetic in Haskell<\/a> Haskell<\/p>\n<\/li>\n

            68. \n

              Deboggler: a small project to play with Haskell and data structures<\/a> Haskell<\/p>\n<\/li>\n

            69. \n

              FP Complete\u2019s guide to GHC extensions – a gentler documentation than the GHC docs<\/a> Haskell<\/p>\n<\/li>\n

            70. \n

              Practical fun with monads – Introducing: MonadPlus!<\/a> Haskell<\/p>\n<\/li>\n

            71. \n

              The list MonadPlus – Practical fun with monads (Part 2 of 3<\/a> Haskell<\/p>\n<\/li>\n

            72. \n

              Wolf, goat, cabbage: The list MonadPlus & logic problems<\/a> Haskell<\/p>\n<\/li>\n

            73. \n

              The heart and soul of computability<\/a> Libro<\/p>\n<\/li>\n

            74. \n

              Fallos inform\u00e1ticos y verificaci\u00f3n de programas.<\/a> Verificaci\u00f3n<\/p>\n<\/li>\n

            75. \n

              Why is formal methods necessary? (Famous software failures)<\/a> Verificaci\u00f3n<\/p>\n<\/li>\n

            76. \n

              Illustrative risks to the public in the use of computer systems and related technology<\/a> Verificaci\u00f3n<\/p>\n<\/li>\n

            77. \n

              El problema del granjero, la cabra y la col en Haskell<\/a> Haskell<\/p>\n<\/li>\n

            78. \n

              Ense\u00f1anza de l\u00f3gica en la universidad: experiencias en el uso de herramientas inform\u00e1ticas<\/a> Ense\u00f1anza<\/p>\n<\/li>\n

            79. \n

              Algoritmos e inducci\u00f3n<\/a> Algor\u00edtmica<\/p>\n<\/li>\n

            80. \n

              M\u00e1quinas de Turing y otros artilugios<\/a> Computabilidad<\/p>\n<\/li>\n

            81. \n

              An\u00e1lisis de algoritmos<\/a> Algor\u00edtmica<\/p>\n<\/li>\n<\/ol>\n

              Lecturas de Enero de 2014<\/h3>\n
                \n
              1. \n

                Lecture notes on the lambda calculus<\/a> LC<\/p>\n<\/li>\n

              2. \n

                Turing machines and undecidability<\/a> Computabilidad<\/p>\n<\/li>\n

              3. \n

                The SageMath Cloud: Python and computational mathematics in the cloud<\/a> Sage Python<\/p>\n<\/li>\n

              4. \n

                EasyAI: a pure-Python artificial intelligence framework for two-players abstract games such as Tic Tac Toe<\/a> IA Python<\/p>\n<\/li>\n

              5. \n

                A whirlwind tour of combinatorial games in Haskell<\/a> Haskell<\/p>\n<\/li>\n

              6. \n

                Semantics-directed machine architecture in ReWire<\/a> Haskell<\/p>\n<\/li>\n

              7. \n

                Formal analysis of the Kerberos authentication protocol with PVS<\/a> PVS<\/p>\n<\/li>\n

              8. \n

                Running Makefiles with Shake<\/a> Haskell<\/p>\n<\/li>\n

              9. \n

                Free Sage math cloud – Python and symbolic math<\/a> Sage Python<\/p>\n<\/li>\n

              10. \n

                Typed syntactic meta-programming<\/a> Agda<\/p>\n<\/li>\n

              11. \n

                Modular type-safety proofs in Agda<\/a> Agda<\/p>\n<\/li>\n

              12. \n

                IsarMathLib (A library of formalized mathematics for Isabelle\/ZF theorem proving environment) 1.9.1 released<\/a> Isabelle<\/p>\n<\/li>\n

              13. \n

                Experimental library of univalent formalization of mathematics<\/a> HoTT Coq<\/p>\n<\/li>\n

              14. \n

                A gentle guide to constraint logic programming via ECLiPSe (Third edition, 2014)<\/a> Libro Prolog<\/p>\n<\/li>\n

              15. \n

                Laziness is a virtue: an introduction to functional programming in Haskell<\/a> Haskell<\/p>\n<\/li>\n

              16. \n

                Dijkstra on Haskell and Java<\/a> Haskell<\/p>\n<\/li>\n

              17. \n

                The \u201cideal\u201d mathematician<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

              18. \n

                Applications of the Gauss-Jordan algorithm, done right<\/a>. Isabelle<\/p>\n<\/li>\n

              19. \n

                Verifying document confidentiality of a conference management system<\/a>. Isabelle<\/p>\n<\/li>\n

              20. \n

                Coinitial semantics for redecoration of triangular matrices<\/a> Coq<\/p>\n<\/li>\n

              21. \n

                Bidirectional proof search procedure for intuitionistic modal logic IS5<\/a> Coq<\/p>\n<\/li>\n

              22. \n

                Axiom selection as a machine learning problem<\/a> Isabelle ML<\/p>\n<\/li>\n

              23. \n

                Squiggoling with bialgebras (Recursion schemes from comonads revisited)<\/a> Haskell<\/p>\n<\/li>\n

              24. \n

                aspeed: Solver scheduling via answer set programming<\/a> ASP<\/p>\n<\/li>\n

              25. \n

                Principles of imperative computation (and methods for ensuring the correctness of programs<\/a> Curso Algor\u00edtmica<\/p>\n<\/li>\n

              26. \n

                Automatic functional harmonic analysis<\/a> Haskell<\/p>\n<\/li>\n

              27. \n

                Proof-by-instance for embedded network design (From prototype to tool roadmap)<\/a> Isabelle<\/p>\n<\/li>\n

              28. \n

                Verifying weight biased leftist heaps using dependent types<\/a> Agda<\/p>\n<\/li>\n

              29. \n

                Abstract interpretation using laziness: Proving Conway\u2019s lost cosmological theorem<\/a> Haskell<\/p>\n<\/li>\n

              30. \n

                Recurrence and induction<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

              31. \n

                Backpack: Retrofitting Haskell with interfaces<\/a> Haskell<\/p>\n<\/li>\n

              32. \n

                Combining proofs and programs in a dependently typed language<\/a> Coq<\/p>\n<\/li>\n

              33. \n

                A trusted mechanised JavaScript specification<\/a> Coq<\/p>\n<\/li>\n

              34. \n

                A verified information-flow architecture<\/a> Coq<\/p>\n<\/li>\n

              35. \n

                CakeML: A verified implementation of ML<\/a> HOL4<\/p>\n<\/li>\n

              36. \n

                Probabilistic relational verification for cryptographic implementations<\/a> Coq<\/p>\n<\/li>\n

              37. \n

                Freeze after writing (Quasi-deterministic parallel programming with LVars)<\/a> Haskell<\/p>\n<\/li>\n

              38. \n

                Modular, higher-order cardinality analysis in theory and practice<\/a> Haskell<\/p>\n<\/li>\n

              39. \n

                Profiling for laziness<\/a> Racket<\/p>\n<\/li>\n

              40. \n

                Modular reasoning about heap paths via effectively propositional formulas<\/a> SMT Z3<\/p>\n<\/li>\n

              41. \n

                Monadic combinators for \u201cputback\u201d style bidirectional programming<\/a> Haskell<\/p>\n<\/li>\n

              42. \n

                The HERMIT in the stream (Fusing stream fusion\u2019s concatMap)<\/a> Haskell<\/p>\n<\/li>\n

              43. \n

                Haskell applicative tutorial: a small tutorial, showing how you can use functors and applicatives<\/a> Haskell<\/p>\n<\/li>\n

              44. \n

                MuCheck : An extensible tool for mutation testing of Haskell programs<\/a> Haskell<\/p>\n<\/li>\n

              45. \n

                A DSL for describing the artificial intelligence in real-time video games<\/a> Haskell<\/p>\n<\/li>\n

              46. \n

                Shortcut fusion for pipes<\/a> Haskell<\/p>\n<\/li>\n

              47. \n

                La sucesi\u00f3n de Kolakoski<\/a> Haskell<\/p>\n<\/li>\n

              48. \n

                Verifying chinese train control system under a combined scenario by theorem proving<\/a> Isabelle<\/p>\n<\/li>\n

              49. \n

                Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5<\/a> Isabelle<\/p>\n<\/li>\n

              50. \n

                La conjetura de Gilbreath en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              51. \n

                Certifying algorithms<\/a> Verificaci\u00f3n<\/p>\n<\/li>\n

              52. \n

                Codificaci\u00f3n por longitud en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              53. \n

                El tri\u00e1ngulo de Pascal en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              54. \n

                Lista de factoriales perezosa en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              55. \n

                Sucesi\u00f3n de Fibonacci, evaluaci\u00f3n perezosa y n\u00fameros construibles<\/a> Haskell<\/p>\n<\/li>\n

              56. \n

                Memorabilia Mathematica (or the philomath\u2019s quotation-book)<\/a> Libro<\/p>\n<\/li>\n

              57. \n

                Codificaci\u00f3n por longitud en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              58. \n

                Two case studies in proving with side-effects: G\u00f6del\u2019s and Kripke\u2019s completeness theorems<\/a> Agda Coq<\/p>\n<\/li>\n

              59. \n

                Fixing bugs in \u201cComputing Homology\u201d<\/a> Python<\/p>\n<\/li>\n

              60. \n

                Formal verification, interactive theorem proving, and automated reasoning<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

              61. \n

                Specification and verification of concurrent programs through refinements<\/a> ACL2<\/p>\n<\/li>\n

              62. \n

                A formally verified generic branching algorithm for global optimization<\/a> PVS<\/p>\n<\/li>\n

              63. \n

                Distributed call-by-value machines<\/a> Agda<\/p>\n<\/li>\n

              64. \n

                Twenty years of theorem proving for HOLs (Past, present and future)<\/a> Historia<\/p>\n<\/li>\n

              65. \n

                Clasificaci\u00f3n supervisada y no supervisada<\/a> IA AA<\/p>\n<\/li>\n

              66. \n

                El juego de Oslo en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              67. \n

                Inductive triple graphs: A purely functional approach to represent RDF<\/a> Haskell Scala<\/p>\n<\/li>\n

              68. \n

                Formalizing the Kleene star for square matrices<\/a> Isabelle<\/p>\n<\/li>\n

              69. \n

                N\u00fameros triangulares y sus propiedades en Haskell<\/a> Haskell<\/p>\n<\/li>\n

              70. \n

                Mathematics in the age of the Turing machine<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

              71. \n

                Lecture notes on type theory<\/a> Libro<\/p>\n<\/li>\n

              72. \n

                A new type of Mathematics? New discoveries expand the scope of computer-assisted proofs of theorems<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

              73. \n

                Algorithms<\/a> Libro Algor\u00edtmica<\/p>\n<\/li>\n

              74. \n

                Balancing lists: a proof pearl<\/a>. Isabelle<\/p>\n<\/li>\n

              75. \n

                Bases de datos en grafo<\/a> IA<\/p>\n<\/li>\n<\/ol>\n

                Lecturas de Febrero de 2014<\/h3>\n
                  \n
                1. \n

                  Alan Turing and the origins of complexity<\/a> Historia<\/p>\n<\/li>\n

                2. \n

                  On Turing\u2019s legacy in mathematical logic and the foundations of mathematics<\/a> Historia<\/p>\n<\/li>\n

                3. \n

                  A survey of axiom selection as a machine learning problem<\/a> Isabelle<\/p>\n<\/li>\n

                4. \n

                  Eilenberg-MacLane spaces in homotopy type theory<\/a> Agda<\/p>\n<\/li>\n

                5. \n

                  Interactive SICP (Structure and Interpretation of Computer Programs)<\/a> Libro Scheme<\/p>\n<\/li>\n

                6. \n

                  A heuristic prover for real inequalities<\/a> AR<\/p>\n<\/li>\n

                7. \n

                  Arbitrary fun: Generating user profiles with QuickCheck<\/a> Haskell QuickCheck<\/p>\n<\/li>\n

                8. \n

                  A little lens starter tutorial<\/a> Haskell<\/p>\n<\/li>\n

                9. \n

                  N\u00fameros poligonales y sus propiedades en Haskell<\/a> Haskell<\/p>\n<\/li>\n

                10. \n

                  El tri\u00e1ngulo de Floyd en Haskell. http:\/\/bit.ly\/1nRULh<\/a> Haskell<\/p>\n<\/li>\n

                11. \n

                  Solving a regular expression crossword with Haskell, Part 2: Representation.<\/a> Haskell<\/p>\n<\/li>\n

                12. \n

                  Basics of \u03bb-calculus<\/a> LC<\/p>\n<\/li>\n

                13. \n

                  Verification of certifying computations through AutoCorres and Simpl<\/a> Isabelle<\/p>\n<\/li>\n

                14. \n

                  Implementing, and understanding type classes<\/a> Haskell<\/p>\n<\/li>\n

                15. \n

                  Survey of Satisfiability Modulo Theories (SMT)<\/a> SAT SMT<\/p>\n<\/li>\n

                16. \n

                  OTTER proofs of theorems in Tarskian geometry<\/a> OTTER<\/p>\n<\/li>\n

                17. \n

                  Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems<\/a> SAT SMT<\/p>\n<\/li>\n

                18. \n

                  Laplace\u2019s equation in Haskell: Using a DSL for stencils<\/a> Haskell<\/p>\n<\/li>\n

                19. \n

                  A test driven haskell course<\/a> Curso Haskell<\/p>\n<\/li>\n

                20. \n

                  Logic, languages and programming<\/a> Haskell<\/p>\n<\/li>\n

                21. \n

                  New draft of Haskell School of Music (PDF)<\/a> Libro Haskell<\/p>\n<\/li>\n

                22. \n

                  Properties of random graphs – subgraph containment<\/a>. Isabelle<\/p>\n<\/li>\n

                23. \n

                  Monad transformers for backtracking search<\/a> Haskell SAT<\/p>\n<\/li>\n

                24. \n

                  A survey of axiom selection as a machine learning problem<\/a>. Isabelle<\/p>\n<\/li>\n

                25. \n

                  Proof-by-instance for embedded network design (From prototype to tool roadmap)<\/a>. Isabelle<\/p>\n<\/li>\n

                26. \n

                  A mathematical proof too long to check – The Erdos discrepancy conjecture<\/a> SAT<\/p>\n<\/li>\n

                27. \n

                  Formalised mathematics<\/a> Agda<\/p>\n<\/li>\n

                28. \n

                  Coinitial semantics for redecoration of triangular matrices<\/a>. Coq<\/p>\n<\/li>\n

                29. \n

                  Rank nullity theorem of linear algebra<\/a> Isabelle<\/p>\n<\/li>\n

                30. \n

                  A brief intro to QuickCheck<\/a> Haskell QuickCheck<\/p>\n<\/li>\n

                31. \n

                  Complexity & verification: The history of programming as problem solving<\/a> Tesis Historia<\/p>\n<\/li>\n

                32. \n

                  A denotational semantics for natural language query interfaces to semantic web triplestores<\/a> Haskell<\/p>\n<\/li>\n

                33. \n

                  Learning-assisted theorem proving with millions of lemmas<\/a> IA AR ML<\/p>\n<\/li>\n

                34. \n

                  Thesis: formal study of efficient algorithms in linear algebra<\/a> Tesis Coq<\/p>\n<\/li>\n

                35. \n

                  A tutorial on using the Aeson packaged to parse JSON data<\/a> Haskell<\/p>\n<\/li>\n

                36. \n

                  A tutorial on the attoparsec parsing package<\/a> Haskell<\/p>\n<\/li>\n

                37. \n

                  Ejercicios sobre definiciones con unfoldr<\/a> Haskell<\/p>\n<\/li>\n

                38. \n

                  Haskell: A whirlwind tour (Part 1)<\/a> Haskell<\/p>\n<\/li>\n

                39. \n

                  Comprehensive formal verification of an OS microkernel<\/a> Isabelle Haskell<\/p>\n<\/li>\n

                40. \n

                  A Cretan maze using Haskell Diagrams<\/a> Haskell<\/p>\n<\/li>\n

                41. \n

                  Comparing Haskell Web frameworks<\/a> Haskell<\/p>\n<\/li>\n

                42. \n

                  What is formalized Mathematics<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

                43. \n

                  Random numbers in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                44. \n

                  Coin change<\/a> Haskell<\/p>\n<\/li>\n

                45. \n

                  Simple examples. Haskell<\/a> Haskell<\/p>\n<\/li>\n

                46. \n

                  Example of why to use monads – what they can do<\/a> Haskell<\/p>\n<\/li>\n

                47. \n

                  Solution counting<\/a> Haskell<\/p>\n<\/li>\n

                48. \n

                  Polynomials: Library for polynomials<\/a> Haskell<\/p>\n<\/li>\n

                49. \n

                  Root finding<\/a> Haskell<\/p>\n<\/li>\n

                50. \n

                  Simple interpolation<\/a> Haskell<\/p>\n<\/li>\n

                51. \n

                  Infinite subsets of natural numbers<\/a> Haskell<\/p>\n<\/li>\n

                52. \n

                  An introduction to QuickCheck testing<\/a> Haskell<\/p>\n<\/li>\n

                53. \n

                  Shortest path: Floyd-Warshall algorithm in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                54. \n

                  Knapsack – Brute force in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                55. \n

                  Automated and (formally) certified proofs of summation formulae<\/a> Coq<\/p>\n<\/li>\n

                56. \n

                  Induction and logical relations<\/a> Agda<\/p>\n<\/li>\n

                57. \n

                  Problema de Ramanujan de radicales anidados<\/a>. Haskell<\/p>\n<\/li>\n

                58. \n

                  Sucesiones auto descriptivas en Haskell<\/a>. Haskell<\/p>\n<\/li>\n

                59. \n

                  Proof assistant based on didactic considerations<\/a>. Ense\u00f1anza ANDY<\/p>\n<\/li>\n

                60. \n

                  A fully automatic problem solver with human-style output<\/a><\/p>\n<\/li>\n

                61. \n

                  Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model<\/a>. PVS<\/p>\n<\/li>\n

                62. \n

                  Formalizing Moessner\u2019s theorem and generalizations in Nuprl<\/a>. Nuprl<\/p>\n<\/li>\n

                63. \n

                  Preservation of Lyapunov-theoretic proofs: From real to floating-point arithmetic<\/a> Coq<\/p>\n<\/li>\n

                64. \n

                  A mechanized proof of loop freedom of the (untimed) AODV routing protocol<\/a> Isabelle<\/p>\n<\/li>\n

                65. \n

                  Showing invariance compositionally for a process algebra of network protocols<\/a> Isabelle<\/p>\n<\/li>\n<\/ol>\n

                  Lecturas de Marzo de 2014<\/h3>\n
                    \n
                  1. \n

                    Interaction entre alg\u00e8bre lin\u00e9aire et analyse en formalisation des math\u00e9matiques<\/a> Tesis Coq<\/p>\n<\/li>\n

                  2. \n

                    A Haskell-implementation of STM Haskell with early conflict detection<\/a> Haskell<\/p>\n<\/li>\n

                  3. \n

                    Mutation testing of functional programming languages<\/a> Haskell<\/p>\n<\/li>\n

                  4. \n

                    Harnessing constraint programming for poetry composition<\/a> ASP<\/p>\n<\/li>\n

                  5. \n

                    Formalization of binary fields and n-dimensional binary vector spaces using the Mizar proof checker<\/a> Mizar<\/p>\n<\/li>\n

                  6. \n

                    Content development for distance education in advanced university mathematics using Mizar<\/a> Mizar<\/p>\n<\/li>\n

                  7. \n

                    Computers, maths and minds<\/a><\/p>\n<\/li>\n

                  8. \n

                    Learning Agda to be a better Haskell programmer<\/a> Haskell Agda<\/p>\n<\/li>\n

                  9. \n

                    Learning Prolog to be a better Haskell programmer<\/a> Haskell Prolog<\/p>\n<\/li>\n

                  10. \n

                    Fun with functional dependencies (or (draft) types as values in static computations in Haskell)<\/a> Haskell<\/p>\n<\/li>\n

                  11. \n

                    Fun with type functions (version 3)<\/a> Haskell<\/p>\n<\/li>\n

                  12. \n

                    Data.Map vs Data.IntMap<\/a> Haskell<\/p>\n<\/li>\n

                  13. \n

                    Multi-line strings in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  14. \n

                    Data.Typeable and Data.Dynamic in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  15. \n

                    Implementing Union-Find algorithms in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  16. \n

                    Calling C library functions dynamically in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  17. \n

                    Implementing a JIT compiled language with Haskell and LLVM<\/a> Haskell<\/p>\n<\/li>\n

                  18. \n

                    Switching from monads to applicative functors<\/a> Haskell<\/p>\n<\/li>\n

                  19. \n

                    The power of lazy evaluation<\/a> Haskell<\/p>\n<\/li>\n

                  20. \n

                    How to replace failure by a list of successes<\/a> Haskell<\/p>\n<\/li>\n

                  21. \n

                    Using string literal for symbols<\/a> Haskell<\/p>\n<\/li>\n

                  22. \n

                    Parsing arithmetic expressions with Parsec<\/a> Haskell<\/p>\n<\/li>\n

                  23. \n

                    An ACL2 mechanization of an axiomatic weak memory model<\/a> ACL2<\/p>\n<\/li>\n

                  24. \n

                    From zipper to lens<\/a> Haskell<\/p>\n<\/li>\n

                  25. \n

                    Auto in Agda (Programming proof search)<\/a> Agda<\/p>\n<\/li>\n

                  26. \n

                    Introducci\u00f3n a las redes complejas<\/a> IA<\/p>\n<\/li>\n

                  27. \n

                    L\u00f3gica de enunciados<\/a> Libro L\u00f3gica<\/p>\n<\/li>\n

                  28. \n

                    L\u00f3gica de predicados<\/a> Libro L\u00f3gica<\/p>\n<\/li>\n

                  29. \n

                    Teor\u00eda de conjuntos b\u00e1sica (Conjuntos, relaciones y funciones)<\/a> Libro L\u00f3gica<\/p>\n<\/li>\n

                  30. \n

                    A brief introduction to Haskell, and why it matters<\/a> Haskell<\/p>\n<\/li>\n

                  31. \n

                    Haskell cheat sheets (Part 1)<\/a> Haskell<\/p>\n<\/li>\n

                  32. \n

                    Hspec: Behavior-driven development for Haskell<\/a> Haskell BDD<\/p>\n<\/li>\n

                  33. \n

                    Free applicative functors<\/a> Haskell<\/p>\n<\/li>\n

                  34. \n

                    Algebraic and analytic programming<\/a> Haskell Math<\/p>\n<\/li>\n

                  35. \n

                    L\u00f3gica y \u00e1lgebra de Boole<\/a> Libro L\u00f3gica<\/p>\n<\/li>\n

                  36. \n

                    LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration<\/a> Haskell<\/p>\n<\/li>\n

                  37. \n

                    Transparencias del curso \u201cAlgoritmia b\u00e1sica\u201d<\/a> Algor\u00edtmica<\/p>\n<\/li>\n

                  38. \n

                    Transparencias del curso \u201cAlgoritmia para problemas dif\u00edciles\u201d<\/a> Algor\u00edtmica<\/p>\n<\/li>\n

                  39. \n

                    Formalizing and verifying a modern build language<\/a> Coq<\/p>\n<\/li>\n

                  40. \n

                    A hybrid TM for Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  41. \n

                    Tiled polymorphic temporal media. (A functional pearl)<\/a> Haskell<\/p>\n<\/li>\n

                  42. \n

                    A seamless, client-centric programming model for type safe web applications<\/a> Haskell<\/p>\n<\/li>\n

                  43. \n

                    Defunctionalizing push arrays<\/a> Haskell<\/p>\n<\/li>\n

                  44. \n

                    Natural language reasoning using proof-assistant technology: Rich typing and beyond<\/a> Coq<\/p>\n<\/li>\n

                  45. \n

                    Intro to Haskell for Erlangers<\/a> Haskell<\/p>\n<\/li>\n

                  46. \n

                    Haskell for OCaml programmers<\/a> Haskell OCaml<\/p>\n<\/li>\n

                  47. \n

                    Programming and reasoning with side-effects in Idris<\/a> Idris<\/p>\n<\/li>\n

                  48. \n

                    Cr\u00e9at\u00far: Framework for artificial life and other evolutionary algorithms<\/a> Haskell<\/p>\n<\/li>\n

                  49. \n

                    Why Haskell is important for research, Part 1 of n<\/a> Haskell<\/p>\n<\/li>\n

                  50. \n

                    Programming with finite fields<\/a> Python<\/p>\n<\/li>\n

                  51. \n

                    Improving readability with the Maybe Foldable instance<\/a> Haskell<\/p>\n<\/li>\n

                  52. \n

                    Probabilistic noninterference<\/a> Isabelle<\/p>\n<\/li>\n

                  53. \n

                    Mechanization of the Algebra for Wireless Networks (AWN)<\/a> Isabelle<\/p>\n<\/li>\n

                  54. \n

                    Haskell for Coq programmers<\/a> Haskell Coq<\/p>\n<\/li>\n

                  55. \n

                    An introduction to recursion schemes and codata<\/a> Haskell<\/p>\n<\/li>\n

                  56. \n

                    Formal analysis of optical systems<\/a> HOL_Light<\/p>\n<\/li>\n

                  57. \n

                    Formally verified computation of enclosures of solutions of ordinary differential equations<\/a> Isabelle<\/p>\n<\/li>\n

                  58. \n

                    Verifying security policies using host attributes<\/a> Isabelle<\/p>\n<\/li>\n

                  59. \n

                    aspeed: Solver scheduling via Answer Set Programming<\/a> ASP<\/p>\n<\/li>\n

                  60. \n

                    A brief introduction to Haskell, and why it matters<\/a> Haskell<\/p>\n<\/li>\n

                  61. \n

                    Monoid morphisms, products, and coproducts<\/a> Scala<\/p>\n<\/li>\n

                  62. \n

                    Interactive tutorial of the sequent calculus<\/a> Ense\u00f1anza<\/p>\n<\/li>\n

                  63. \n

                    Bayesian analysis: A conjugate prior and Markov chain Monte Carlo<\/a> Haskell<\/p>\n<\/li>\n

                  64. \n

                    Cantor\u2019s diagonal argument in Agda<\/a> Agda<\/p>\n<\/li>\n

                  65. \n

                    H2048: A Haskell implementation of game 2048<\/a> Haskell<\/p>\n<\/li>\n

                  66. \n

                    Haskell in the browser: setting up Yesod and Fay<\/a> Haskell<\/p>\n<\/li>\n

                  67. \n

                    Presentation of Haskell in the Hackerspace Trento<\/a> Haskell<\/p>\n<\/li>\n

                  68. \n

                    Teach yourself logic: A study guide. Version 10.0 (20 March 2014<\/a> Libro<\/p>\n<\/li>\n

                  69. \n

                    Haskell from C: Where are the for Loops<\/a> Haskell<\/p>\n<\/li>\n

                  70. \n

                    What\u2019s wrong with the for loop<\/a> Haskell<\/p>\n<\/li>\n

                  71. \n

                    Why learn Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  72. \n

                    Algorithme de Babylone : une boucle sous toutes ses formes<\/a> Haskell<\/p>\n<\/li>\n

                  73. \n

                    Discr\u00e9tisation d\u2019\u00e9quations diff\u00e9rentielles<\/a> Haskell<\/p>\n<\/li>\n

                  74. \n

                    Au del\u00e0 des r\u00e9els: m\u00e9thodes num\u00e9riques en informatique<\/a> Haskell<\/p>\n<\/li>\n

                  75. \n

                    Polyn\u00f4mes de Taylor: graphiques et animations<\/a> Haskell<\/p>\n<\/li>\n

                  76. \n

                    M\u00e9thode de Briggs et de H\u00e9ron avec MPFR via Haskell et Sage<\/a> Haskell Sage<\/p>\n<\/li>\n

                  77. \n

                    Gauss par t\u00eate et queue<\/a> Haskell<\/p>\n<\/li>\n

                  78. \n

                    Z\/nZ sans arithm\u00e9tique modulaire \u2026<\/a> Haskell<\/p>\n<\/li>\n

                  79. \n

                    Alg\u00e8bre et informatique<\/a> Haskell<\/p>\n<\/li>\n

                  80. \n

                    Programmation fonctionnelle et Haskell for dummies<\/a> Haskell<\/p>\n<\/li>\n

                  81. \n

                    Relations binaires et fonctions avec Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  82. \n

                    Poker en Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  83. \n

                    Logique des propositions en Haskell part I<\/a> Haskell<\/p>\n<\/li>\n

                  84. \n

                    Math\u00e9matique discr\u00e8te et informatique<\/a> Libro Haskell<\/p>\n<\/li>\n

                  85. \n

                    Calcul math\u00e9matique avec Sage<\/a> Libro Sage<\/p>\n<\/li>\n

                  86. \n

                    The power algorithm<\/a> Haskell PHP<\/p>\n<\/li>\n

                  87. \n

                    Modeling and verification of distributed algorithms in theorem proving environments<\/a> Isabelle<\/p>\n<\/li>\n

                  88. \n

                    Directed security policies: A stateful network implementation<\/a> Isabelle<\/p>\n<\/li>\n

                  89. \n

                    John McCarthy \u2013 Father of Artificial Intelligence<\/a> Historia<\/p>\n<\/li>\n

                  90. \n

                    What it\u2019s like to use Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  91. \n

                    R\u00e9solution dichotomique de f(x)=0<\/a> Haskell<\/p>\n<\/li>\n

                  92. \n

                    Colecci\u00f3n de problemas sobre inteligencia artificial<\/a> Libro IA<\/p>\n<\/li>\n

                  93. \n

                    Monaris: A tetris clone written in Haskell using free-game<\/a> Haskell<\/p>\n<\/li>\n

                  94. \n

                    Formal proof of the fundamental theorem of decorated interval arithmetic<\/a> Tesis Coq<\/p>\n<\/li>\n

                  95. \n

                    Library to calculate Gr\u00f6bner basis written in Haskell<\/a> Haskell<\/p>\n<\/li>\n

                  96. \n

                    Introduction \u00e0 l\u2019algorithmique et \u00e0 la programmation avec Python<\/a> Python<\/p>\n<\/li>\n

                  97. \n

                    Algorithmic problem solving with Python<\/a> Libro Python<\/p>\n<\/li>\n

                  98. \n

                    Computational discrete mathematics with Python<\/a> Libro Python<\/p>\n<\/li>\n

                  99. \n

                    Formally verified mathematics<\/a> Divulgaci\u00f3n<\/p>\n<\/li>\n

                  100. \n

                    Towards a formally verified proof assistant<\/a> Coq Nuprl<\/p>\n<\/li>\n

                  101. \n

                    Formalization of a dynamic logic for graph transformation in the Coq proof assistant<\/a> Coq<\/p>\n<\/li>\n

                  102. \n

                    Interactive simplifier tracing and debugging in Isabelle<\/a> Isabelle<\/p>\n<\/li>\n<\/ol>\n

                    Una recopilaci\u00f3n de todas las lecturas se encuentra aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

                    Esta entrada es una recopilaci\u00f3n de lecturas compartidas en la lista de correo del grupo de l\u00f3gica computacional o en mi p\u00e1gina de twitter desde la anterior recopilaci\u00f3n. La recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista o en twitter. Al final de cada art\u00edculo se encuentra etiquetas relativas a los…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[6,177],"tags":[178,292],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4226"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4226"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4226\/revisions"}],"predecessor-version":[{"id":4229,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4226\/revisions\/4229"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4226"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4226"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4226"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}