Lecturas del año 2011

Lecturas de Enero de 2011

• Semantic web reasoners and languages #RA #WS
• El 2011 y los números primos (en Haskell) #Haskell
• The dialectica interpertation in Coq #Coq
• Errores aritméticos en Haskell y en Lisp #Haskell #Lisp
• Why Lisp is a big hack (and Haskell is doomed to succeed) #Lisp #Haskell
• ProofWiki y la verificación de las demostraciones matemáticas #Verificación #MKM
• A quick and gentle guide to constraint logic programming via ECLiPSe #PL #Restricciones
• A language for mathematical knowledge management #MKM
• Automated inference of finite unsatisfiability #AR
• The free vector space on a type. #Haskell
• Formal methods applied to a floating-point number system #Z
• A machine-checked theory of floating point arithmetic #HOL_Light
• Formal verification of floating point trigonometric functions #HOL_Light
• A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon TM processor #ACL2
• A generic library for floating-point numbers and its application to exact computing #Coq.
• A high-level formalization of floating-point numbers in PVS #PVS
• Formal verification of floating-point programs #Coq
• The pitfalls of verifying floating-point computations #Verificación
• Floats and ropes: A case study for formal numerical program verification #Coq.
• Formal reliability analysis of combinational circuits using theorem proving #HOL
• Programación funcional con Haskell #Libro #Haskell
• Certifying compilers using higher-order theorem provers as certificate checker #Isabelle #Coq
• El tipo abstracto de datos de las colas en Haskell #Haskell

Lecturas de Febrero de 2011

• Deducción natural en lógica proposicional con Isabelle/Isar #Isabelle
• Deducción natural en lógica de primer orden con Isabelle/Isar #Isabelle
• A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL. #Isabelle
• El tipo abstracto de datos de las colas de prioridad en Haskell #Haskell
• Program verification and functioning of operative computing revisited: How about mathematics engineering? #Verificación
• El próximo después de 1811 #Haskell
• Charming proofs: A journey into elegant mathematics #Libro #DAO
• Functional binomial queues #RF #Isabelle
• Lower semicontinuous functions #RF #Isabelle
• Lógica Informática (2010-11) #LI
• Artificial intelligence (Foundations of computational agents) #Libro #IA

Lecturas de Marzo de 2011

• Software verification turns maintstream #Verificación
• Formalising, improving, and reusing the Java module system http://bit.ly/dF68vF #Tesis #Isabelle
• SMT solvers: new oracles for the HOL theorem prover #SMT #HOL4
• Isabelle como un lenguaje funcional #Isabelle
• El tipo abstracto de datos de las pilas en Haskell #Haskell
• El tipo abstracto de datos de las colas en Haskell #Haskell
• Executable transitive closures of finite relations #RF #Isabelle

+ Reduced ordered binary decision diagram with implied literals: A new knowledge compilation approach #AR

• Introduction to artificial intelligence #Libro #IA
• Experience report: Functional programming through deep time (Modeling the first complex ecosystems on Earth) #Haskell
• Logic-based artificial intelligence #Libro #IA
• A Formalization of the C99 Standard in HOL, Isabelle and Coq #HOL #Isabelle #Coq
• Formal methods in agent-oriented software engineering #MF
• The cognitive agents specification language and verification environment #Verificación
• Software bugs and scientific progress #Verificación
• Representing model theory in a type-theoretical logical framework #RF #Twelfe
• Towards a verification framework for faulty message passing systems in PVS #PVS

Lecturas de Abril de 2011

