default search action
1. 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
- Gerwin Klein
A Formally Verified OS Kernel. Now What? 1-7 - Benjamin C. Pierce:
Proof Assistants as Teaching Assistants: A View from the Trenches. 8
Proof Pearls
- David Cachera, David Pichardie:
A Certified Denotational Abstract Interpreter. 9-24 - John R. Cowles, Ruben Gamboa:
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. 25-34 - Brian Huffman, Christian Urban:
A New Foundation for Nominal Isabelle. 35-50 - 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 - Serge Autexier
A Tactic Language for Declarative Proofs. 99-114 - 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
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. 147-162 - Thomas Braibant, Damien Pous
An Efficient Coq Tactic for Deciding Kleene Algebras. 163-178 - Sascha Böhme, Tjark Weber:
Fast LCF-Style Proof Reconstruction for Z3. 179-194 - Arthur Charguéraud:
The Optimal Fixed Point Combinator. 195-210 - Jean-François Dufourd, Yves Bertot:
Formal Study of Plane Delaunay Triangulation. 211-226 - 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 - Moa Johansson, Lucas Dixon, Alan Bundy:
Case-Analysis for Rippling and Inductive Proof. 291-306 - Chantal Keller, Benjamin Werner:
Importing HOL Light into Coq. 307-322 - Alexander Krauss, Andreas Schropp:
A Mechanized Translation from Higher-Order Logic to Set Theory. 323-338 - Peter Lammich, Andreas Lochbihler
The Isabelle Collections Framework. 339-354 - Panagiotis Manolios
Interactive Termination Proofs Using Termination Cores. 355-370 - William Mansky, Elsa L. Gunter:
A Framework for Formal Verification of Compiler Optimizations. 371-386 - Tarek Mhamdi, Osman Hasan
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 - Matthieu Sozeau:
Equations: A Dependent Pattern-Matching Compiler. 419-434 - Sol Swords
A Mechanically Verified AIG-to-BDD Conversion Algorithm. 435-449 - Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz:
Inductive Consequences in the Calculus of Constructions. 450-465 - Tjark Weber:
Validating QBF Invalidity in HOL4. 466-480
Rough Diamonds
- Douglas J. Howe:
Higher-Order Abstract Syntax in Isabelle/HOL. 481-484 - Magnus O. Myreen:
Separation Logic Adapted for Proofs by Rewriting. 485-489 - Bas Spitters
Developing the Algebraic Hierarchy with Type Classes in Coq. 490-493
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-11-15 19:20 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: