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