• Por qué y cómo se hace investigación en matemáticas #CM
• Introduction to newLISP #Libro #Lisp
• Verified firewall policy transformations for test case generation #Isabelle
• An approach to modular and testable security models of real-world health-care applications #Isabelle
• Psi-calculi: a framework for mobile processes with nominal data and logic #Isabelle
• Simplification rules for intuitionistic propositional tableaux #AR
• A fast and verified algorithm for proving store-and-forward networks deadlock-free #ACL2
• Gestión mecanizada del conocimiento matemático en Topología algebraica #Tesis #ACL2
• The first formalized math wiki is here #MKM
• Extending Sledgehammer with SMT Solvers #Isabelle #SMT
• Book of proof #Libro #DAO
• The general triangle is unique #RF #Isabelle
• NASA Formal Methods #Libro #MF #Verificación
• Haskell for the cloud #Haskell
• The opentheory standard theory library #Verificación
• A Coq-based library for interactive and automated theorem proving in plane geometry #RF #Coq
• Mechanical support for efficient dissemination on the CAN overlay network #Isabelle
• A Wiki for formal mathematics #MKM
• Recent developments in computing and philosophy #Prover9
• Constructive formalization of classical modal logic. #Coq
• Proving equality between streams #Coq
• The limits of correctness #Verificación
• A formal proof of the Riesz representation theorem #RF #PVS
• A formal proof that π₁(S¹)=Z #RF #Coq

Lecturas de Mayo de 2011

• Balancing weight-balanced trees #Coq #Haskell
• A formal programming model of Orléans skeleton library #Coq
• Formal verification of a small real-time operating system #Tesis #Isabelle
• Deus ex machina. #Prover9
• Computationally-discovered simplification of the ontological argument. #Prover9
• Satisfiability of acyclic and almost acyclic CNF formulas (II) #AR
• Heaps and data structures: A challenge for automated provers #AR
• Haskell: Not pure enough? #Haskell
• Verified stack-based genetic programming via dependent types #RF #Agda #IA
• Sorpresa sumando potencias de 2 en Haskell #Haskell
• A list-machine benchmark for mechanized metatheory #AR
• The locally nameless representation #AR
• Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem #TFM #PVS
• Solving Rubik's cube using SAT solvers #SAT
• Programação funcional: Novos horizontes para a expansão da consciência #PF
• Computer certified efficient exact reals in Coq #Coq
• Parallel and concurrent programming in Haskell #Haskell
• TRX: A formally verified parser interpreter #Coq
• Computational meta-ethics: Towards the meta-ethical robot #Prover9
• Formal metatheory of programming languages in the Matita interactive theorem prover #RF #Matita
• ALPprolog — A new logic programming method for dynamic domains #PL
• Logical formalization of semantic business vocabulary and Rules #RC
• The proof is in the pudding (The changing nature of mathematical proof) #Libro #LI
• Knowledge-based programs #RF #Isabelle
• Elegance and power #Haskell
• Validated compilation through logic #Verificación
• Teaching computational logic: Technology-enhanced learning and animations #Enseñanza #LI
• Sigma: An integrated development environment for formal ontology #RC
• Termination of Isabelle functions via termination of rewriting #AR #Isabelle
• Combining and automating classical and non-classical logics in classical higher-order logics #AR
• Rationality and escalation in infinite extensive games #Libro #RF #Coq

Lecturas de Junio de 2011

• Efficient interactive construction of machine-checked protocol security proofs in the context of dynamically compromising adversaries #TFM #RF #Isabelle
• Specification and verification: The Spec# experience #Verificación
• Formal verification of chess endgames tables #HOL4 #IA
• Integrating testing and interactive theorem proving #ACL2
• Conway’s games and some of their basic properties #Mizar
• A verified runtime for a verified theorem prover #HOL4
• Modelling distributed cognition systems in PVS #PVS
• Three chapters of measure theory in Isabelle/HOL #RF #Isabelle
• seL4 enforces integrity #Verificación #Isabelle
• Initial semantics for higher-order typed syntax in Coq #Coq
• Initial semantics for higher-order typed syntax in Coq #RF #Coq
• Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #RF #Coq
• Specification of imperative languages using operational semantics in Coq #RF #Coq
• A first-order calculus for allegories #AR
• Generating schemata of resolution proofs #AR
• On the generation of positivstellensatz witnesses in degenerate cases #RF #Coq
• Deciding Kleene algebras in Coq #RF #Coq
• Glasgow Haskell vs. Lispworks #Haskell #Lisp
• On the expressive power of unit resolution #AR
• Proceedings 15th international refinement workshop #AR
• Solving the unsolvable #AR
• Type classes for efficient exact real arithmetic in Coq #Coq
• Un problema de las olimpiadas rusas en Haskell #Haskell
• BDDs verified in a proof assistant #Isabelle
• Embedding and automating conditional logics in classical higher-order logic.
• Incidence simplicial matrices formalized in Coq/SSReflect. #RF #Coq
• Isabelle repository for relational and algebraic methods #Isabelle
• Automated engineering of relational and algebraic methods in Isabelle/HOL #Isabelle

