Lecturas del año 2011 - Historial de revisiones

Jalonso en 05:16 28 abr 2013

2013-04-28T05:16:21Z

Mostrar los cambios

Jalonso en 17:39 27 abr 2013

2013-04-27T17:39:01Z

Jalonso: /* Lecturas de Enero de 2011 */

2013-04-27T17:25:51Z

‎Lecturas de Enero de 2011

Jalonso: New page: == Lecturas de Enero de 2011 == * [http://goo.gl/95csF Does Godel's theorem matter to mathematics?] * [http://goo.gl/LBsyx Distributed SAT]. #SAT * [http://posgrado.escom.ipn.mx/bibliotec...

2013-04-27T17:25:02Z

New page: == Lecturas de Enero de 2011 == * [http://goo.gl/95csF Does Godel's theorem matter to mathematics?] * [http://goo.gl/LBsyx Distributed SAT]. #SAT * [http://posgrado.escom.ipn.mx/bibliotec...

Página nueva

== Lecturas de Enero de 2011 ==
* [http://goo.gl/95csF Does Godel's theorem matter to mathematics?]
* [http://goo.gl/LBsyx Distributed SAT]. #SAT
* [http://posgrado.escom.ipn.mx/biblioteca/Semantic%20web%20reasoners%20and%20languages.pdf Semantic web reasoners and languages] #WS
* [http://bit.ly/emHhvZ El 2011 y los números primos (en Haskell)] #Haskell #V
* [http://bit.ly/ebNi54 The dialectica interpertation in Coq] #Coq
* [http://bit.ly/heSTJJ Errores aritméticos en Haskell y en Lisp] #Haskell #Lisp #V
* [http://bit.ly/gLU60K Why Lisp is a big hack (and Haskell is doomed to succeed)] #Lisp #Haskell
* [http://bit.ly/h5v14x ProofWiki y la verificación de las demostraciones matemáticas] #Verificación #MKM #V
* [http://bit.ly/fMi9V7 A quick and gentle guide to constraint logic programming via ECLiPSe] #PL #Restricciones
* [http://bit.ly/gb4Dn9 A language for mathematical knowledge management] #MKM
* [http://bit.ly/eLkbsW Automated inference of finite unsatisfiability] #AR
* [http://bit.ly/evywxv The free vector space on a type]. #Haskell
* [http://goo.gl/6t8YI Formal methods applied to a floating-point number system] #Z
* [http://goo.gl/WT6G3 A machine-checked theory of floating point arithmetic] #HOL_Light
* [http://goo.gl/k6NJJ Formal verification of floating point trigonometric functions] #HOL_Light
* [http://goo.gl/RRb7p A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon TM processor] #ACL2
* [http://goo.gl/gvh4C A generic library for floating-point numbers and its application to exact computing] #Coq.
* [http://goo.gl/oEgxU A high-level formalization of floating-point numbers in PVS] #PVS
* [http://goo.gl/4CHMF Formal verification of floating-point programs] #Coq
* [http://goo.gl/W9svV The pitfalls of verifying floating-point computations] #Verificación
* [http://goo.gl/xs5IG Floats and ropes: A case study for formal numerical program verification] #Coq.
* [http://bit.ly/grfNfD Algorithms take control of Wall Street] #IA
* [http://bit.ly/gC0m7p Formal reliability analysis of combinational circuits using theorem proving] #HOL
* [http://bit.ly/f8Nvpv Determinación, esperanza y éxitos en la resolución de problemas] #Enseñanza #V
* [http://bit.ly/gZYKNJ Lectures in game theory for computer scientists] #Libro
* [http://bit.ly/dNvlXU Reactive valuations] #TFM
* [http://slidesha.re/f8SKgI

+ Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet] Algunas aplicaciones de las bases de Groebner http://bit.ly/haeTax
* [http://bit.ly/hrwBXD Programación funcional con Haskell] #Libro #Haskell
* [http://bit.ly/eGqBDZ Certifying compilers using higher-order theorem provers as certificate checker] #Isabelle #Coq
* [http://bit.ly/ht6544 El tipo abstracto de datos de las colas en Haskell] #Haskell #V

== Lecturas de Febrero de 2011 ==
* [http://bit.ly/eZiRVL Deducción natural en lógica proposicional con Isabelle/Isar] #Isabelle #V
* [http://bit.ly/hTYRXf Deducción natural en lógica de primer orden con Isabelle/Isar] #Isabelle #V
* [http://bit.ly/h2co0D

+ fKenzo: A user interface for computations in Algebraic Topology]
* [http://bit.ly/hZdkPN A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL]. #Isabelle
* [http://bit.ly/gcvJNz El tipo abstracto de datos de las colas de prioridad en Haskell] #Haskell #V
* [http://bit.ly/epypbt Program verification and functioning of operative computing revisited: How about mathematics engineering?] #Verificación
* [http://bit.ly/hIeQQi El próximo después de 1811] #Haskell #V
* [http://bit.ly/hWod4k Humanos más capaces y robots que están en las nubes] #IA
* [http://bit.ly/fTekAA Charming proofs: A journey into elegant mathematics] #Libro #DAO
* [http://bit.ly/fpnnu7 Functional binomial queues] #RF #Isabelle
* [http://bit.ly/glOw9x Lower semicontinuous functions] #RF #Isabelle
* [http://bit.ly/hvqHiB Lógica Informática (2010-11)] #V
* [http://bit.ly/e6TgsN Inconsistent heuristics in theory and practice] #IA
* [http://goo.gl/Igcbu On proof and progress in mathematics] #CM
* [http://bit.ly/i9FH8v Artificial intelligence (Foundations of computational agents)] #Libro #IA
* [http://bit.ly/eLUOMY Are mathematicians in Jeopardy?] #IA
* [http://bit.ly/fMVueD Give me that good old-fashioned AI] #IA
* [http://bit.ly/evZnr7 Building Watson: An overview of the deepQA project] #IA

== Lecturas de Marzo de 2011 ==
* [http://bit.ly/hJWFDv Software verification turns maintstream] #Verificación
* [http://rok.strnisa.com/thesis/thesis.pdf Formalising, improving, and reusing the Java Module System] http://bit.ly/dF68vF #Tesis #Isabelle
* [http://goo.gl/D4L3j SMT solvers: new oracles for the HOL theorem prover] #SMT #HOL4
* [http://bit.ly/e3QiRU Isabelle como un lenguaje funcional] #Isabelle #V
* [http://bit.ly/fKKC3D El tipo abstracto de datos de las pilas en Haskell] #Haskell #V
* [http://bit.ly/hBKzIz El tipo abstracto de datos de las colas en Haskell] #Haskell #V
* [http://goo.gl/oUlcY Executable transitive closures of finite relations] #RF #Isabelle
* [http://goo.gl/epNrc

+ Solución española para un problema de John Nash] Reduced Ordered Binary Decision Diagram with Implied Literals: A New knowledge Compilation Approach http://goo.gl/FoL94 #AR
* [http://bit.ly/gHpfXL Teaching FP to freshmen] #Enseñanza #PF
* [http://goo.gl/2fK3d Introduction to artificial intelligence] #Libro #IA
* [http://bit.ly/hZ9TWG La Universidad Carnegie-Mellon elimina la programación OO de su primer curso] #Enseñanza
* [http://goo.gl/NXhJI Experience report: Functional programming through deep Time (Modeling the first complex ecosystems on Earth)] #Haskell
* [http://bit.ly/eEvWOO A comparative study on ILP-based concept discovery systems] #ILP
* [http://bit.ly/gE69RT Logic-based artificial intelligence] #Libro #IA
* [http://bit.ly/f4JcZN A Formalization of the C99 Standard in HOL, Isabelle and Coq] #HOL #Isabelle #Coq
* [http://bit.ly/gQRpsr Formal methods in agent-oriented software engineering] #MF
* [http://bit.ly/hO9ewV The cognitive agents specification language and verification environment] #Verificación
* [http://bit.ly/hjBReD Software bugs and scientific progress] #Verificación
* [http://bit.ly/ffR1jT Representing model theory in a type-theoretical logical framework] #RF #Twelfe
* [http://goo.gl/vCDeE Towards a verification framework for faulty message passing systems in PVS] #PVS

== Lecturas de Abril de 2011 ==
* [http://bit.ly/g2tz4T Por qué y cómo se hace investigación en matemáticas] #CM
* [http://goo.gl/Y6pl Introduction to newLISP] #Libro #Lisp
* [http://goo.gl/23une Verified firewall policy transformations for test case generation] #Isabelle
* [http://goo.gl/bxSx7 An approach to modular and testable security models of real-world health-care applications] #Isabelle
* [http://bit.ly/fTzgF0 Psi-calculi: a framework for mobile processes with nominal data and logic] #Isabelle
* [http://goo.gl/ZAqRw Artificial intelligence and human thinking] #IA
* [http://goo.gl/aKNFv Simplification rules for intuitionistic propositional tableaux] #AR
* [http://bit.ly/e0qElc A fast and verified algorithm for proving store-and-forward networks deadlock-free] #ACL2
* [http://bit.ly/h7oESi Gestión mecanizada del conocimiento matemático en Topología algebraica] #Tesis #ACL2
* [http://bit.ly/faUvcE The first formalized math wiki is here] #MKM
* [http://bit.ly/fAt2n2 Los matemáticos no buscan resultados, van tras la belleza] #CM
* [http://bit.ly/hXvjFF Extending Sledgehammer with SMT Solvers] #Isabelle #SMT
* [http://bit.ly/eTdbPY Book of proof] #Libro #DAO
* [http://bit.ly/hTeyJl The general triangle is unique] #RF #Isabelle
* [http://bit.ly/fPmmPo NASA Formal Methods] #Libro #MF #Verificación
* [http://bit.ly/eK1u3z How to read a mathematics textbook] #Enseñanza
* [http://bit.ly/eGDE9E Haskell for the cloud] #Haskell
* [http://bit.ly/gx9OfA The opentheory standard theory library] #Verificación
* [http://bit.ly/ghnBkQ A Coq-based library for interactive and automated theorem proving in plane geometry] #RF #Coq
* [http://bit.ly/esoyE5 Mechanical support for efﬁcient dissemination on the CAN overlay network] #Isabelle
* [http://bit.ly/g0ybyb A Wiki for formal mathematics] #MKM
* [http://bit.ly/eNHWj1 Recent developments in computing and philosophy] #Prover9
* [http://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2011_Constructive.pdf Constructive formalization of classical modal logic]. #Coq
* [http://bit.ly/f7uyEs Numbers as data structures: the prime successor function as primitive] #Enseñanza
* [http://bit.ly/iYb67t Proving equality between streams] #Coq
* [http://bit.ly/dOkauQ The limits of correctness] #Verificación
* [http://bit.ly/e2aqGc A formal proof of the Riesz representation theorem] #RF #PVS
* [http://bit.ly/lXvY1G A formal proof that π₁(S¹)=Z] #RF #Coq

== Lecturas de Mayo de 2011 ==
* [http://bit.ly/f0FX0O On a strongly normalizing STG machine] #Tesis
* [http://bit.ly/hi9u3T Balancing weight-balanced trees] #Coq #Haskell
* [http://bit.ly/gDCUy0 A formal programming model of Orléans skeleton library] #Coq
* [http://bit.ly/gxGyjq Formal verification of a small real-time operating system] #Tesis #Isabelle
* [http://bit.ly/io1joM Deus ex machina]. #Prover9
* [http://bit.ly/jdhTBc Computationally-discovered simplification of the ontological argument]. #Prover9
* [http://bit.ly/eI3roc Satisfiability of acyclic and almost acyclic CNF formulas (II)] #AR
* [http://bit.ly/f9tTAC Heaps and data structures: A challenge for automated provers] #AR
* [http://bit.ly/jkEZGy Haskell: Not pure enough?] #Haskell
* [http://bit.ly/lT7IZ3 Verified stack-based genetic programming via dependent types] #RF #Agda #IA
* [http://bit.ly/lDrbjG Sorpresa sumando potencias de 2 en Haskell] #Haskell #V
* [http://bit.ly/kzKmwS A list-machine benchmark for mechanized metatheory] #AR
* [http://bit.ly/ls0jmQ The locally nameless representation] #AR
* [http://bit.ly/j1Ma1D Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem] #TFM #PVS
* [http://bit.ly/lxkECl Solving Rubik's cube using SAT solvers] #SAT
* [http://bit.ly/kU11XQ Entusiasmo, clave del buen maestro] #Enseñanza
* [http://slidesha.re/iwSxsW Programação funcional: Novos horizontes para a expansão da consciência] #PF
* [http://bit.ly/lL64ln Computer certified efficient exact reals in Coq] #Coq
* [http://bit.ly/ieX6gS Parallel and concurrent programming in Haskell] #Haskell
* [http://bit.ly/lvyAWJ TRX: A formally verified parser interpreter] #Coq
* [http://bit.ly/lgbo2i Computational meta-ethics: Towards the meta-ethical robot] #Prover9
* [http://bit.ly/j8R2cA Formal metatheory of programming languages in the Matita interactive theorem prover] #RF #Matita
* [http://bit.ly/kYxElW ALPprolog — A new logic programming method for dynamic domains] #PL
* [http://bit.ly/mBQXgl Logical formalization of semantic business vocabulary and Rules] #RC
* [http://bit.ly/illSo The proof is in the pudding (The changing nature of mathematical proof)] #Libro
* [http://goo.gl/JzUX7 Knowledge-based programs] #RF #Isabelle
* [http://bit.ly/kH7Xz7 Elegance and power] #Haskell
* [http://bit.ly/iiAhk5 Validated compilation through logic] #Verificación
* [http://bit.ly/jXmH4d Teaching computational logic: Technology-enhanced learning and animations] #Enseñanza
* [http://bit.ly/k0HycO Sigma: An integrated development environment for formal ontology] #RC
* [http://bit.ly/m3Qmr3 Termination of Isabelle functions via termination of rewriting] #AR #Isabelle
* [http://bit.ly/koQ4Ti Combining and automating classical and non-classical logics in classical higher-order logics] #AR
* [http://bit.ly/jzGZo1 Rationality and escalation in infinite extensive games] #Libro #RF #Coq

== Lecturas de Junio de 2011 ==
* [http://bit.ly/lHXxS8 Efficient interactive construction of machine-checked protocol security proofs in the context of dynamically compromising adversaries] #TFM #RF #Isabelle
* [http://bit.ly/iir2wI Specification and verification: The Spec# experience] #Verificación
* [http://bit.ly/lhybds Formal verification of chess endgames tables] #HOL4 #IA
* [http://bit.ly/l5BtTc Integrating testing and interactive theorem proving] #ACL2
* [http://bit.ly/l5gjtf Conway’s games and some of their basic properties] #Mizar
* [http://bit.ly/jZeiPa A verified runtime for a verified theorem prover] #HOL4
* [http://bit.ly/jnkpNT Modelling distributed cognition systems in PVS] #PVS
* [http://bit.ly/kuY9Ad Three chapters of measure theory in Isabelle/HOL] #RF #Isabelle
* [http://bit.ly/kbX6ZI seL4 enforces integrity] #Verificación #Isabelle
* [http://bit.ly/m4r6a7#RF Initial semantics for higher-order typed syntax in Coq] #Coq
* [http://bit.ly/lGZVoa Initial semantics for higher-order typed syntax in Coq] #RF #Coq
* [http://bit.ly/jXe3QN Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #RF #Coq
* [http://bit.ly/mOh20v Specification of imperative languages using operational semantics in Coq] #RF #Coq
* [http://bit.ly/mlftfm A first-order calculus for allegories] #AR
* [http://bit.ly/imjeTQ Generating schemata of resolution proofs] #AR
* [http://bit.ly/iGWaxr On the generation of positivstellensatz witnesses in degenerate cases] #RF #Coq
* [http://bit.ly/lAHBc0 Deciding Kleene algebras in Coq] #RF #Coq
* [http://bit.ly/lH7T3a Glasgow Haskell vs. Lispworks] #Haskell #Lisp
* [http://bit.ly/jzm3hG On the expressive power of unit resolution] #AR
* [http://bit.ly/jo9RKj Proceedings 15th international refinement workshop] #AR
* [http://bit.ly/mLskMG Solving the unsolvable] #AR
* [http://bit.ly/kJTmix Type classes for efficient exact real arithmetic in Coq] #Coq
* [http://bit.ly/lbXy2P Un problema de las olimpiadas rusas en Haskell] #Haskell #V
* [http://bit.ly/lcO4n8 BDDs verified in a proof assistant] #Isabelle
* [http://arxiv.org/pdf/1106.3685v3 Embedding and automating conditional logics in classical higher-order logic].
* [http://bit.ly/iJwaDm Incidence simplicial matrices formalized in Coq/SSReflect]. #RF #Coq
* [http://bit.ly/mTuPbK What’s fun about teaching] #Enseñanza
* [http://bit.ly/khYlHh Isabelle repository for relational and algebraic methods] #Isabelle
* [http://bit.ly/kPQSDw Automated engineering of relational and algebraic methods in Isabelle/HOL] #Isabelle

== Lecturas de Julio de 2011 ==
* [http://bit.ly/kANpSp SAT solver of Howe & King as a logic program] #SAT #PL
* [http://bit.ly/jGEdXT Razonamiento formalizado para la enseñanza de las matemáticas]. #Vestigium, #Enseñanza
* [http://bit.ly/jlZ8Cm The ideal mathematician]. #Humor
* [http://bit.ly/m4SyOB El problema de las puertas en Haskell]. #Haskell
* [http://bit.ly/qa3Pu4 Metadata for a mathematical wiki: Initial experiments]. #Mizar
* [http://bit.ly/pTzB4X Logical verification]. #Coq
* [http://bit.ly/rgkvHw Formal proofs for theoretical properties of Newton's method]. #Coq
* [http://www.irit.fr/~Martin.Strecker/Publications/jfo09.html Formalisation de la logique de description ALC dans l'assistant de preuve Coq]. #Coq, #ALC
* [http://www.irit.fr/~Martin.Strecker/Publications/afadl10.html Vérification d'une méthode de preuve pour la logique de description ALC]. #Isabelle. #ALC
* [http://bit.ly/oVkDGz A critique of Abelson and Sussman or why calculating is better than scheming]. #Haskell, #Lisp
* [http://www.cs.ru.nl/~spitters/paper_5.pdf Experiments with computable matrices in the Coq system]. #Coq
* [http://arxiv.org/pdf/1107.3396v1 Computing the homology of groups: the geometric way]. #Kenzo
* [http://bit.ly/qr2Mxy Peut-on faire des mathématiques avec un ordinateur?]. #ME
* [http://bit.ly/oPpVNf The theory behind TheoryMind]. #Isabelle
* [http://shemesh.larc.nasa.gov/people/cam/publications/scico2011-draft.pdf Provably correct conflict prevention bands algorithms]. #PVS
* [http://bit.ly/oe6zF6 Peut-on avoir confiance en l'informatique?]. #Verificación
* [http://bit.ly/pzjDet Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)]. #GLC, #Vestigium
* [~/BibliotecaDigital/Bundy_2011_Automated theorem provers a practical tool for the working mathematician.pdf Automated theorem provers a practical tool for the working mathematician]. #DAO, #Vestigium
* [http://www.phdcomics.com/comics.php?f=1436 Intellectual Freedom]. #Humor
* [http://bit.ly/q4rgao Expresiones aritméticas mediante tipos abstracto de datos y polinomios]. #Haskell, #Vestigium
* [http://bit.ly/qcEEP5 A verified runtime for a verified theorem prover]. #ACL2
* [http://www.iist.unu.edu/www/docs/techreports/reports/report453.pdf A framework for automated and certified refinement steps]. #Isabelle]
* [http://bit.ly/pNvssL Descomposiciones en sumas de cuadrados en Haskell]. #Haskell, #Vestigium
* [http://www.glc.us.es/~jalonso/vestigium/interactive-proof-introduction-to-isabellehol Interactive proof introduction to IsabelleHOL]. #Isabelle
* [http://www1.eafit.edu.co/asicard/teaching/dtfl-CB0683/projects/juan-pedro-villa-isaza/coqav/coqav-slides.pdf Coq au vin (The Coq proof assistant and the Curry-Howard correspondence)] #Coq
* [ftp://ftp.cs.man.ac.uk/pub/amulet/theses/D_Richards11_phd.pdf Hardware languages and proof]. #Tesis, #PVS, #SAL

== Lecturas de Agosto de 2011 ==
* [http://www.cs.utexas.edu/~moore/publications/talks/early-days.pdf Theorem proving for verification (the early days)] #Historia
* [http://bit.ly/qfAZ27 Selecting attributes for sport forecasting using formal concept analysis] #AFC
* [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-julio-de-2011/ Lecturas del Grupo de Lógica Computacional (Julio de 2011)]. #GLC #Vestigium
* [http://www-users.cs.york.ac.uk/~jim/fmsurvey.pdf Formal methods: practice and experience] #Métodos formales
* [http://dream.inf.ed.ac.uk/events/ssfrr-2010/SSFRR_files/CSUR-shankar.pdf Automated deduction for verification] #DAT
* [http://www.cs.ucla.edu/~rupak/Papers/SoftwareModelChecking.pdf Software model checking] #Model checking
* [http://qpq.csl.sri.com/vsr/manifesto.pdf The verified software initiative: A Manifesto] #Verificación
* [http://www.cs.utexas.edu/~moore/publications/acl2-how-to-2011.pdf How can i do that with ACL2 recent enhancements to ACL2] #ACL2
* [http://www.math.cas.cz/~tzameret/nonComm.pdf Algebraic proofs over noncommutative formulas] #Cálculo_polinomial
* [http://itcs.tsinghua.edu.cn/~tzameret/Iddo-PhD-thesis.pdf Studies in algebraic and propositional proof complexity] #Tesis #Cálculo_polinomial
* [http://shemesh.larc.nasa.gov/people/cam/Bernstein/bernstein.pdf Formalization of an efficient representation of Bernstein polynomials and applications to global optimization] #PVS
* [http://www.cl.cam.ac.uk/~tw333/publications/guttmann11automating.pdf Automating algebraic methods in Isabelle] #Isabelle
* [http://www.cl.cam.ac.uk/~tw333/publications/guttmann11repository.pdf A repository for Tarski-Kleene Algebras] #Isabelle
* [https://www.iist.unu.edu/www/docs/techreports/reports/report429.pdf Emergence and refinement] #Emergencia, #Refinamentos
* [http://www.stanford.edu/~danlass/esslli2011stus/petrovic.pdf Automated proving in geometry using Gröbner bases in Isabelle/HOL] #Isabelle
* [http://www.stanford.edu/~danlass/esslli2011stus/stojadinovic.pdf How efficient can fully verified functional programs be - A case study of graph traversal algorithms] #Isabelle
* [http://www4.in.tum.de/~krauss/imperative/imperative.pdf Imperative functional programming with Isabelle/HOL] #Isabelle
* [http://www.cs.utexas.edu/~jared/publications/2011-memocode-centaur.pdf A flexible formal verification framework for industrial scale validation] #ACL2
* [http://papers.ssrn.com/sol3/papers.cfm?abstract_id=1773169 Markets are efficient if and only if P = NP].
* [http://www.cs.utexas.edu/~jared/publications/2011-acl2-bitblast.pdf Bit-blasting ACL2 theorems] #ACL2 #GL
* [http://repositories.lib.utexas.edu/bitstream/handle/2152/ETD-UT-2010-12-2210/SWORDS-DISSERTATION.pdf?sequence=1 A verified framework for symbolic execution in the ACL2 theorem prover]. #ACL2 #GL
* [http://www.ccs.neu.edu/home/harshrc/ITaITP.pdf Integrating testing and interactive theorem proving] #ACL2
* [http://ertos.nicta.com.au/publications/papers/Sewell_WGMAK.pdf seL4 enforces integrity] #Isabelle
* [http://arxiv.org/pdf/1108.2429v1 Peirce's truth-functional analysis and the origin of truth tables]. #Historia
* [http://hvg.ece.concordia.ca/Publications/Conferences/NFM2011.pdf Towards flight control verification using automated theorem proving] #MetiTarski
* [http://www.cl.cam.ac.uk/~pes20/ott/ott-jfp.pdf Ott: Effective tool support for the working semanticist]. #Ott #Coq #Isabelle #HOL
* [http://www.cl.cam.ac.uk/~so294/lem/lem-description.pdf Lightweight tools for heavyweight semantics]. #Lem #Ott #Coq #Isabelle #HOL
* [http://hal.inria.fr/inria-00614041/PDF/ArmandAl.pdf Verifying SAT and SMT in Coq for a fully automated decision procedure]. #Coq #SAT #SMT
* [http://afp.sourceforge.net/entries/Max-Card-Matching.shtml Maximum cardinality matching]. #Isabelle
* [http://arxiv.org/pdf/1108.3446v1 Premise selection for mathematics by corpus analysis and kernel methods]. #AA
* [http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml Gauss-Jordan elimination for matrices represented as functions]. #Isabelle
* [Verification of dependable software using Spark and Isabelle]. #Isabelle
* [Verification of programs in virtual memory using separation logic]. #Isabelle
* [Automated specification analysis using an interactive theorem prover]. #ACL2
* [Formal analysis of fractional order systems in HOL]. #HOL

== Lecturas de Septiembre de 2011 ==
* [Formalization of abstract state transition systems for SAT]. #Isabelle
* [http://bit.ly/pmJLlD Zeno: A tool for the automatic verification of algebraic properties of functional programs] #Isabelle #Haskell
* [http://research.microsoft.com/en-us/um/people/leino/papers/krml218.pdf Automating induction with an SMT Solver]. #SMT #Z3
* [http://www.ai.uga.edu/arc/VanLiefferinge-ICAI.pdf Artificial intelligence techniques for understanding gothic cathedrals] #Prolog
* [http://www.few.vu.nl/%7Ejui200/thesis.pdf RDFS/OWL reasoning using the MapReduce framework]. #DL #SW
* [http://www4.in.tum.de/~blanchet/frocos2011-dis-proof.pdf Automatic proof and disproof in Isabelle/HOL]. #Isabelle
* [http://www4.in.tum.de/~blanchet/jar2009-huffman.pdf Proof Pearl: Mechanizing the textbook proof of Huffman’s algorithm]. #Isabelle
* [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians]. #Isabelle
* [http://www4.in.tum.de/~nipkow/pubs/ijsi11.pdf Majority vote algorithm revisited again] #Isabelle
* [http://www.cs.unibo.it/~asperti/SLIDES/itp.pdf A survey on interactive theorem proving] #Survey #ITP
* [http://hal.inria.fr/docs/00/61/87/45/PDF/document.pdf Formalization of Wu’s simple method in Coq]. #Coq
* [http://bit.ly/nzAkpX Functional programming for Java developers]. #PF #Tutorial
* [http://tel.archives-ouvertes.fr/docs/00/55/51/58/PDF/pasca_phd_thesis.pdf Formal verification for numerical methods]. #Tesis #Coq
* [http://www.etnassoft.com/biblioteca/practical-semantic-web-and-linked-data-applications-lisp-edition/ Practical Semantic Web and linked data applications. Lisp edition]. #SW #Lisp
* [http://www.lri.fr/~paulin/LASER/lab-coq.pdf Basics of Coq]. #Coq #Tutorial
* [http://cel.archives-ouvertes.fr/docs/00/47/58/07/PDF/coq-hurry.pdf Coq in a hurry]. #Coq #Tutorial
* [http://www.springerlink.com/content/0078822671532p5x/ Reasoning processes in propositional logic].
* [http://www.etnassoft.com/biblioteca/programacion-funcional Programación funcional con Haskell]. #Haskell
* [http://www.etnassoft.com/biblioteca/ejercicios-de-programacion-funcional-con-haskell Ejercicios de programación funcional con Haskell]. #Haskell
* [http://www.etnassoft.com/biblioteca/introduccion-a-la-programacion-logica-con-prolog/ Introducción a la programación lógica con Prolog]. #Prolog
* [http://www.etnassoft.com/biblioteca/ejercicios-de-programacion-declarativa-con-prolog/ Ejercicios de programación declarativa con Prolog]. #Prolog
* [http://iswc2011.semanticweb.org/fileadmin/iswc/Papers/Research_Paper/07/70310224.pdf Verification of the OWL-time ontology]. #Prover9 #Ontología
* [http://www.cs.us.es/~jalonso/publicaciones/2005-tphols.pdf Proof Pearl: A formal proof of Higman’s lemma in ACL2]. #ACL2
* [http://lyah.haskell.fr Apprendre Haskell vous fera le plus grand bien!]. #Haskell
* [http://jfr.cib.unibo.it/article/view/1899 Implementation of Bourbaki's elements of mathematics in Coq: Part one, Theory of sets]. #Coq
* [http://sqig.math.ist.utl.pt/pub/DionisioFM/04-DGM-dlogisa.pdf Defining and using deductive systems with Isabelle]. #Isabelle
* [http://es.scribd.com/doc/25234088/Applications-of-Propositional-Logic-to-Cellular-Automata Some applications of propositional logic to cellular Automata].
* [http://hal.inria.fr/inria-00440786/en Implementation of Bourbaki's elements of mathematics in Coq: Part Two; Ordered sets, Cardinals, integers]. #Coq
* [http://www-fourier.ujf-grenoble.fr/~sergerar/Papers/La%20Rochelle.pdf How Kenzo program works].

== Lecturas de Octubre de 2011 ==
* [http://argo.matf.bg.ac.rs/publications/2011/CECIIS-AR-Janicic.pdf Automated reasoning: some successes and new challenges]. #RA
* [http://cl-informatik.uibk.ac.at/users/griff/publications/ST-FroCoS11.pdf Generalized and formalized uncurrying]. #Isabelle
* [http://jfr.cib.unibo.it/article/download/1974/1361 Basic first-order model theory in Mizar]. #Mizar
* [http://www.unirioja.es/cu/joheras/acmtsdiwtks.pdf A certified module to study digital images with the Kenzo system]. #ACL2
* [http://bit.ly/r45fAZ What is a proof?]
* [http://t.co/9XUjojkz Los peligros de “pagar por publicar” en las revistas científicas de acceso abierto].
* [http://www.ams.org/notices/201109/rtx110901294p.pdf The dangers of the “author pays” model in mathematical publishing].
* [http://www4.in.tum.de/~nipkow/pubs/cpp11.pdf Proof Pearl: The marriage theorem]. #Isabelle
* [http://www.jamisbuck.org/presentations/rubyconf2011/index.html "Algorithms" is not a four-letter word]. #Algorítmica
* [http://ceur-ws.org/Vol-760/paper2.pdf An overview of methods for large-theory automated theorem proving] #DAT.
* [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-septiembre-de-2011/ Lecturas del Grupo de Lógica Computacional (Septiembre de 2011)]
* [http://www.etnassoft.com/biblioteca/haskell-tutorial-for-c-programmers Haskell tutorial for C programmers]. #Tutorial #Haskell
* [http://pierre-yves.strub.nu/research/ec/bartzia-master-report.pdf Formalisation des courbes elliptiques en Coq]. #Tesis #Coq
* [http://www.ai.uga.edu/arc/HollingsworthReport.pdf Progress report on the ARC Project: Creating logical models of Gothic cathedrals]. #IA #Prolog #RC
* [http://queue.acm.org/detail.cfm?id=2038036 OCaml for the masses: Why the next language you learn should be functional]. #FP

== Lecturas de Noviembre de 2011 ==
* [http://afp.sourceforge.net/entries/Efficient-Mergesort.shtml Efficient mergesort]. #Isabelle #AFP
* [http://logika.uwb.edu.pl/studies/download.php?volid=35&artid=mg Formalization of propositional linear temporal logic in the Mizar system]. #Mizar
* [http://www.mpi-inf.mpg.de/~mehlhorn/ftp/VerificationCertComps.pdf Verification of certifying computations] #Isabelle
* [http://formes.asia/media/seminars/2011-11-16-jpj.pdf Coq, a proof assistant based on higher-order intuitionistic type theory]. #Coq
* [http://slidesha.re/v4QfB5 Retos y oportunidades de la IA en I+D+i con empresas]. #IA
* [http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20090040481_2009041314.pdf Compositional verification of a communication protocol for a remotely operated vehicle]. #PVS
* [http://afp.sourceforge.net/entries/TLA.shtml A definitional encoding of TLA== in Isabelle/HOL]. #Isabelle ==
* [http://www.divms.uiowa.edu/~astump/papers/vmcai12.pdf VerSAT: a verified modern SAT solver]. #GURU
* [http://www.eecs.berkeley.edu/Pubs/TechRpts/2011/EECS-2011-118.pdf Towards automated system synthesis using SCIDUCTION]. #Tesis

== Lecturas de Diciembre de 2011 ==
* [http://lara.epfl.ch/~kuncak/thesis-piskac.pdf Decision procedures for program synthesis and verification]. #Tesis
* [http://lib.tkk.fi/Diss/2011/isbn9789526043685/isbn9789526043685.pdf Grid based propositional satisfiability solving]. #Tesis #SAT
* [http://arxiv.org/pdf/1111.5775 Partial mutual exclusion for infinitely many processes]. #PVS
* [http://www.mpi-inf.mpg.de/~mehlhorn/ftp/CertifyingAlgorithms.pdf Certifying algorithms]. #Algoritmos_fehacientes
* [http://www.ioc.ee/~tarmo/papers/aplas11.pdf A Proof Pearl with the fan theorem and bar induction (Walking through infinite trees with mixed induction and coinduction)] #Coq
* [http://www-personal.umich.edu/~mejn/papers/cssurvey.pdf Complex systems: A survey]
* [http://www.csse.monash.edu.au/~jnc/jnc-tutorial.pdf What is mathematical logic? A survey].
* [http://cs.ru.nl/~peterl/teaching/KeR/summary.pdf Knowledge representation and reasoning (Logic meets probability theory)] #Libro
* [http://perso.crans.org/cohen/work/realalg/code/cohen.pdf Construction des nombres algébriques réels en Coq]. #Coq
* [https://tspace.library.utoronto.ca/bitstream/1807/31274/1/Katsumi_Megan_S_201111_MASc_thesis.pdf A methodology for the development and verification of expressive ontologies]. #Tesis #Prover9
* [http://arxiv.org/pdf/1112.1795 Wave equation numerical resolution: mathematics and program]. #Coq
* [http://www.lri.fr/~lelay/Rapport.pdf Étude de la différentiabilité et de l'intégrabilité en Coq (Application à la formule de d'Alembert pour l'équation des ondes)] #Coq
* [http://jfr.cib.unibo.it/article/view/2269 Formalizing a proof that e is transcendental]. #HOL_Light
* [http://jfr.cib.unibo.it/article/view/2225 A proof-theoretic account of primitive recursion and primitive iteration]. #MinLog
* [http://jfr.cib.unibo.it/article/view/2066 Initial semantics for higher-order typed syntax in Coq]. #Coq
* [Http://www.ams.org/notices/200807/tx080700773p.pdf Desperately seeking mathematical truth]. #Filosofia
* [http://www.andrew.cmu.edu/user/avigad/Talks/ioannina.pdf Interactive theorem proving (A survey/tutorial, for logician)]. #Tutorial #ITP
* [http://www.cs.ru.nl/~herman/ictopen.pdf Can the computer really help us to prove theorems?]. #ITP #Panorama
* [http://ggweb.stanford.edu/assets/ctx/1.0-SNAPSHOT/downloads/TechReports/OP-Cogsci-2008.pdf An empirical study of errors in translating natural language into logic]. #MDE
* [http://www.hcs.harvard.edu/~hrp/issues/1996/Boolos.pdf The hardest logic puzzle ever]. #Rompecabeza

@@ Línea 26: / Línea 26: @@
 * [http://bit.ly/gZYKNJ Lectures in game theory for computer scientists] #Libro
 * [http://bit.ly/dNvlXU Reactive valuations] #TFM
-* [http://slidesha.re/f8SKgI Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet] Algunas aplicaciones de las bases de Groebner http://bit.ly/haeTax
+* [http://slidesha.re/f8SKgI Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet]
 * [http://bit.ly/hrwBXD Programación funcional con Haskell] #Libro #Haskell
 * [http://bit.ly/eGqBDZ Certifying compilers using higher-order theorem provers as certificate checker] #Isabelle #Coq
@@ Línea 34: / Línea 35: @@
 * [http://bit.ly/eZiRVL Deducción natural en lógica proposicional con Isabelle/Isar] #Isabelle #V
 * [http://bit.ly/hTYRXf Deducción natural en lógica de primer orden con Isabelle/Isar] #Isabelle #V
-* [http://bit.ly/h2co0D
+* [http://bit.ly/h2co0D fKenzo: A user interface for computations in Algebraic Topology]
 * [http://bit.ly/hZdkPN A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL]. #Isabelle
 * [http://bit.ly/gcvJNz El tipo abstracto de datos de las colas de prioridad en Haskell] #Haskell #V
@@ Línea 61: / Línea 60: @@
 * [http://bit.ly/hBKzIz El tipo abstracto de datos de las colas en Haskell] #Haskell #V
 * [http://goo.gl/oUlcY Executable transitive closures of finite relations] #RF #Isabelle
-* [http://goo.gl/epNrc
+* [http://goo.gl/epNrc Solución española para un problema de John Nash]
++ [http://goo.gl/FoL94 Reduced ordered binary decision diagram with implied literals: A new knowledge compilation approach]  #AR
 * [http://bit.ly/gHpfXL Teaching FP to freshmen] #Enseñanza #PF
 * [http://goo.gl/2fK3d Introduction to artificial intelligence] #Libro #IA
@@ Línea 191: / Línea 189: @@
 * [http://bit.ly/oe6zF6 Peut-on avoir confiance en l'informatique?]. #Verificación
 * [http://bit.ly/pzjDet Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)]. #GLC, #Vestigium
-* [~/BibliotecaDigital/Bundy_2011_Automated theorem provers a practical tool for the working mathematician.pdf Automated theorem provers a practical tool for the working mathematician]. #DAO, #Vestigium
+* [http://www.glc.cs.us.es/~jalonso/BibliotecaDigital/Bundy_2011_Automated theorem provers a practical tool for the working mathematician.pdf Automated theorem provers a practical tool for the working mathematician]. #DAO, #Vestigium
 * [http://www.phdcomics.com/comics.php?f=1436 Intellectual Freedom]. #Humor
 * [http://bit.ly/q4rgao Expresiones aritméticas mediante tipos abstracto de datos y polinomios]. #Haskell, #Vestigium
@@ Línea 233: / Línea 231: @@
 * [http://arxiv.org/pdf/1108.3446v1 Premise selection for mathematics by corpus analysis and kernel methods]. #AA
 * [http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml Gauss-Jordan elimination for matrices represented as functions]. #Isabelle
-* [Verification of dependable software using Spark and Isabelle]. #Isabelle
+* [http://goo.gl/LyRYt Verification of dependable software using Spark and Isabelle]. #Isabelle
-* [Verification of programs in virtual memory using separation logic]. #Isabelle
+* [http://goo.gl/W6eUw Verification of programs in virtual memory using separation logic]. #Isabelle
-* [Automated specification analysis using an interactive theorem prover]. #ACL2
+* [http://goo.gl/zWkeU Automated specification analysis using an interactive theorem prover]. #ACL2
-* [Formal analysis of fractional order systems in HOL]. #HOL
+* [http://goo.gl/C6HfW Formal analysis of fractional order systems in HOL]. #HOL
 == Lecturas de Septiembre de 2011 ==
-* [Formalization of abstract state transition systems for SAT]. #Isabelle
+* [http://goo.gl/fRfbP Formalization of abstract state transition systems for SAT]. #Isabelle
 * [http://bit.ly/pmJLlD Zeno: A tool for the automatic verification of algebraic properties of functional programs] #Isabelle #Haskell
 * [http://research.microsoft.com/en-us/um/people/leino/papers/krml218.pdf Automating induction with an SMT Solver]. #SMT #Z3
@@ Línea 313: / Línea 311: @@
 * [http://jfr.cib.unibo.it/article/view/2225 A proof-theoretic account of primitive recursion and primitive iteration]. #MinLog
 * [http://jfr.cib.unibo.it/article/view/2066 Initial semantics for higher-order typed syntax in Coq]. #Coq
-* [Http://www.ams.org/notices/200807/tx080700773p.pdf Desperately seeking mathematical truth]. #Filosofia
+* [http://www.ams.org/notices/200807/tx080700773p.pdf Desperately seeking mathematical truth]. #Filosofia
 * [http://www.andrew.cmu.edu/user/avigad/Talks/ioannina.pdf Interactive theorem proving (A survey/tutorial, for logician)]. #Tutorial #ITP
 * [http://www.cs.ru.nl/~herman/ictopen.pdf Can the computer really help us to prove theorems?]. #ITP #Panorama
 * [http://ggweb.stanford.edu/assets/ctx/1.0-SNAPSHOT/downloads/TechReports/OP-Cogsci-2008.pdf An empirical study of errors in translating natural language into logic]. #MDE
 * [http://www.hcs.harvard.edu/~hrp/issues/1996/Boolos.pdf The hardest logic puzzle ever]. #Rompecabeza