Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic Scholar1. ITP 2010: Edinburgh, UK
Matt Kaufmann, Lawrence C. Paulson:
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science 6172, Springer 2010, ISBN 978-3-642-14051-8
Invited Talks
Proof Pearls
- John R. Cowles, Ruben Gamboa:
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. 25-34 - Ramana Kumar, Michael Norrish:
(Nominal) Unification by Recursive Descent with Triangular Substitutions. 51-66 - Freek Verbeek, Julien Schmaltz:
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. 67-82
Regular Papers
- Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
Extending Coq with Imperative Features and Its Application to SAT Verification. 83-98 - Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Programming Language Techniques for Cryptographic Proofs. 115-130 - Jasmin Christian Blanchette, Tobias Nipkow:
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. 131-146 - Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. 147-162 - Amy P. Felty, Brigitte Pientka:
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. 227-242 - Anthony C. J. Fox, Magnus O. Myreen:
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. 243-258 - Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen:
Automated Machine-Checked Hybrid System Safety Proofs. 259-274 - Joe Hendrix, Deepak Kapur, José Meseguer:
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. 275-290 - Alexander Krauss, Andreas Schropp:
A Mechanized Translation from Higher-Order Logic to Set Theory. 323-338 - William Mansky, Elsa L. Gunter:
A Framework for Formal Verification of Compiler Optimizations. 371-386 - Tarek Mhamdi, Osman Hasan, Sofiène Tahar:
On the Formalization of the Lebesgue Integration Theory in HOL. 387-402 - Ernie Cohen, Bert Schirmer:
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. 403-418 - Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz:
Inductive Consequences in the Calculus of Constructions. 450-465
Rough Diamonds
- Bas Spitters, Eelis van der Weegen:
Developing the Algebraic Hierarchy with Type Classes in Coq. 490-493
maintained by 
, founded at 
, founded at 
last updated on 2019-02-22 23:49 CET by the dblp team
data released under the ODC-BY 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
