Lecturas del año 2014

De WikiGLC

Saltar a: navegación, buscar

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
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

Obtenido de «https://www.glc.us.es/web/index.php?title=Lecturas_del_año_2014&oldid=1232»