Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)

Esta entrada es una recopilación de lecturas sobre razonamiento formalizado que hemos compartido este curso en la lista de correo del grupo de lógica computacional.

La recopilación de los está ordenada según el sistema de razonamiento utilizado (ACL2, Agda, Coq, HOL, Isabelle, Matita, Mizar, Otter/Prover9, PVS ó Twelfe) y, dentro de cada uno, por la fecha de su publicación.

ACL2

1. Lógica Computacional en Sevilla (30 años en una hora)
2. A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free
3. Gestión mecanizada del conocimiento matemático en Topología algebraica
4. Integrating Testing and Interactive Theorem Proving

Agda

1. Verified Stack-Based Genetic Programming via Dependent Types

Coq

1. Certifying compilers using higher-order theorem provers as certificate checkers
2. The Dialectica interpertation in Coq
3. A Formalization of the C99 Standard in HOL, Isabelle and Coq
4. A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry
5. Constructive Formalization of Classical Modal Logic
6. Proving Equality between Streams
7. A formal proof that π₁(S¹)=Z
8. Balancing Weight-Balanced Trees
9. A Formal Programming Model of Orléans Skeleton Library
10. Computer certified efficient exact reals in Coq
11. TRX: A Formally Verified Parser Interpreter
12. Rationality and Escalation in Infinite Extensive Games
13. Initial Semantics for higher-order typed syntax in Coq
14. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
15. Specification of imperative languages using operational semantics in Coq
16. On the Generation of Positivstellensatz Witnesses in Degenerate Cases
17. Deciding Kleene Algebras in Coq
18. Type classes for efficient exact real arithmetic in Coq
19. Incidence simplicial matrices formalized in Coq/SSReflect

HOL

1. Formal reliability analysis of combinational circuits using theorem proving
2. SMT solvers: new oracles for the HOL theorem prover
3. A Formalization of the C99 Standard in HOL, Isabelle and Coq
4. Formal Verification of Chess Endgames Tables
5. A verified runtime for a verified theorem prover

Isabelle

1. Lógica Computacional en Sevilla (30 años en una hora)
2. Certifying compilers using higher-order theorem provers as certificate checkers
3. Deducción natural en lógica proposicional con Isabelle/Isar
4. Deducción natural en lógica de primer orden con Isabelle/Isar
5. A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL
6. Functional Binomial Queues
7. Lower Semicontinuous Functions
8. Formalising, improving, and reusing the Java Module System
9. Isabelle como un lenguaje funcional
10. Executable Transitive Closures of Finite Relations
11. A Formalization of the C99 Standard in HOL, Isabelle and Coq
12. Verified Firewall Policy Transformations for Test Case Generation
13. An Approach to Modular and Testable Security Models of Real-world Health-care Applications
14. Psi-calculi: a framework for mobile processes with nominal data and logic
15. Extending Sledgehammer with SMT Solvers
16. The General Triangle Is Unique
17. Mechanical Support for Efficient Dissemination on the CAN Overlay Network
18. Formal Verification of a small real-time operating system
19. Knowledge-Based Programs
20. Termination of Isabelle Functions via Termination of Rewriting
21. Efficient Interactive Construction of Machine-Checked Protocol Security Proofs in the Context of Dynamically Compromising Adversaries
22. Three Chapters of Measure Theory in Isabelle/HOL
23. seL4 Enforces Integrity
24. Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL
25. BDDs verified in a proof assistant
26. Isabelle Repository for Relational and Algebraic Methods
27. Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL

Matita

1. Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover

Mizar

1. Conway’s Games and Some of Their Basic Properties

Otter o Prover9

1. Lógica Computacional en Sevilla (30 años en una hora)
2. Recent Developments in Computing and Philosophy
3. Computational Meta-Ethics: Towards the Meta-Ethical Robot

PVS

1. Lógica Computacional en Sevilla (30 años en una hora)
2. Towards a verification framework for faulty message passing systems in PVS
3. A Formal Proof Of The Riesz Representation Theorem
4. Computationally-Discovered Simplification of the Ontological Argument
5. Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem
6. Modelling Distributed Cognition Systems in PVS

Twelfe

1. Representing model theory in a type-theoretical logical framework