default search action
22nd TPHOLs 2009: Munich, Germany
- Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel:
Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Lecture Notes in Computer Science 5674, Springer 2009, ISBN 978-3-642-03358-2
Invited Papers
- David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt:
Let's Get Physical: Models and Methods for Real-World Security Protocols. 1-22 - Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies:
VCC: A Practical System for Verifying Concurrent C. 23-42 - John Harrison:
Without Loss of Generality. 43-59
Invited Tutorials
- John Harrison:
HOL Light: An Overview. 60-66 - Adam Naumowicz
, Artur Kornilowicz
A Brief Overview of Mizar. 67-72 - Ana Bove
A Brief Overview of Agda - A Functional Language with Dependent Types. 73-78 - Carsten Schürmann:
The Twelf Proof Assistant. 79-83
Regular Papers
- Andrea Asperti
Hints in Unification. 84-98 - Jesper Bengtson, Joachim Parrow:
Psi-calculi in Isabelle. 99-114 - Nick Benton, Andrew Kennedy, Carsten Varming:
Some Domain Theory and Denotational Semantics in Coq. 115-130 - Stefan Berghofer, Lukas Bulwahn, Florian Haftmann:
Turning Inductive into Equational Specifications. 131-146 - Stefan Berghofer, Markus Reiter:
Formalizing the Logic-Automaton Connection. 147-163 - Chad E. Brown, Gert Smolka:
Extended First-Order Logic. 164-179 - Jeremy E. Dawson
Formalising Observer Theory for Environment-Sensitive Bisimulation. 180-195 - Javier de Dios, Ricardo Peña-Marí:
Formal Certification of a Resource-Aware Language Implementation. 196-211 - Frédéric Dabrowski, David Pichardie:
A Certified Data Race Analysis for a Java-like Language. 212-227 - Osman Hasan
Formal Analysis of Optical Waveguides in HOL. 228-243 - Peter V. Homeier:
The HOL-Omega Logic. 244-259 - Brian Huffman:
A Purely Definitional Universal Domain. 260-275 - Rafal Kolanski, Gerwin Klein
Types, Maps and Separation Logic. 276-292 - Stéphane Le Roux:
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence. 293-309 - Andreas Lochbihler
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. 310-326 - François Garillot
Packaging Mathematical Structures. 327-342 - Andrew McCreight:
Practical Tactics for Separation Logic. 343-358 - Magnus O. Myreen, Michael J. C. Gordon:
Verified LISP Implementations on ARM, x86 and PowerPC. 359-374 - Keiko Nakata, Tarmo Uustalu
Trace-Based Coinductive Operational Semantics for While. 375-390 - Scott Owens
A Better x86 Memory Model: x86-TSO. 391-407 - Nicolas Julien, Ioana Pasca:
Formal Verification of Exact Computations Using Newton's Method. 408-423 - Alexander Schimpf, Stephan Merz, Jan-Georg Smaus:
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. 424-439 - Wouter Swierstra:
A Hoare Logic for the State Monad. 440-451 - René Thiemann
Certification of Termination Proofs Using CeTA. 452-468 - Thomas Tuerk:
A Formalisation of Smallfoot in HOL. 469-484 - Jinshuang Wang, Huabing Yang, Xingyuan Zhang:
Liveness Reasoning with Isabelle/HOL. 485-499 - Simon Winwood, Gerwin Klein
Mind the Gap. 500-515
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 2025-03-08 00:35 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: