Diferencia entre revisiones de «Lecturas del año 2014»
(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/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/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/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/1eyCorP Running Makefiles with Shake] Haskell | |
− | + | # [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/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/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/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/1kupMZT The "ideal" mathematician] Divulgación | |
− | + | # [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/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/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/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/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/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/Slaark Recurrence and induction] Divulgación | |
− | + | # [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/1mg0Vom A trusted mechanised JavaScript specification] 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/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/1kLWk1R Modular, higher-order cardinality analysis in theory and practice] Haskell | |
− | + | # [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/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/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/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/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/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/tuVSiL Certifying algorithms] Verificación | |
− | + | # [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/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/1dQFPh6 Memorabilia Mathematica (or the philomath’s quotation-book)] Libro | |
− | + | # [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/1hswudC Fixing bugs in "Computing Homology"] Python | |
− | + | # [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://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/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/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/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/1baWRRr Mathematics in the age of the Turing machine] Divulgación | |
− | + | # [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/1kidLDr Algorithms] Libro Algorítmica | |
− | + | # [http://arxiv.org/abs/1401.7886 Balancing lists: a proof pearl]. Isabelle | |
− | + | # [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/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/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/1cIRixz A heuristic prover for real inequalities] AR | |
− | + | # [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/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/1dqWdix Solving a regular expression crossword with Haskell, Part 2: Representation.] Haskell | |
− | + | # [http://bit.ly/1dqXlCE Basics of λ-calculus] LC | |
− | + | # [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/1aTwaG4 Survey of Satisfiability Modulo Theories (SMT)] SAT SMT | |
− | + | # [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/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/1gNOr5Z Logic, languages and programming] 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://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/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/1mtutEf Formalised mathematics] Agda | |
− | + | # [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/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/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/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/1h9MsdF A tutorial on the attoparsec parsing package] Haskell | |
− | + | # [http://bit.ly/1h9QT8j Ejercicios sobre definiciones con unfoldr] 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/1eteufH A Cretan maze using Haskell Diagrams] Haskell | |
− | + | # [http://bit.ly/1eteTyA Comparing Haskell Web frameworks] Haskell | |
− | + | # [http://bit.ly/1hP6Kwm What is formalized Mathematics] Divulgación | |
− | + | # [http://bit.ly/NzEGPy Random numbers in Haskell] Haskell | |
− | + | # [http://bit.ly/NzF7tn Coin change] 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/NzIlgo Solution counting] Haskell | |
− | + | # [http://bit.ly/NzIPmD Polynomials: Library for polynomials] Haskell | |
− | + | # [http://bit.ly/NzJuog Root finding] Haskell | |
− | + | # [http://bit.ly/NzJG6Y Simple interpolation] Haskell | |
− | + | # [http://bit.ly/NzJYe6 Infinite subsets of natural numbers] 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/NzZLto Knapsack - Brute force in Haskell] Haskell | |
− | + | # [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/18LQNvH Problema de Ramanujan de radicales anidados]. 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://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://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/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 | |
== 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/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/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/Ng8SiZ Content development for distance education in advanced university mathematics using Mizar] Mizar | |
− | + | # [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/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/1eJX17u Fun with type functions (version 3)] Haskell | |
− | + | # [http://bit.ly/1eJXoyI Data.Map vs Data.IntMap] 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/1eJZ0J0 Implementing Union-Find algorithms 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/1eK1oiM Switching from monads to applicative functors] 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/1eK3pM6 Using string literal for symbols] 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/1i3Jo1E From zipper to lens] Haskell | |
− | + | # [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/1gP0EH5 Lógica de enunciados] 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/1cHRkCw A brief introduction to Haskell, and why it matters] 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/1liXbDq Free applicative functors] Haskell | |
− | + | # [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/1liZ0jZ LogicGrowsOnTrees: a parallel implementation of logic programming using distributed tree exploration] Haskell | |
− | + | # [http://bit.ly/1fPv5AB Transparencias del curso "Algoritmia básica"] Algorítmica | |
− | + | # [http://bit.ly/1kGJGAs Transparencias del curso "Algoritmia para problemas difíciles"] Algorítmica | |
− | + | # [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/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/1cNS752 Defunctionalizing push arrays] Haskell | |
− | + | # [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/1gnmqQW Haskell for OCaml programmers] Haskell OCaml | |
− | + | # [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/1qBMxM0 Why Haskell is important for research, Part 1 of n] Haskell | |
− | + | # [http://bit.ly/1qBNrZ1 Programming with finite fields] Python | |
− | + | # [http://bit.ly/1qBO98H Improving readability with the Maybe Foldable instance] Haskell | |
− | + | # [http://bit.ly/1d8JT7x Probabilistic noninterference] 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/OpHM9M An introduction to recursion schemes and codata] Haskell | |
− | + | # [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/1gIpBCN Verifying security policies using host attributes] Isabelle | |
− | + | # [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/1mj7v1Q Monoid morphisms, products, and coproducts] Scala | |
− | + | # [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/OJsn3X Cantor's diagonal argument in Agda] Agda | |
− | + | # [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/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/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/1iRyOwZ Why learn Haskell] 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/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/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/1iRJpbt Z/nZ sans arithmétique modulaire ...] Haskell | |
− | + | # [http://bit.ly/1gg0LOR Algèbre et informatique] 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/1gg2ljD Poker en Haskell] 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/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/1h1BGqv Directed security policies: A stateful network implementation] Isabelle | |
− | + | # [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/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/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/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/1rJz2dM Introduction à l’algorithmique et à la programmation avec Python] 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/1gBJyQ7 Formally verified mathematics] Divulgación | |
− | + | # [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/1h63p56 Interactive simplifier tracing and debugging in Isabelle] Isabelle |
Revisión del 17:13 30 mar 2014
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