Lecturas de Julio de 2011

• SAT solver of Howe & King as a logic program #SAT #PL
• Razonamiento formalizado para la enseñanza de las matemáticas. #Enseñanza
• El problema de las puertas en Haskell. #Haskell
• Metadata for a mathematical wiki: Initial experiments. #Mizar
• Logical verification. #Coq
• Formal proofs for theoretical properties of Newton's method. #Coq
• Formalisation de la logique de description ALC dans l'assistant de preuve Coq. #Coq, #ALC
• Vérification d'une méthode de preuve pour la logique de description ALC. #Isabelle. #ALC
• A critique of Abelson and Sussman or why calculating is better than scheming. #Haskell, #Lisp
• Experiments with computable matrices in the Coq system. #Coq
• Computing the homology of groups: the geometric way. #Kenzo
• Peut-on faire des mathématiques avec un ordinateur?. #ME
• The theory behind TheoryMind. #Isabelle
• Provably correct conflict prevention bands algorithms. #PVS
• Peut-on avoir confiance en l'informatique?. #Verificación
• Automated theorem provers a practical tool for the working mathematician. #DAO
• Expresiones aritméticas mediante tipos abstracto de datos y polinomios. #Haskell
• A verified runtime for a verified theorem prover. #ACL2
• A framework for automated and certified refinement steps. #Isabelle
• Descomposiciones en sumas de cuadrados en Haskell. #Haskell
• Interactive proof introduction to IsabelleHOL. #Isabelle
• Coq au vin (The Coq proof assistant and the Curry-Howard correspondence) #Coq
• Hardware languages and proof. #Tesis #PVS #SAL

Lecturas de Agosto de 2011

• Theorem proving for verification (the early days) #Historia
• Selecting attributes for sport forecasting using formal concept analysis #AFC
• Formal methods: practice and experience #MF
• Automated deduction for verification #DAT
• Software model checking #Model_checking
• The verified software initiative: A Manifesto #Verificación
• How can i do that with ACL2 recent enhancements to ACL2 #ACL2
• Algebraic proofs over noncommutative formulas #Cálculo_polinomial
• Studies in algebraic and propositional proof complexity #Tesis #Cálculo_polinomial
• Formalization of an efficient representation of Bernstein polynomials and applications to global optimization #PVS
• Automating algebraic methods in Isabelle #Isabelle
• A repository for Tarski-Kleene Algebras #Isabelle
• Emergence and refinement #Emergencia, #Refinamentos
• Automated proving in geometry using Gröbner bases in Isabelle/HOL #Isabelle
• How efficient can fully verified functional programs be - A case study of graph traversal algorithms #Isabelle
• Imperative functional programming with Isabelle/HOL #Isabelle
• A flexible formal verification framework for industrial scale validation #ACL2
• Bit-blasting ACL2 theorems #ACL2 #GL
• A verified framework for symbolic execution in the ACL2 theorem prover. #ACL2 #GL
• Integrating testing and interactive theorem proving #ACL2
• seL4 enforces integrity #Isabelle
• Towards flight control verification using automated theorem proving #MetiTarski
• Ott: Effective tool support for the working semanticist. #Ott #Coq #Isabelle #HOL
• Lightweight tools for heavyweight semantics. #Lem #Ott #Coq #Isabelle #HOL
• Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq #SAT #SMT
• Maximum cardinality matching. #Isabelle
• 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
• Zeno: A tool for the automatic verification of algebraic properties of functional programs #Isabelle #Haskell
• Automating induction with an SMT Solver. #SMT #Z3
• Artificial intelligence techniques for understanding gothic cathedrals #Prolog
• RDFS/OWL reasoning using the MapReduce framework. #DL #SW
• Automatic proof and disproof in Isabelle/HOL. #Isabelle
• Proof Pearl: Mechanizing the textbook proof of Huffman’s algorithm. #Isabelle
• Isabelle primer for mathematicians. #Isabelle
• Majority vote algorithm revisited again #Isabelle
• A survey on interactive theorem proving #Survey #ITP
• Formalization of Wu’s simple method in Coq. #Coq
• Functional programming for Java developers. #PF #Tutorial
• Formal verification for numerical methods. #Tesis #Coq
• Practical Semantic Web and linked data applications. Lisp edition. #SW #Lisp
• Basics of Coq. #Coq #Tutorial
• Coq in a hurry. #Coq #Tutorial
• Programación funcional con Haskell. #Haskell
• Ejercicios de programación funcional con Haskell. #Haskell
• Introducción a la programación lógica con Prolog. #Prolog
• Ejercicios de programación declarativa con Prolog. #Prolog
• Verification of the OWL-time ontology. #Prover9 #Ontología
• Proof Pearl: A formal proof of Higman’s lemma in ACL2. #ACL2
• Apprendre Haskell vous fera le plus grand bien!. #Haskell
• Implementation of Bourbaki's elements of mathematics in Coq: Part one, Theory of sets. #Coq
• Defining and using deductive systems with Isabelle. #Isabelle
• Some applications of propositional logic to cellular automata.
• Implementation of Bourbaki's elements of mathematics in Coq: Part Two; Ordered sets, Cardinals, integers. #Coq
• How Kenzo program works. #Kenzo

