More Web Proxy on the site http://driver.im/

default search action

combined dblp search
author search
venue search
publication search

ask others

21st TPHOLs 2008: Montreal, Canada

> Home > Conferences and Workshops > TPHOLs

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/2008
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/2008
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

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Gordon08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Gordon08
Mike Gordon:
Twenty Years of Theorem Proving for HOLs Past, Present and Future. 1-5
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Miller08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Miller08
Steven P. Miller:
Will This Be Formal? 6-11

Tutorials

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Bertot08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Bertot08
Yves Bertot:
A Short Presentation of Coq. 12-16
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/KaufmannM08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/KaufmannM08
Matt Kaufmann, J Strother Moore:
An ACL2 Tutorial. 17-21
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/OwreS08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/OwreS08
Sam Owre, Natarajan Shankar:
A Brief Overview of PVS. 22-27
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/SlindN08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/SlindN08
Konrad Slind, Michael Norrish:
A Brief Overview of HOL4. 28-32
- view
  authority control:
- export record
  dblp key:
  - conf/tphol/WenzelPN08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/WenzelPN08
Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow:
The Isabelle Framework. 33-38

Regular Papers

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

Proof Pearls

- view
  authority control:
- export record
  dblp key:
  - conf/tphol/Thery08
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/tphol/Thery08
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.