Diferencia entre revisiones de «Lecturas del año 2014»

De WikiGLC
Saltar a: navegación, buscar
(Página creada con «== Lecturas de enero de 2014 == * [http://bit.ly/1doVDph Lecture notes on the lambda calculus] LC * [http://bit.ly/1doVOkh Turing machines and undecidability] Computabilid...»)
 
Línea 1: Línea 1:
 
== Lecturas de enero de 2014 ==
 
== Lecturas de enero de 2014 ==
  
* [http://bit.ly/1doVDph Lecture notes on the lambda calculus] LC
+
# [http://bit.ly/1doVDph Lecture notes on the lambda calculus] LC
* [http://bit.ly/1doVOkh Turing machines and undecidability] Computabilidad
+
# [http://bit.ly/1doVOkh Turing machines and undecidability] Computabilidad
* [http://bit.ly/1doWar4 The SageMath Cloud: Python and computational mathematics in the cloud] Sage Python
+
# [http://bit.ly/1doWar4 The SageMath Cloud: Python and computational mathematics in the cloud] Sage Python
* [http://bit.ly/1doWiHk EasyAI: a pure-Python artificial intelligence framework for two-players abstract games such as Tic Tac Toe] IA Python
+
# [http://bit.ly/1doWiHk EasyAI: a pure-Python artificial intelligence framework for two-players abstract games such as Tic Tac Toe] IA Python
* [http://bit.ly/19BqRdX A whirlwind tour of combinatorial games in Haskell] Haskell
+
# [http://bit.ly/19BqRdX A whirlwind tour of combinatorial games in Haskell] Haskell
* [http://bit.ly/1f2kkv5 Semantics-directed machine architecture in ReWire] Haskell
+
# [http://bit.ly/1f2kkv5 Semantics-directed machine architecture in ReWire] Haskell
* [http://bit.ly/1f2l57m Formal analysis of the Kerberos authentication protocol with PVS] PVS
+
# [http://bit.ly/1f2l57m Formal analysis of the Kerberos authentication protocol with PVS] PVS
* [http://bit.ly/1eyCorP Running Makefiles with Shake] Haskell
+
# [http://bit.ly/1eyCorP Running Makefiles with Shake] Haskell
* [http://bit.ly/KrgxcB Free Sage math cloud - Python and symbolic math] Sage Python
+
# [http://bit.ly/KrgxcB Free Sage math cloud - Python and symbolic math] Sage Python
* [http://bit.ly/KrgUUD Typed syntactic meta-programming] Agda
+
# [http://bit.ly/KrgUUD Typed syntactic meta-programming] Agda
* [http://bit.ly/Krh2n4 Modular type-safety proofs in Agda] Agda
+
# [http://bit.ly/Krh2n4 Modular type-safety proofs in Agda] Agda
* [http://bit.ly/KrhaTy IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment) 1.9.1 released] Isabelle
+
# [http://bit.ly/KrhaTy IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment) 1.9.1 released] Isabelle
* [http://bit.ly/KridTg Experimental library of univalent formalization of mathematics] HoTT Coq
+
# [http://bit.ly/KridTg Experimental library of univalent formalization of mathematics] HoTT Coq
* [http://bit.ly/fMi9V7 A gentle guide to constraint logic programming via ECLiPSe (Third edition, 2014)] Libro Prolog
+
# [http://bit.ly/fMi9V7 A gentle guide to constraint logic programming via ECLiPSe (Third edition, 2014)] Libro Prolog
* [http://bit.ly/1cDG2kL Laziness is a virtue: an introduction to functional programming in Haskell] Haskell
+
# [http://bit.ly/1cDG2kL Laziness is a virtue: an introduction to functional programming in Haskell] Haskell
* [http://bit.ly/1cDLTGs Dijkstra on Haskell and Java] Haskell
+
# [http://bit.ly/1cDLTGs Dijkstra on Haskell and Java] Haskell
* [http://bit.ly/1kupMZT The "ideal" mathematician] Divulgación
+
# [http://bit.ly/1kupMZT The "ideal" mathematician] Divulgación
* [http://arxiv.org/abs/1401.5910 Applications of the Gauss-Jordan algorithm, done right]. Isabelle
+
# [http://arxiv.org/abs/1401.5910 Applications of the Gauss-Jordan algorithm, done right]. Isabelle
* [http://bit.ly/1h4Sv2M Verifying document confidentiality of a conference management system]. Isabelle
+
# [http://bit.ly/1h4Sv2M Verifying document confidentiality of a conference management system]. Isabelle
* [http://bit.ly/KT95Yu Coinitial semantics for redecoration of triangular matrices] Coq
+
# [http://bit.ly/KT95Yu Coinitial semantics for redecoration of triangular matrices] Coq
* [http://bit.ly/KbZElN Bidirectional proof search procedure for intuitionistic modal logic IS5] Coq
+
# [http://bit.ly/KbZElN Bidirectional proof search procedure for intuitionistic modal logic IS5] Coq
* [http://bit.ly/1afMGui Axiom selection as a machine learning problem] Isabelle ML
+
# [http://bit.ly/1afMGui Axiom selection as a machine learning problem] Isabelle ML
* [http://bit.ly/1aa3Yfw Squiggoling with bialgebras (Recursion schemes from comonads revisited)] Haskell
+
# [http://bit.ly/1aa3Yfw Squiggoling with bialgebras (Recursion schemes from comonads revisited)] Haskell
* [http://bit.ly/1iwrUvQ aspeed: Solver scheduling via answer set programming] ASP
+
# [http://bit.ly/1iwrUvQ aspeed: Solver scheduling via answer set programming] ASP
* [http://bit.ly/1iORrjY Principles of imperative computation (and methods for ensuring the correctness of programs] Curso Algorítmica
+
# [http://bit.ly/1iORrjY Principles of imperative computation (and methods for ensuring the correctness of programs] Curso Algorítmica
* [http://bit.ly/1eLRPiA Automatic functional harmonic analysis] Haskell
+
# [http://bit.ly/1eLRPiA Automatic functional harmonic analysis] Haskell
* [http://bit.ly/L8umgu Proof-by-instance for embedded network design (From prototype to tool roadmap)] Isabelle
+
# [http://bit.ly/L8umgu Proof-by-instance for embedded network design (From prototype to tool roadmap)] Isabelle
* [http://bit.ly/1j9sfr9 Verifying weight biased leftist heaps using dependent types] Agda
+
# [http://bit.ly/1j9sfr9 Verifying weight biased leftist heaps using dependent types] Agda
* [http://bit.ly/1gVe5py Abstract interpretation using laziness: Proving Conway’s lost cosmological theorem] Haskell
+
# [http://bit.ly/1gVe5py Abstract interpretation using laziness: Proving Conway’s lost cosmological theorem] Haskell
* [http://bit.ly/Slaark Recurrence and induction] Divulgación
+
# [http://bit.ly/Slaark Recurrence and induction] Divulgación
* [http://bit.ly/Lodrq9 Backpack: Retrofitting Haskell with interfaces] Haskell
+
# [http://bit.ly/Lodrq9 Backpack: Retrofitting Haskell with interfaces] Haskell
* [http://bit.ly/1e3api8 Combining proofs and programs in a dependently typed language] Coq
+
# [http://bit.ly/1e3api8 Combining proofs and programs in a dependently typed language] Coq
* [http://bit.ly/1mg0Vom A trusted mechanised JavaScript specification] Coq
+
# [http://bit.ly/1mg0Vom A trusted mechanised JavaScript specification] Coq
* [http://bit.ly/1f1PvlJ A verified information-flow architecture] Coq
+
# [http://bit.ly/1f1PvlJ A verified information-flow architecture] Coq
* [http://bit.ly/1eVIzIF CakeML: A verified implementation of ML] HOL4
+
# [http://bit.ly/1eVIzIF CakeML: A verified implementation of ML] HOL4
* [http://bit.ly/1eVITHr Probabilistic relational verification for cryptographic implementations] Coq
+
# [http://bit.ly/1eVITHr Probabilistic relational verification for cryptographic implementations] Coq
* [http://bit.ly/1h3xqoH Freeze after writing (Quasi-deterministic parallel programming with LVars)] Haskell
+
# [http://bit.ly/1h3xqoH Freeze after writing (Quasi-deterministic parallel programming with LVars)] Haskell
* [http://bit.ly/1kLWk1R Modular, higher-order cardinality analysis in theory and practice] Haskell
+
# [http://bit.ly/1kLWk1R Modular, higher-order cardinality analysis in theory and practice] Haskell
* [http://bit.ly/1gVpFDX Profiling for laziness] Racket
+
# [http://bit.ly/1gVpFDX Profiling for laziness] Racket
* [http://bit.ly/1jeG87n Modular reasoning about heap paths via effectively propositional formulas] SMT Z3
+
# [http://bit.ly/1jeG87n Modular reasoning about heap paths via effectively propositional formulas] SMT Z3
* [http://bit.ly/1kLZpPj Monadic combinators for "putback" style bidirectional programming] Haskell
+
# [http://bit.ly/1kLZpPj Monadic combinators for "putback" style bidirectional programming] Haskell
* [http://bit.ly/1hCPJSt The HERMIT in the stream (Fusing stream fusion’s concatMap)] Haskell
+
# [http://bit.ly/1hCPJSt The HERMIT in the stream (Fusing stream fusion’s concatMap)] Haskell
* [http://bit.ly/1bmNmSJ Haskell applicative tutorial: a small tutorial, showing how you can use functors and applicatives] Haskell
+
# [http://bit.ly/1bmNmSJ Haskell applicative tutorial: a small tutorial, showing how you can use functors and applicatives] Haskell
* [http://bit.ly/1brZaTK MuCheck : An extensible tool for mutation testing of Haskell programs] Haskell
+
# [http://bit.ly/1brZaTK MuCheck : An extensible tool for mutation testing of Haskell programs] Haskell
* [http://bit.ly/1icYPbn A DSL for describing the artificial intelligence in real-time video games] Haskell
+
# [http://bit.ly/1icYPbn A DSL for describing the artificial intelligence in real-time video games] Haskell
* [http://bit.ly/1icZt8N Shortcut fusion for pipes] Haskell
+
# [http://bit.ly/1icZt8N Shortcut fusion for pipes] Haskell
* [http://bit.ly/1beeZt6 La sucesión de Kolakoski] Haskell
+
# [http://bit.ly/1beeZt6 La sucesión de Kolakoski] Haskell
* [http://bit.ly/LLDZlZ Verifying chinese train control system under a combined scenario by theorem proving] Isabelle
+
# [http://bit.ly/LLDZlZ Verifying chinese train control system under a combined scenario by theorem proving] Isabelle
* [http://bit.ly/1f7Xyxg Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5] Isabelle
+
# [http://bit.ly/1f7Xyxg Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5] Isabelle
* [http://bit.ly/1jjXbFe La conjetura de Gilbreath en Haskell] Haskell
+
# [http://bit.ly/1jjXbFe La conjetura de Gilbreath en Haskell] Haskell
* [http://bit.ly/tuVSiL Certifying algorithms] Verificación
+
# [http://bit.ly/tuVSiL Certifying algorithms] Verificación
* [http://bit.ly/1kUBU6P Codificación por longitud en Haskell] Haskell
+
# [http://bit.ly/1kUBU6P Codificación por longitud en Haskell] Haskell
* [http://bit.ly/1dROMVG El triángulo de Pascal en Haskell] Haskell
+
# [http://bit.ly/1dROMVG El triángulo de Pascal en Haskell] Haskell
* [http://bit.ly/19MLK5D Lista de factoriales perezosa en Haskell] Haskell
+
# [http://bit.ly/19MLK5D Lista de factoriales perezosa en Haskell] Haskell
* [http://bit.ly/1aJb233 Sucesión de Fibonacci, evaluación perezosa y números construibles] Haskell
+
# [http://bit.ly/1aJb233 Sucesión de Fibonacci, evaluación perezosa y números construibles] Haskell
* [http://bit.ly/1dQFPh6 Memorabilia Mathematica (or the philomath’s quotation-book)] Libro
+
# [http://bit.ly/1dQFPh6 Memorabilia Mathematica (or the philomath’s quotation-book)] Libro
* [http://bit.ly/1kUBU6P Codificación por longitud en Haskell] Haskell
+
# [http://bit.ly/1kUBU6P Codificación por longitud en Haskell] Haskell
* [http://bit.ly/1hstlL4 Two case studies in proving with side-effects: Gödel's and Kripke's completeness theorems] Agda Coq
+
# [http://bit.ly/1hstlL4 Two case studies in proving with side-effects: Gödel's and Kripke's completeness theorems] Agda Coq
* [http://bit.ly/1hswudC Fixing bugs in "Computing Homology"] Python
+
# [http://bit.ly/1hswudC Fixing bugs in "Computing Homology"] Python
* [http://bit.ly/1hsA8Ew Formal verification, interactive theorem proving, and automated reasoning] Divulgación
+
# [http://bit.ly/1hsA8Ew Formal verification, interactive theorem proving, and automated reasoning] Divulgación
* [http://bit.ly/M7OmAM Specification and verification of concurrent programs through refinements] ACL2
+
# [http://bit.ly/M7OmAM Specification and verification of concurrent programs through refinements] ACL2
* [http://1.usa.gov/16v4vXx A formally verified generic branching algorithm for global optimization] PVS
+
# [http://1.usa.gov/16v4vXx A formally verified generic branching algorithm for global optimization] PVS
* [http://bit.ly/1dWSLlt Distributed call-by-value machines] Agda
+
# [http://bit.ly/1dWSLlt Distributed call-by-value machines] Agda
* [http://bit.ly/pplL8j Twenty years of theorem proving for HOLs (Past, present and future)] Historia
+
# [http://bit.ly/pplL8j Twenty years of theorem proving for HOLs (Past, present and future)] Historia
* [http://bit.ly/MeJYjs Clasificación supervisada y no supervisada] IA AA
+
# [http://bit.ly/MeJYjs Clasificación supervisada y no supervisada] IA AA
* [http://bit.ly/1e0n0bs El juego de Oslo en Haskell] Haskell
+
# [http://bit.ly/1e0n0bs El juego de Oslo en Haskell] Haskell
* [http://bit.ly/1jZMSUs Inductive triple graphs: A purely functional approach to represent RDF] Haskell Scala
+
# [http://bit.ly/1jZMSUs Inductive triple graphs: A purely functional approach to represent RDF] Haskell Scala
* [http://bit.ly/19Yo2n2 Formalizing the Kleene star for square matrices] Isabelle
+
# [http://bit.ly/19Yo2n2 Formalizing the Kleene star for square matrices] Isabelle
* [http://bit.ly/LlfdZA Números triangulares y sus propiedades en Haskell] Haskell
+
# [http://bit.ly/LlfdZA Números triangulares y sus propiedades en Haskell] Haskell
* [http://bit.ly/1baWRRr Mathematics in the age of the Turing machine] Divulgación
+
# [http://bit.ly/1baWRRr Mathematics in the age of the Turing machine] Divulgación
* [http://bit.ly/1baXeLC Lecture notes on type theory] Libro
+
# [http://bit.ly/1baXeLC Lecture notes on type theory] Libro
* [http://bit.ly/1baXzhk A new type of Mathematics? New discoveries expand the scope of computer-assisted proofs of theorems] Divulgación
+
# [http://bit.ly/1baXzhk A new type of Mathematics? New discoveries expand the scope of computer-assisted proofs of theorems] Divulgación
* [http://bit.ly/1kidLDr Algorithms] Libro Algorítmica
+
# [http://bit.ly/1kidLDr Algorithms] Libro Algorítmica
* [http://arxiv.org/abs/1401.7886 Balancing lists: a proof pearl]. Isabelle
+
# [http://arxiv.org/abs/1401.7886 Balancing lists: a proof pearl]. Isabelle
* [http://bit.ly/1eDgAtQ Bases de datos en grafo] IA
+
# [http://bit.ly/1eDgAtQ Bases de datos en grafo] IA
  
 
== Lecturas de febrero de 2014 ==
 
== Lecturas de febrero de 2014 ==
  
* [http://bit.ly/MI5qO0 Alan Turing and the origins of complexity] Historia
+
# [http://bit.ly/MI5qO0 Alan Turing and the origins of complexity] Historia
* [http://bit.ly/MI5ddN On Turing’s legacy in mathematical logic and the foundations of mathematics] Historia
+
# [http://bit.ly/MI5ddN On Turing’s legacy in mathematical logic and the foundations of mathematics] Historia
* [http://bit.ly/1beUD3f A survey of axiom selection as a machine learning problem] Isabelle
+
# [http://bit.ly/1beUD3f A survey of axiom selection as a machine learning problem] Isabelle
* [http://bit.ly/LknVql Eilenberg-MacLane spaces in homotopy type theory] Agda
+
# [http://bit.ly/LknVql Eilenberg-MacLane spaces in homotopy type theory] Agda
* [http://bit.ly/1cIQTLL Interactive SICP (Structure and Interpretation of Computer Programs)] Libro Scheme
+
# [http://bit.ly/1cIQTLL Interactive SICP (Structure and Interpretation of Computer Programs)] Libro Scheme
* [http://bit.ly/1cIRixz A heuristic prover for real inequalities] AR
+
# [http://bit.ly/1cIRixz A heuristic prover for real inequalities] AR
* [http://bit.ly/1cISaCv Arbitrary fun: Generating user profiles with QuickCheck] Haskell QuickCheck
+
# [http://bit.ly/1cISaCv Arbitrary fun: Generating user profiles with QuickCheck] Haskell QuickCheck
* [http://bit.ly/1cISqRS A little lens starter tutorial] Haskell
+
# [http://bit.ly/1cISqRS A little lens starter tutorial] Haskell
* [http://bit.ly/1nJJ78B Números poligonales y sus propiedades en Haskell] Haskell
+
# [http://bit.ly/1nJJ78B Números poligonales y sus propiedades en Haskell] Haskell
* [http://bit.ly/1dqVqOH El triángulo de Floyd en Haskell. http://bit.ly/1nRULh] Haskell
+
# [http://bit.ly/1dqVqOH El triángulo de Floyd en Haskell. http://bit.ly/1nRULh] Haskell
* [http://bit.ly/1dqWdix Solving a regular expression crossword with Haskell, Part 2: Representation.] Haskell
+
# [http://bit.ly/1dqWdix Solving a regular expression crossword with Haskell, Part 2: Representation.] Haskell
* [http://bit.ly/1dqXlCE Basics of λ-calculus] LC
+
# [http://bit.ly/1dqXlCE Basics of λ-calculus] LC
* [http://bit.ly/1nUCosA Verification of certifying computations through AutoCorres and Simpl] Isabelle
+
# [http://bit.ly/1nUCosA Verification of certifying computations through AutoCorres and Simpl] Isabelle
* [http://bit.ly/1nlMu2A Implementing, and understanding type classes] Haskell
+
# [http://bit.ly/1nlMu2A Implementing, and understanding type classes] Haskell
* [http://bit.ly/1aTwaG4 Survey of Satisfiability Modulo Theories (SMT)] SAT SMT
+
# [http://bit.ly/1aTwaG4 Survey of Satisfiability Modulo Theories (SMT)] SAT SMT
* [http://bit.ly/1fY7R7k OTTER proofs of theorems in Tarskian geometry] OTTER
+
# [http://bit.ly/1fY7R7k OTTER proofs of theorems in Tarskian geometry] OTTER
* [http://bit.ly/1ffnHJf Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems] SAT SMT
+
# [http://bit.ly/1ffnHJf Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems] SAT SMT
* [http://bit.ly/1boQAHu Laplace’s equation in Haskell: Using a DSL for stencils] Haskell
+
# [http://bit.ly/1boQAHu Laplace’s equation in Haskell: Using a DSL for stencils] Haskell
* [http://bit.ly/1boShEE A test driven haskell course] Curso Haskell
+
# [http://bit.ly/1boShEE A test driven haskell course] Curso Haskell
* [http://bit.ly/1gNOr5Z Logic, languages and programming] Haskell
+
# [http://bit.ly/1gNOr5Z Logic, languages and programming] Haskell
* [http://bit.ly/1g8ETSq New draft of Haskell School of Music (PDF)] Libro Haskell
+
# [http://bit.ly/1g8ETSq New draft of Haskell School of Music (PDF)] Libro Haskell
* [http://afp.sourceforge.net/entries/Random_Graph_Subgraph_Threshold.shtml Properties of random graphs - subgraph containment]. Isabelle
+
# [http://afp.sourceforge.net/entries/Random_Graph_Subgraph_Threshold.shtml Properties of random graphs - subgraph containment]. Isabelle
* [http://bit.ly/1moYTrm Monad transformers for backtracking search] Haskell SAT
+
# [http://bit.ly/1moYTrm Monad transformers for backtracking search] Haskell SAT
* [http://bit.ly/1beUD3f A survey of axiom selection as a machine learning problem]. Isabelle
+
# [http://bit.ly/1beUD3f A survey of axiom selection as a machine learning problem]. Isabelle
* [http://bit.ly/L8umgu Proof-by-instance for embedded network design (From prototype to tool roadmap)]. Isabelle
+
# [http://bit.ly/L8umgu Proof-by-instance for embedded network design (From prototype to tool roadmap)]. Isabelle
* [http://bit.ly/1mtttA9 A mathematical proof too long to check - The Erdos discrepancy conjecture] SAT
+
# [http://bit.ly/1mtttA9 A mathematical proof too long to check - The Erdos discrepancy conjecture] SAT
* [http://bit.ly/1mtutEf Formalised mathematics] Agda
+
# [http://bit.ly/1mtutEf Formalised mathematics] Agda
* [http://bit.ly/KT95Yu Coinitial semantics for redecoration of triangular matrices]. Coq
+
# [http://bit.ly/KT95Yu Coinitial semantics for redecoration of triangular matrices]. Coq
* [http://bit.ly/Oelpo0 Rank nullity theorem of linear algebra] Isabelle
+
# [http://bit.ly/Oelpo0 Rank nullity theorem of linear algebra] Isabelle
* [http://bit.ly/1jSi9bI A brief intro to QuickCheck] Haskell QuickCheck
+
# [http://bit.ly/1jSi9bI A brief intro to QuickCheck] Haskell QuickCheck
* [http://bit.ly/1gUsJ22 Complexity & verification: The history of programming as problem solving] Tesis Historia
+
# [http://bit.ly/1gUsJ22 Complexity & verification: The history of programming as problem solving] Tesis Historia
* [http://bit.ly/1fiwHmc A denotational semantics for natural language query interfaces to semantic web triplestores] Haskell
+
# [http://bit.ly/1fiwHmc A denotational semantics for natural language query interfaces to semantic web triplestores] Haskell
* [http://bit.ly/1foYkIB Learning-assisted theorem proving with millions of lemmas] IA AR ML
+
# [http://bit.ly/1foYkIB Learning-assisted theorem proving with millions of lemmas] IA AR ML
* [http://bit.ly/Mi30Vk Thesis: formal study of efficient algorithms in linear algebra] Tesis Coq
+
# [http://bit.ly/Mi30Vk Thesis: formal study of efficient algorithms in linear algebra] Tesis Coq
* [http://bit.ly/1caqym3 A tutorial on using the Aeson packaged to parse JSON data] Haskell
+
# [http://bit.ly/1caqym3 A tutorial on using the Aeson packaged to parse JSON data] Haskell
* [http://bit.ly/1h9MsdF A tutorial on the attoparsec parsing package] Haskell
+
# [http://bit.ly/1h9MsdF A tutorial on the attoparsec parsing package] Haskell
* [http://bit.ly/1h9QT8j Ejercicios sobre definiciones con unfoldr] Haskell
+
# [http://bit.ly/1h9QT8j Ejercicios sobre definiciones con unfoldr] Haskell
* [http://slidesha.re/j44h2L Haskell: A whirlwind tour (Part 1)] Haskell
+
# [http://slidesha.re/j44h2L Haskell: A whirlwind tour (Part 1)] Haskell
* [http://bit.ly/1etdYON Comprehensive formal verification of an OS microkernel] Isabelle Haskell
+
# [http://bit.ly/1etdYON Comprehensive formal verification of an OS microkernel] Isabelle Haskell
* [http://bit.ly/1eteufH A Cretan maze using Haskell Diagrams] Haskell
+
# [http://bit.ly/1eteufH A Cretan maze using Haskell Diagrams] Haskell
* [http://bit.ly/1eteTyA Comparing Haskell Web frameworks] Haskell
+
# [http://bit.ly/1eteTyA Comparing Haskell Web frameworks] Haskell
* [http://bit.ly/1hP6Kwm What is formalized Mathematics] Divulgación
+
# [http://bit.ly/1hP6Kwm What is formalized Mathematics] Divulgación
* [http://bit.ly/NzEGPy Random numbers in Haskell] Haskell
+
# [http://bit.ly/NzEGPy Random numbers in Haskell] Haskell
* [http://bit.ly/NzF7tn Coin change] Haskell
+
# [http://bit.ly/NzF7tn Coin change] Haskell
* [http://bit.ly/NzFyUo Simple examples. Haskell] Haskell
+
# [http://bit.ly/NzFyUo Simple examples. Haskell] Haskell
* [http://bit.ly/NzGBUz Example of why to use monads - what they can do] Haskell
+
# [http://bit.ly/NzGBUz Example of why to use monads - what they can do] Haskell
* [http://bit.ly/NzIlgo Solution counting] Haskell
+
# [http://bit.ly/NzIlgo Solution counting] Haskell
* [http://bit.ly/NzIPmD Polynomials: Library for polynomials] Haskell
+
# [http://bit.ly/NzIPmD Polynomials: Library for polynomials] Haskell
* [http://bit.ly/NzJuog Root finding] Haskell
+
# [http://bit.ly/NzJuog Root finding] Haskell
* [http://bit.ly/NzJG6Y Simple interpolation] Haskell
+
# [http://bit.ly/NzJG6Y Simple interpolation] Haskell
* [http://bit.ly/NzJYe6 Infinite subsets of natural numbers] Haskell
+
# [http://bit.ly/NzJYe6 Infinite subsets of natural numbers] Haskell
* [http://bit.ly/NzKmsS An introduction to QuickCheck testing] Haskell
+
# [http://bit.ly/NzKmsS An introduction to QuickCheck testing] Haskell
* [http://bit.ly/NzZtTo Shortest path: Floyd-Warshall algorithm in Haskell] Haskell
+
# [http://bit.ly/NzZtTo Shortest path: Floyd-Warshall algorithm in Haskell] Haskell
* [http://bit.ly/NzZLto Knapsack - Brute force in Haskell] Haskell
+
# [http://bit.ly/NzZLto Knapsack - Brute force in Haskell] Haskell
* [http://bit.ly/1fhn6d0 Automated and (formally) certified proofs of summation formulae] Coq
+
# [http://bit.ly/1fhn6d0 Automated and (formally) certified proofs of summation formulae] Coq
* [http://bit.ly/1fhuqpa Induction and logical relations] Agda
+
# [http://bit.ly/1fhuqpa Induction and logical relations] Agda
* [http://bit.ly/18LQNvH Problema de Ramanujan de radicales anidados]. Haskell
+
# [http://bit.ly/18LQNvH Problema de Ramanujan de radicales anidados]. Haskell
* [http://bit.ly/18LroZ9 Sucesiones auto descriptivas en Haskell]. Haskell
+
# [http://bit.ly/18LroZ9 Sucesiones auto descriptivas en Haskell]. Haskell
* [http://www.jucs.org/jucs_19_11/proof_assistant_based_on/jucs_19_11_1570_1596_pais.pdf Proof assistant based on didactic considerations]. Enseñanza ANDY
+
# [http://www.jucs.org/jucs_19_11/proof_assistant_based_on/jucs_19_11_1570_1596_pais.pdf Proof assistant based on didactic considerations]. Enseñanza ANDY
* [http://arxiv.org/abs/1309.4501 A fully automatic problem solver with human-style output]
+
# [http://arxiv.org/abs/1309.4501 A fully automatic problem solver with human-style output]
* [http://jfr.unibo.it/article/download/3720/3357 Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. PVS
+
# [http://jfr.unibo.it/article/download/3720/3357 Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. PVS
* [http://128.84.154.137/~kozen/papers/MoessnerNuprl.pdf Formalizing Moessner’s theorem and generalizations in Nuprl]. Nuprl
+
# [http://128.84.154.137/~kozen/papers/MoessnerNuprl.pdf Formalizing Moessner’s theorem and generalizations in Nuprl]. Nuprl
* [http://bit.ly/MAsnSg Preservation of Lyapunov-theoretic proofs: From real to floating-point arithmetic] Coq
+
# [http://bit.ly/MAsnSg Preservation of Lyapunov-theoretic proofs: From real to floating-point arithmetic] Coq
* [http://bit.ly/1kf2mHd A mechanized proof of loop freedom of the (untimed) AODV routing protocol] Isabelle
+
# [http://bit.ly/1kf2mHd A mechanized proof of loop freedom of the (untimed) AODV routing protocol] Isabelle
* [http://bit.ly/1pBA62e Showing invariance compositionally for a process algebra of network protocols] Isabelle
+
# [http://bit.ly/1pBA62e Showing invariance compositionally for a process algebra of network protocols] Isabelle
  
 
== Lecturas de marzo de 2014 ==
 
== Lecturas de marzo de 2014 ==
  
* [http://bit.ly/1ctASFL Interaction entre algèbre linéaire et analyse en formalisation des mathématiques] Tesis Coq
+
# [http://bit.ly/1ctASFL Interaction entre algèbre linéaire et analyse en formalisation des mathématiques] Tesis Coq
* [http://bit.ly/1cib1Go A Haskell-implementation of STM Haskell with early conflict detection] Haskell
+
# [http://bit.ly/1cib1Go A Haskell-implementation of STM Haskell with early conflict detection] Haskell
* [http://bit.ly/1mMlBK0 Mutation testing of functional programming languages] Haskell
+
# [http://bit.ly/1mMlBK0 Mutation testing of functional programming languages] Haskell
* [http://bit.ly/1gIUPef Harnessing constraint programming for poetry composition] ASP
+
# [http://bit.ly/1gIUPef Harnessing constraint programming for poetry composition] ASP
* [http://bit.ly/1bUUp7f Formalization of binary fields and n-dimensional binary vector spaces using the Mizar proof checker] Mizar
+
# [http://bit.ly/1bUUp7f Formalization of binary fields and n-dimensional binary vector spaces using the Mizar proof checker] Mizar
* [http://bit.ly/Ng8SiZ Content development for distance education in advanced university mathematics using Mizar] Mizar
+
# [http://bit.ly/Ng8SiZ Content development for distance education in advanced university mathematics using Mizar] Mizar
* [http://bit.ly/1dqVqOH Computers, maths and minds]
+
# [http://bit.ly/1dqVqOH Computers, maths and minds]
* [http://bit.ly/1eJUhXD Learning Agda to be a better Haskell programmer] Haskell Agda
+
# [http://bit.ly/1eJUhXD Learning Agda to be a better Haskell programmer] Haskell Agda
* [http://bit.ly/1eJVcHK Learning Prolog to be a better Haskell programmer] Haskell Prolog
+
# [http://bit.ly/1eJVcHK Learning Prolog to be a better Haskell programmer] Haskell Prolog
* [http://bit.ly/1lu5H5y Fun with functional dependencies (or (draft) types as values in static computations in Haskell)] Haskell
+
# [http://bit.ly/1lu5H5y Fun with functional dependencies (or (draft) types as values in static computations in Haskell)] Haskell
* [http://bit.ly/1eJX17u Fun with type functions (version 3)] Haskell
+
# [http://bit.ly/1eJX17u Fun with type functions (version 3)] Haskell
* [http://bit.ly/1eJXoyI Data.Map vs Data.IntMap] Haskell
+
# [http://bit.ly/1eJXoyI Data.Map vs Data.IntMap] Haskell
* [http://bit.ly/1eJY1Zl Multi-line strings in Haskell] Haskell
+
# [http://bit.ly/1eJY1Zl Multi-line strings in Haskell] Haskell
* [http://bit.ly/1eJYF91 Data.Typeable and Data.Dynamic in Haskell] Haskell
+
# [http://bit.ly/1eJYF91 Data.Typeable and Data.Dynamic in Haskell] Haskell
* [http://bit.ly/1eJZ0J0 Implementing Union-Find algorithms in Haskell] Haskell
+
# [http://bit.ly/1eJZ0J0 Implementing Union-Find algorithms in Haskell] Haskell
* [http://bit.ly/1eJZr5T Calling C library functions dynamically in Haskell] Haskell
+
# [http://bit.ly/1eJZr5T Calling C library functions dynamically in Haskell] Haskell
* [http://bit.ly/1eK08fG Implementing a JIT compiled language with Haskell and LLVM] Haskell
+
# [http://bit.ly/1eK08fG Implementing a JIT compiled language with Haskell and LLVM] Haskell
* [http://bit.ly/1eK1oiM Switching from monads to applicative functors] Haskell
+
# [http://bit.ly/1eK1oiM Switching from monads to applicative functors] Haskell
* [http://bit.ly/1eK2E5J The power of lazy evaluation] Haskell
+
# [http://bit.ly/1eK2E5J The power of lazy evaluation] Haskell
* [http://bit.ly/1eK2Vpg How to replace failure by a list of successes] Haskell
+
# [http://bit.ly/1eK2Vpg How to replace failure by a list of successes] Haskell
* [http://bit.ly/1eK3pM6 Using string literal for symbols] Haskell
+
# [http://bit.ly/1eK3pM6 Using string literal for symbols] Haskell
* [http://bit.ly/1eK4Aee Parsing arithmetic expressions with Parsec] Haskell
+
# [http://bit.ly/1eK4Aee Parsing arithmetic expressions with Parsec] Haskell
* [http://bit.ly/1fXOMEP An ACL2 mechanization of an axiomatic weak memory model] ACL2
+
# [http://bit.ly/1fXOMEP An ACL2 mechanization of an axiomatic weak memory model] ACL2
* [http://bit.ly/1i3Jo1E From zipper to lens] Haskell
+
# [http://bit.ly/1i3Jo1E From zipper to lens] Haskell
* [http://bit.ly/1i3KcDU Auto in Agda (Programming proof search)] Agda
+
# [http://bit.ly/1i3KcDU Auto in Agda (Programming proof search)] Agda
* [http://bit.ly/1i3Lvmk Introducción a las redes complejas] IA
+
# [http://bit.ly/1i3Lvmk Introducción a las redes complejas] IA
* [http://bit.ly/1gP0EH5 Lógica de enunciados] Libro Lógica
+
# [http://bit.ly/1gP0EH5 Lógica de enunciados] Libro Lógica
* [http://bit.ly/1gP140c Lógica de predicados] Libro Lógica
+
# [http://bit.ly/1gP140c Lógica de predicados] Libro Lógica
* [http://bit.ly/1gP1kfz Teoría de conjuntos básica (Conjuntos, relaciones y funciones)] Libro Lógica
+
# [http://bit.ly/1gP1kfz Teoría de conjuntos básica (Conjuntos, relaciones y funciones)] Libro Lógica
* [http://bit.ly/1cHRkCw A brief introduction to Haskell, and why it matters] Haskell
+
# [http://bit.ly/1cHRkCw A brief introduction to Haskell, and why it matters] Haskell
* [http://bit.ly/1cHRRV9 Haskell cheat sheets (Part 1)] Haskell
+
# [http://bit.ly/1cHRRV9 Haskell cheat sheets (Part 1)] Haskell
* [http://bit.ly/1liV56O Hspec: Behavior-driven development for Haskell]<br /> Haskell BDD
+
# [http://bit.ly/1liV56O Hspec: Behavior-driven development for Haskell]<br /> Haskell BDD
* [http://bit.ly/1liXbDq Free applicative functors] Haskell
+
# [http://bit.ly/1liXbDq Free applicative functors] Haskell
* [http://bit.ly/1liXtKC Algebraic and analytic programming]<br /> Haskell Math
+
# [http://bit.ly/1liXtKC Algebraic and analytic programming]<br /> Haskell Math
* [http://bit.ly/1liYyCa Lógica y álgebra de Boole]<br /> Libro Lógica
+
# [http://bit.ly/1liYyCa Lógica y álgebra de Boole]<br /> Libro Lógica
* [http://bit.ly/1liZ0jZ LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration] Haskell
+
# [http://bit.ly/1liZ0jZ LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration] Haskell
* [http://bit.ly/1fPv5AB Transparencias del curso &quot;Algoritmia básica&quot;] Algorítmica
+
# [http://bit.ly/1fPv5AB Transparencias del curso &quot;Algoritmia básica&quot;] Algorítmica
* [http://bit.ly/1kGJGAs Transparencias del curso &quot;Algoritmia para problemas difíciles&quot;] Algorítmica
+
# [http://bit.ly/1kGJGAs Transparencias del curso &quot;Algoritmia para problemas difíciles&quot;] Algorítmica
* [http://bit.ly/1qofhaX Formalizing and verifying a modern build language] Coq
+
# [http://bit.ly/1qofhaX Formalizing and verifying a modern build language] Coq
* [http://bit.ly/1fZvxXb A hybrid TM for Haskell] Haskell
+
# [http://bit.ly/1fZvxXb A hybrid TM for Haskell] Haskell
* [http://bit.ly/1nbznGs Tiled polymorphic temporal media. (A functional pearl)] Haskell
+
# [http://bit.ly/1nbznGs Tiled polymorphic temporal media. (A functional pearl)] Haskell
* [http://bit.ly/1fhORn5 A seamless, client-centric programming model for type safe web applications] Haskell
+
# [http://bit.ly/1fhORn5 A seamless, client-centric programming model for type safe web applications] Haskell
* [http://bit.ly/1cNS752 Defunctionalizing push arrays] Haskell
+
# [http://bit.ly/1cNS752 Defunctionalizing push arrays] Haskell
* [http://bit.ly/1lnm1lF Natural language reasoning using proof-assistant technology: Rich typing and beyond] Coq
+
# [http://bit.ly/1lnm1lF Natural language reasoning using proof-assistant technology: Rich typing and beyond] Coq
* [http://bit.ly/NSSkOk Intro to Haskell for Erlangers] Haskell
+
# [http://bit.ly/NSSkOk Intro to Haskell for Erlangers] Haskell
* [http://bit.ly/1gnmqQW Haskell for OCaml programmers] Haskell OCaml
+
# [http://bit.ly/1gnmqQW Haskell for OCaml programmers] Haskell OCaml
* [http://t.co/ygGkw5SmCj Programming and reasoning with side-effects in Idris] Idris
+
# [http://t.co/ygGkw5SmCj Programming and reasoning with side-effects in Idris] Idris
* [http://bit.ly/1qBKbwO Créatúr: Framework for artificial life and other evolutionary algorithms] Haskell
+
# [http://bit.ly/1qBKbwO Créatúr: Framework for artificial life and other evolutionary algorithms] Haskell
* [http://bit.ly/1qBMxM0 Why Haskell is important for research, Part 1 of n] Haskell
+
# [http://bit.ly/1qBMxM0 Why Haskell is important for research, Part 1 of n] Haskell
* [http://bit.ly/1qBNrZ1 Programming with finite fields] Python
+
# [http://bit.ly/1qBNrZ1 Programming with finite fields] Python
* [http://bit.ly/1qBO98H Improving readability with the Maybe Foldable instance] Haskell
+
# [http://bit.ly/1qBO98H Improving readability with the Maybe Foldable instance] Haskell
* [http://bit.ly/1d8JT7x Probabilistic noninterference] Isabelle
+
# [http://bit.ly/1d8JT7x Probabilistic noninterference] Isabelle
* [http://bit.ly/1d8KIgS Mechanization of the Algebra for Wireless Networks (AWN)] Isabelle
+
# [http://bit.ly/1d8KIgS Mechanization of the Algebra for Wireless Networks (AWN)] Isabelle
* [http://bit.ly/OpChHX Haskell for Coq programmers] Haskell Coq
+
# [http://bit.ly/OpChHX Haskell for Coq programmers] Haskell Coq
* [http://bit.ly/OpHM9M An introduction to recursion schemes and codata] Haskell
+
# [http://bit.ly/OpHM9M An introduction to recursion schemes and codata] Haskell
* [http://bit.ly/1cTDJ0s Formal analysis of optical systems] HOL_Light
+
# [http://bit.ly/1cTDJ0s Formal analysis of optical systems] HOL_Light
* [http://bit.ly/1d93HNK Formally verified computation of enclosures of solutions of ordinary differential equations] Isabelle
+
# [http://bit.ly/1d93HNK Formally verified computation of enclosures of solutions of ordinary differential equations] Isabelle
* [http://bit.ly/1gIpBCN Verifying security policies using host attributes] Isabelle
+
# [http://bit.ly/1gIpBCN Verifying security policies using host attributes] Isabelle
* [http://bit.ly/1iwrUvQ aspeed: Solver scheduling via Answer Set Programming] ASP
+
# [http://bit.ly/1iwrUvQ aspeed: Solver scheduling via Answer Set Programming] ASP
* [http://bit.ly/1gNMUez A brief introduction to Haskell, and why it matters] Haskell
+
# [http://bit.ly/1gNMUez A brief introduction to Haskell, and why it matters] Haskell
* [http://bit.ly/1mj7v1Q Monoid morphisms, products, and coproducts] Scala
+
# [http://bit.ly/1mj7v1Q Monoid morphisms, products, and coproducts] Scala
* [http://bit.ly/1mjatmK Interactive tutorial of the sequent calculus] Enseñanza
+
# [http://bit.ly/1mjatmK Interactive tutorial of the sequent calculus] Enseñanza
* [http://bit.ly/ODpamB Bayesian analysis: A conjugate prior and Markov chain Monte Carlo] Haskell
+
# [http://bit.ly/ODpamB Bayesian analysis: A conjugate prior and Markov chain Monte Carlo] Haskell
* [http://bit.ly/OJsn3X Cantor's diagonal argument in Agda] Agda
+
# [http://bit.ly/OJsn3X Cantor's diagonal argument in Agda] Agda
* [http://bit.ly/1h52eDJ H2048: A Haskell implementation of game 2048] Haskell
+
# [http://bit.ly/1h52eDJ H2048: A Haskell implementation of game 2048] Haskell
* [http://bit.ly/1h536bt Haskell in the browser: setting up Yesod and Fay] Haskell
+
# [http://bit.ly/1h536bt Haskell in the browser: setting up Yesod and Fay] Haskell
* [http://bit.ly/1eAD2HO Presentation of Haskell in the Hackerspace Trento] Haskell
+
# [http://bit.ly/1eAD2HO Presentation of Haskell in the Hackerspace Trento] Haskell
* [http://bit.ly/1eADVQG Teach yourself logic: A study guide. Version 10.0 (20 March 2014] Libro
+
# [http://bit.ly/1eADVQG Teach yourself logic: A study guide. Version 10.0 (20 March 2014] Libro
* [http://bit.ly/1dfdjq3 Haskell from C: Where are the for Loops] Haskell
+
# [http://bit.ly/1dfdjq3 Haskell from C: Where are the for Loops] Haskell
* [http://bit.ly/1dfeOVj What's wrong with the for loop] Haskell
+
# [http://bit.ly/1dfeOVj What's wrong with the for loop] Haskell
* [http://bit.ly/1iRyOwZ Why learn Haskell] Haskell
+
# [http://bit.ly/1iRyOwZ Why learn Haskell] Haskell
* [http://bit.ly/1iRBZos Algorithme de Babylone : une boucle sous toutes ses formes] Haskell
+
# [http://bit.ly/1iRBZos Algorithme de Babylone : une boucle sous toutes ses formes] Haskell
* [http://bit.ly/1iRDXW1 Discrétisation d'équations différentielles] Haskell
+
# [http://bit.ly/1iRDXW1 Discrétisation d'équations différentielles] Haskell
* [http://bit.ly/1iRG8ss Au delà des réels: méthodes numériques en informatique] Haskell
+
# [http://bit.ly/1iRG8ss Au delà des réels: méthodes numériques en informatique] Haskell
* [http://bit.ly/1iRHmnB Polynômes de Taylor: graphiques et animations] Haskell
+
# [http://bit.ly/1iRHmnB Polynômes de Taylor: graphiques et animations] Haskell
* [http://bit.ly/1iRIlEv Méthode de Briggs et de Héron avec MPFR via Haskell et Sage] Haskell Sage
+
# [http://bit.ly/1iRIlEv Méthode de Briggs et de Héron avec MPFR via Haskell et Sage] Haskell Sage
* [http://bit.ly/1iRISpM Gauss par tête et queue] Haskell
+
# [http://bit.ly/1iRISpM Gauss par tête et queue] Haskell
* [http://bit.ly/1iRJpbt Z/nZ sans arithmétique modulaire ...] Haskell
+
# [http://bit.ly/1iRJpbt Z/nZ sans arithmétique modulaire ...] Haskell
* [http://bit.ly/1gg0LOR Algèbre et informatique] Haskell
+
# [http://bit.ly/1gg0LOR Algèbre et informatique] Haskell
* [http://bit.ly/1gg1EXB Programmation fonctionnelle et Haskell for dummies] Haskell
+
# [http://bit.ly/1gg1EXB Programmation fonctionnelle et Haskell for dummies] Haskell
* [http://bit.ly/1gg200o Relations binaires et fonctions avec Haskell] Haskell
+
# [http://bit.ly/1gg200o Relations binaires et fonctions avec Haskell] Haskell
* [http://bit.ly/1gg2ljD Poker en Haskell] Haskell
+
# [http://bit.ly/1gg2ljD Poker en Haskell] Haskell
* [http://bit.ly/1gg2Fix Logique des propositions en Haskell part I] Haskell
+
# [http://bit.ly/1gg2Fix Logique des propositions en Haskell part I] Haskell
* [http://bit.ly/1gg358l Mathématique discrète et informatique] Libro Haskell
+
# [http://bit.ly/1gg358l Mathématique discrète et informatique] Libro Haskell
* [http://bit.ly/1gg5mk7 Calcul mathématique avec Sage] Libro Sage
+
# [http://bit.ly/1gg5mk7 Calcul mathématique avec Sage] Libro Sage
 
* Th[http://bit.ly/1ju03fL e power algorithm] Haskell PHP
 
* Th[http://bit.ly/1ju03fL e power algorithm] Haskell PHP
* [http://bit.ly/1gu02KX Modeling and verification of distributed algorithms in theorem proving environments] Isabelle
+
# [http://bit.ly/1gu02KX Modeling and verification of distributed algorithms in theorem proving environments] Isabelle
* [http://bit.ly/1h1BGqv Directed security policies: A stateful network implementation] Isabelle
+
# [http://bit.ly/1h1BGqv Directed security policies: A stateful network implementation] Isabelle
* [http://bit.ly/1hUHbW4 John McCarthy – Father of Artificial Intelligence] Historia
+
# [http://bit.ly/1hUHbW4 John McCarthy – Father of Artificial Intelligence] Historia
* [http://bit.ly/P1C0Lr What it’s like to use Haskell] Haskell
+
# [http://bit.ly/P1C0Lr What it’s like to use Haskell] Haskell
* [http://bit.ly/1g1xd2v Brutal [meta]introduction to dependent types in Agda] Agda
+
# [http://bit.ly/1g1xd2v Brutal [meta]introduction to dependent types in Agda] Agda
 
* Estructurando y consultando información en grafos. ~ Fernando Sancho http://bit.ly/1g1y6It Grafos Redes_complejas
 
* Estructurando y consultando información en grafos. ~ Fernando Sancho http://bit.ly/1g1y6It Grafos Redes_complejas
* [http://bit.ly/1mvpphW Résolution dichotomique de f(x)=0] Haskell
+
# [http://bit.ly/1mvpphW Résolution dichotomique de f(x)=0] Haskell
* [http://bit.ly/1mvqB4P Colección de problemas sobre inteligencia artificial] Libro IA
+
# [http://bit.ly/1mvqB4P Colección de problemas sobre inteligencia artificial] Libro IA
* [http://bit.ly/1jNDTVZ Monaris: A tetris clone written in Haskell using free-game] Haskell
+
# [http://bit.ly/1jNDTVZ Monaris: A tetris clone written in Haskell using free-game] Haskell
* [http://bit.ly/1m7vqOF Formal proof of the fundamental theorem of decorated interval arithmetic] Tesis Coq
+
# [http://bit.ly/1m7vqOF Formal proof of the fundamental theorem of decorated interval arithmetic] Tesis Coq
* [http://bit.ly/1l7Hgs9 Library to calculate Gröbner basis written in Haskell] Haskell
+
# [http://bit.ly/1l7Hgs9 Library to calculate Gröbner basis written in Haskell] Haskell
* [http://bit.ly/1rJz2dM Introduction à l’algorithmique et à la programmation avec Python] Python
+
# [http://bit.ly/1rJz2dM Introduction à l’algorithmique et à la programmation avec Python] Python
* [http://bit.ly/1pB7KSV Algorithmic problem solving with Python] Libro Python
+
# [http://bit.ly/1pB7KSV Algorithmic problem solving with Python] Libro Python
* [http://bit.ly/1frwPek Computational discrete mathematics with Python] Libro Python
+
# [http://bit.ly/1frwPek Computational discrete mathematics with Python] Libro Python
* [http://bit.ly/1gBJyQ7 Formally verified mathematics] Divulgación
+
# [http://bit.ly/1gBJyQ7 Formally verified mathematics] Divulgación
* [http://bit.ly/1gBKJyY Towards a formally verified proof assistant] Coq Nuprl
+
# [http://bit.ly/1gBKJyY Towards a formally verified proof assistant] Coq Nuprl
* [http://bit.ly/1mAtH7J Formalization of a dynamic logic for graph transformation in the Coq proof assistant] Coq
+
# [http://bit.ly/1mAtH7J Formalization of a dynamic logic for graph transformation in the Coq proof assistant] Coq
* [http://bit.ly/1h63p56 Interactive simplifier tracing and debugging in Isabelle] Isabelle
+
# [http://bit.ly/1h63p56 Interactive simplifier tracing and debugging in Isabelle] Isabelle

Revisión del 17:13 30 mar 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
  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