Lecturas de Octubre de 2011

• Automated reasoning: some successes and new challenges. #RA
• Generalized and formalized uncurrying. #Isabelle
• Basic first-order model theory in Mizar. #Mizar
• A certified module to study digital images with the Kenzo system. #ACL2
• What is a proof? #LI
• Proof Pearl: The marriage theorem. #Isabelle
• "Algorithms" is not a four-letter word. #Algorítmica
• An overview of methods for large-theory automated theorem proving #DAT.
• Haskell tutorial for C programmers. #Tutorial #Haskell
• Formalisation des courbes elliptiques en Coq. #Tesis #Coq
• Progress report on the ARC Project: Creating logical models of Gothic cathedrals. #IA #Prolog #RC
• OCaml for the masses: Why the next language you learn should be functional. #FP

Lecturas de Noviembre de 2011

• Efficient mergesort. #Isabelle #AFP
• Formalization of propositional linear temporal logic in the Mizar system. #Mizar
• Verification of certifying computations #Isabelle
• Coq, a proof assistant based on higher-order intuitionistic type theory. #Coq
• Retos y oportunidades de la IA en I+D+i con empresas. #IA
• Compositional verification of a communication protocol for a remotely operated vehicle. #PVS
• A definitional encoding of TLA* in Isabelle/HOL. #Isabelle
• VerSAT: a verified modern SAT solver. #GURU
• Towards automated system synthesis using SCIDUCTION. #Tesis

Lecturas de Diciembre de 2011

• Decision procedures for program synthesis and verification. #Tesis
• Grid based propositional satisfiability solving. #Tesis #SAT
• Partial mutual exclusion for infinitely many processes. #PVS
• Certifying algorithms. #Algoritmos_fehacientes
• A Proof Pearl with the fan theorem and bar induction (Walking through infinite trees with mixed induction and coinduction) #Coq
• Complex systems: A survey #Sistemas_complejos
• What is mathematical logic? A survey. #LI
• Knowledge representation and reasoning (Logic meets probability theory) #Libro #RC
• Construction des nombres algébriques réels en Coq. #Coq
• A methodology for the development and verification of expressive ontologies. #Tesis #Prover9
• Wave equation numerical resolution: mathematics and program. #Coq
• Étude de la différentiabilité et de l'intégrabilité en Coq (Application à la formule de d'Alembert pour l'équation des ondes) #Coq
• Formalizing a proof that e is transcendental. #HOL_Light
• A proof-theoretic account of primitive recursion and primitive iteration. #MinLog
• Initial semantics for higher-order typed syntax in Coq. #Coq
• Interactive theorem proving (A survey/tutorial, for logician). #Tutorial #ITP
• Can the computer really help us to prove theorems?. #ITP #Panorama
• An empirical study of errors in translating natural language into logic. #MDE
• The hardest logic puzzle ever. #Rompecabeza #LI