21. TPHOLs 2008: Montreal, Canada

Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar (Eds.): Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings. Lecture Notes in Computer Science 5170 Springer 2008, ISBN 978-3-540-71065-3

Invited Papers

Mike Gordon:
Twenty Years of Theorem Proving for HOLs Past, Present and Future. 1-5
Steven P. Miller:
Will This Be Formal? 6-11

Tutorials

Yves Bertot:
A Short Presentation of Coq. 12-16
Matt Kaufmann, J. Strother Moore:
An ACL2 Tutorial. 17-21
Sam Owre, Natarajan Shankar:
A Brief Overview of PVS. 22-27
Konrad Slind, Michael Norrish:
A Brief Overview of HOL4. 28-32
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow:
The Isabelle Framework. 33-38

Regular Papers

Klaus Aehlig, Florian Haftmann, Tobias Nipkow:
A Compiled Implementation of Normalization by Evaluation. 39-54
Hasan Amjad:
LCF-Style Propositional Simplification with BDDs and SAT Solvers. 55-70
Stefan Berghofer, Christian Urban:
Nominal Inversion Principles. 71-85
Yves Bertot, Georges Gonthier, Sidi Ould Biha, Ioana Pasca:
Canonical Big Operators. 86-101
Ana Bove, Venanzio Capretta:
A Type of Partial Recursive Functions. 102-117
Jens Brandt, Klaus Schneider:
Formal Reasoning About Causality Analysis. 118-133
Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkök, John Matthews:
Imperative Functional Programming with Isabelle/HOL. 134-149
Sascha Böhme, K. Rustan M. Leino, Burkhart Wolff:
HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. 150-166
David Cock, Gerwin Klein, Thomas Sewell:
Secure Microkernels, State Monads and Scalable Refinement. 167-182
Pierre Courtieu, Julien Forest, Xavier Urbain:
Certifying a Termination Criterion Based on Graphs, without Graphs. 183-198
Holger Gast:
Lightweight Separation. 199-214
David R. Lester:
Real Number Calculations and Theorem Proving. 215-229
Sayan Mitra, K. Mani Chandy:
A Formalized Theory for Verifying Stability and Convergence of Automata in PVS. 230-245
Russell O'Connor:
Certified Exact Transcendental Real Number Computation in Coq. 246-261
Polyvios Pratikakis, Jeffrey S. Foster, Michael Hicks, Iulian Neamtiu:
Formalizing Soundness of Contextual Effects. 262-277
Matthieu Sozeau, Nicolas Oury:
First-Class Type Classes. 278-293
Daniel Wasserrab, Andreas Lochbihler:
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. 294-309

Proof Pearls

Laurent Théry:
Proof Pearl: Revisiting the Mini-rubik in Coq. 310-319

Last update Tue May 21 00:58:15 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page