default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID21st TPHOLs 2008: Montreal, Canada
- Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar:
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 A. 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
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 2026-01-18 21:57 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:
