Lecturas del año 2014
Revisión del 18:13 30 mar 2014 de Jalonso (discusión | contribuciones) (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...»)
Lecturas de enero de 2014
- Lecture notes on the lambda calculus LC
- Turing machines and undecidability Computabilidad
- The SageMath Cloud: Python and computational mathematics in the cloud Sage Python
- EasyAI: a pure-Python artificial intelligence framework for two-players abstract games such as Tic Tac Toe IA Python
- A whirlwind tour of combinatorial games in Haskell Haskell
- Semantics-directed machine architecture in ReWire Haskell
- Formal analysis of the Kerberos authentication protocol with PVS PVS
- Running Makefiles with Shake Haskell
- Free Sage math cloud - Python and symbolic math Sage Python
- Typed syntactic meta-programming Agda
- Modular type-safety proofs in Agda Agda
- IsarMathLib (A library of formalized mathematics for Isabelle/ZF theorem proving environment) 1.9.1 released Isabelle
- Experimental library of univalent formalization of mathematics HoTT Coq
- A gentle guide to constraint logic programming via ECLiPSe (Third edition, 2014) Libro Prolog
- Laziness is a virtue: an introduction to functional programming in Haskell Haskell
- Dijkstra on Haskell and Java Haskell
- The "ideal" mathematician Divulgación
- Applications of the Gauss-Jordan algorithm, done right. Isabelle
- Verifying document confidentiality of a conference management system. Isabelle
- Coinitial semantics for redecoration of triangular matrices Coq
- Bidirectional proof search procedure for intuitionistic modal logic IS5 Coq
- Axiom selection as a machine learning problem Isabelle ML
- Squiggoling with bialgebras (Recursion schemes from comonads revisited) Haskell
- aspeed: Solver scheduling via answer set programming ASP
- Principles of imperative computation (and methods for ensuring the correctness of programs Curso Algorítmica
- Automatic functional harmonic analysis Haskell
- Proof-by-instance for embedded network design (From prototype to tool roadmap) Isabelle
- Verifying weight biased leftist heaps using dependent types Agda
- Abstract interpretation using laziness: Proving Conway’s lost cosmological theorem Haskell
- Recurrence and induction Divulgación
- Backpack: Retrofitting Haskell with interfaces Haskell
- Combining proofs and programs in a dependently typed language Coq
- A trusted mechanised JavaScript specification Coq
- A verified information-flow architecture Coq
- CakeML: A verified implementation of ML HOL4
- Probabilistic relational verification for cryptographic implementations Coq
- Freeze after writing (Quasi-deterministic parallel programming with LVars) Haskell
- Modular, higher-order cardinality analysis in theory and practice Haskell
- Profiling for laziness Racket
- Modular reasoning about heap paths via effectively propositional formulas SMT Z3
- Monadic combinators for "putback" style bidirectional programming Haskell
- The HERMIT in the stream (Fusing stream fusion’s concatMap) Haskell
- Haskell applicative tutorial: a small tutorial, showing how you can use functors and applicatives Haskell
- MuCheck : An extensible tool for mutation testing of Haskell programs Haskell
- A DSL for describing the artificial intelligence in real-time video games Haskell
- Shortcut fusion for pipes Haskell
- La sucesión de Kolakoski Haskell
- Verifying chinese train control system under a combined scenario by theorem proving Isabelle
- Featherweight OCL: A proposal for a machine-checked formal semantics for OCL 2.5 Isabelle
- La conjetura de Gilbreath en Haskell Haskell
- Certifying algorithms Verificación
- Codificación por longitud en Haskell Haskell
- El triángulo de Pascal en Haskell Haskell
- Lista de factoriales perezosa en Haskell Haskell
- Sucesión de Fibonacci, evaluación perezosa y números construibles Haskell
- Memorabilia Mathematica (or the philomath’s quotation-book) Libro
- Codificación por longitud en Haskell Haskell
- Two case studies in proving with side-effects: Gödel's and Kripke's completeness theorems Agda Coq
- Fixing bugs in "Computing Homology" Python
- Formal verification, interactive theorem proving, and automated reasoning Divulgación
- Specification and verification of concurrent programs through refinements ACL2
- A formally verified generic branching algorithm for global optimization PVS
- Distributed call-by-value machines Agda
- Twenty years of theorem proving for HOLs (Past, present and future) Historia
- Clasificación supervisada y no supervisada IA AA
- El juego de Oslo en Haskell Haskell
- Inductive triple graphs: A purely functional approach to represent RDF Haskell Scala
- Formalizing the Kleene star for square matrices Isabelle
- Números triangulares y sus propiedades en Haskell Haskell
- Mathematics in the age of the Turing machine Divulgación
- Lecture notes on type theory Libro
- A new type of Mathematics? New discoveries expand the scope of computer-assisted proofs of theorems Divulgación
- Algorithms Libro Algorítmica
- Balancing lists: a proof pearl. Isabelle
- Bases de datos en grafo IA
Lecturas de febrero de 2014
- Alan Turing and the origins of complexity Historia
- On Turing’s legacy in mathematical logic and the foundations of mathematics Historia
- A survey of axiom selection as a machine learning problem Isabelle
- Eilenberg-MacLane spaces in homotopy type theory Agda
- Interactive SICP (Structure and Interpretation of Computer Programs) Libro Scheme
- A heuristic prover for real inequalities AR
- Arbitrary fun: Generating user profiles with QuickCheck Haskell QuickCheck
- A little lens starter tutorial Haskell
- Números poligonales y sus propiedades en Haskell Haskell
- El triángulo de Floyd en Haskell. http://bit.ly/1nRULh Haskell
- Solving a regular expression crossword with Haskell, Part 2: Representation. Haskell
- Basics of λ-calculus LC
- Verification of certifying computations through AutoCorres and Simpl Isabelle
- Implementing, and understanding type classes Haskell
- Survey of Satisfiability Modulo Theories (SMT) SAT SMT
- OTTER proofs of theorems in Tarskian geometry OTTER
- Air traffic controller shift scheduling by reduction to CSP, SAT and SAT-related problems SAT SMT
- Laplace’s equation in Haskell: Using a DSL for stencils Haskell
- A test driven haskell course Curso Haskell
- Logic, languages and programming Haskell
- New draft of Haskell School of Music (PDF) Libro Haskell
- Properties of random graphs - subgraph containment. Isabelle
- Monad transformers for backtracking search Haskell SAT
- A survey of axiom selection as a machine learning problem. Isabelle
- Proof-by-instance for embedded network design (From prototype to tool roadmap). Isabelle
- A mathematical proof too long to check - The Erdos discrepancy conjecture SAT
- Formalised mathematics Agda
- Coinitial semantics for redecoration of triangular matrices. Coq
- Rank nullity theorem of linear algebra Isabelle
- A brief intro to QuickCheck Haskell QuickCheck
- Complexity & verification: The history of programming as problem solving Tesis Historia
- A denotational semantics for natural language query interfaces to semantic web triplestores Haskell
- Learning-assisted theorem proving with millions of lemmas IA AR ML
- Thesis: formal study of efficient algorithms in linear algebra Tesis Coq
- A tutorial on using the Aeson packaged to parse JSON data Haskell
- A tutorial on the attoparsec parsing package Haskell
- Ejercicios sobre definiciones con unfoldr Haskell
- Haskell: A whirlwind tour (Part 1) Haskell
- Comprehensive formal verification of an OS microkernel Isabelle Haskell
- A Cretan maze using Haskell Diagrams Haskell
- Comparing Haskell Web frameworks Haskell
- What is formalized Mathematics Divulgación
- Random numbers in Haskell Haskell
- Coin change Haskell
- Simple examples. Haskell Haskell
- Example of why to use monads - what they can do Haskell
- Solution counting Haskell
- Polynomials: Library for polynomials Haskell
- Root finding Haskell
- Simple interpolation Haskell
- Infinite subsets of natural numbers Haskell
- An introduction to QuickCheck testing Haskell
- Shortest path: Floyd-Warshall algorithm in Haskell Haskell
- Knapsack - Brute force in Haskell Haskell
- Automated and (formally) certified proofs of summation formulae Coq
- Induction and logical relations Agda
- Problema de Ramanujan de radicales anidados. Haskell
- Sucesiones auto descriptivas en Haskell. Haskell
- Proof assistant based on didactic considerations. Enseñanza ANDY
- A fully automatic problem solver with human-style output
- Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. PVS
- Formalizing Moessner’s theorem and generalizations in Nuprl. Nuprl
- Preservation of Lyapunov-theoretic proofs: From real to floating-point arithmetic Coq
- A mechanized proof of loop freedom of the (untimed) AODV routing protocol Isabelle
- Showing invariance compositionally for a process algebra of network protocols Isabelle
Lecturas de marzo de 2014
- Interaction entre algèbre linéaire et analyse en formalisation des mathématiques Tesis Coq
- A Haskell-implementation of STM Haskell with early conflict detection Haskell
- Mutation testing of functional programming languages Haskell
- Harnessing constraint programming for poetry composition ASP
- Formalization of binary fields and n-dimensional binary vector spaces using the Mizar proof checker Mizar
- Content development for distance education in advanced university mathematics using Mizar Mizar
- Computers, maths and minds
- Learning Agda to be a better Haskell programmer Haskell Agda
- Learning Prolog to be a better Haskell programmer Haskell Prolog
- Fun with functional dependencies (or (draft) types as values in static computations in Haskell) Haskell
- Fun with type functions (version 3) Haskell
- Data.Map vs Data.IntMap Haskell
- Multi-line strings in Haskell Haskell
- Data.Typeable and Data.Dynamic in Haskell Haskell
- Implementing Union-Find algorithms in Haskell Haskell
- Calling C library functions dynamically in Haskell Haskell
- Implementing a JIT compiled language with Haskell and LLVM Haskell
- Switching from monads to applicative functors Haskell
- The power of lazy evaluation Haskell
- How to replace failure by a list of successes Haskell
- Using string literal for symbols Haskell
- Parsing arithmetic expressions with Parsec Haskell
- An ACL2 mechanization of an axiomatic weak memory model ACL2
- From zipper to lens Haskell
- Auto in Agda (Programming proof search) Agda
- Introducción a las redes complejas IA
- Lógica de enunciados Libro Lógica
- Lógica de predicados Libro Lógica
- Teoría de conjuntos básica (Conjuntos, relaciones y funciones) Libro Lógica
- A brief introduction to Haskell, and why it matters Haskell
- Haskell cheat sheets (Part 1) Haskell
- Hspec: Behavior-driven development for Haskell
Haskell BDD - Free applicative functors Haskell
- Algebraic and analytic programming
Haskell Math - Lógica y álgebra de Boole
Libro Lógica - LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration Haskell
- Transparencias del curso "Algoritmia básica" Algorítmica
- Transparencias del curso "Algoritmia para problemas difíciles" Algorítmica
- Formalizing and verifying a modern build language Coq
- A hybrid TM for Haskell Haskell
- Tiled polymorphic temporal media. (A functional pearl) Haskell
- A seamless, client-centric programming model for type safe web applications Haskell
- Defunctionalizing push arrays Haskell
- Natural language reasoning using proof-assistant technology: Rich typing and beyond Coq
- Intro to Haskell for Erlangers Haskell
- Haskell for OCaml programmers Haskell OCaml
- Programming and reasoning with side-effects in Idris Idris
- Créatúr: Framework for artificial life and other evolutionary algorithms Haskell
- Why Haskell is important for research, Part 1 of n Haskell
- Programming with finite fields Python
- Improving readability with the Maybe Foldable instance Haskell
- Probabilistic noninterference Isabelle
- Mechanization of the Algebra for Wireless Networks (AWN) Isabelle
- Haskell for Coq programmers Haskell Coq
- An introduction to recursion schemes and codata Haskell
- Formal analysis of optical systems HOL_Light
- Formally verified computation of enclosures of solutions of ordinary differential equations Isabelle
- Verifying security policies using host attributes Isabelle
- aspeed: Solver scheduling via Answer Set Programming ASP
- A brief introduction to Haskell, and why it matters Haskell
- Monoid morphisms, products, and coproducts Scala
- Interactive tutorial of the sequent calculus Enseñanza
- Bayesian analysis: A conjugate prior and Markov chain Monte Carlo Haskell
- Cantor's diagonal argument in Agda Agda
- H2048: A Haskell implementation of game 2048 Haskell
- Haskell in the browser: setting up Yesod and Fay Haskell
- Presentation of Haskell in the Hackerspace Trento Haskell
- Teach yourself logic: A study guide. Version 10.0 (20 March 2014 Libro
- Haskell from C: Where are the for Loops Haskell
- What's wrong with the for loop Haskell
- Why learn Haskell Haskell
- Algorithme de Babylone : une boucle sous toutes ses formes Haskell
- Discrétisation d'équations différentielles Haskell
- Au delà des réels: méthodes numériques en informatique Haskell
- Polynômes de Taylor: graphiques et animations Haskell
- Méthode de Briggs et de Héron avec MPFR via Haskell et Sage Haskell Sage
- Gauss par tête et queue Haskell
- Z/nZ sans arithmétique modulaire ... Haskell
- Algèbre et informatique Haskell
- Programmation fonctionnelle et Haskell for dummies Haskell
- Relations binaires et fonctions avec Haskell Haskell
- Poker en Haskell Haskell
- Logique des propositions en Haskell part I Haskell
- Mathématique discrète et informatique Libro Haskell
- Calcul mathématique avec Sage Libro Sage
- The power algorithm Haskell PHP
- Modeling and verification of distributed algorithms in theorem proving environments Isabelle
- Directed security policies: A stateful network implementation Isabelle
- John McCarthy – Father of Artificial Intelligence Historia
- What it’s like to use Haskell Haskell
- Brutal [metaintroduction to dependent types in Agda] Agda
- Estructurando y consultando información en grafos. ~ Fernando Sancho http://bit.ly/1g1y6It Grafos Redes_complejas
- Résolution dichotomique de f(x)=0 Haskell
- Colección de problemas sobre inteligencia artificial Libro IA
- Monaris: A tetris clone written in Haskell using free-game Haskell
- Formal proof of the fundamental theorem of decorated interval arithmetic Tesis Coq
- Library to calculate Gröbner basis written in Haskell Haskell
- Introduction à l’algorithmique et à la programmation avec Python Python
- Algorithmic problem solving with Python Libro Python
- Computational discrete mathematics with Python Libro Python
- Formally verified mathematics Divulgación
- Towards a formally verified proof assistant Coq Nuprl
- Formalization of a dynamic logic for graph transformation in the Coq proof assistant Coq
- Interactive simplifier tracing and debugging in Isabelle Isabelle
