Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic Scholar22. 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-22Ernie 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-42John Harrison:
Without Loss of Generality. 43-59
Invited Tutorials
John Harrison:
HOL Light: An Overview. 60-66Adam Naumowicz, Artur Kornilowicz:
A Brief Overview of Mizar. 67-72Ana Bove, Peter Dybjer, Ulf Norell:
A Brief Overview of Agda - A Functional Language with Dependent Types. 73-78Carsten Schürmann:
The Twelf Proof Assistant. 79-83
Regular Papers
Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi:
Hints in Unification. 84-98Jesper Bengtson, Joachim Parrow:
Psi-calculi in Isabelle. 99-114Nick Benton, Andrew Kennedy, Carsten Varming:
Some Domain Theory and Denotational Semantics in Coq. 115-130Stefan Berghofer, Lukas Bulwahn, Florian Haftmann:
Turning Inductive into Equational Specifications. 131-146Stefan Berghofer, Markus Reiter:
Formalizing the Logic-Automaton Connection. 147-163Chad E. Brown, Gert Smolka:
Extended First-Order Logic. 164-179Jeremy E. Dawson, Alwen Tiu:
Formalising Observer Theory for Environment-Sensitive Bisimulation. 180-195Javier de Dios, Ricardo Peña-Marí:
Formal Certification of a Resource-Aware Language Implementation. 196-211Frédéric Dabrowski, David Pichardie:
A Certified Data Race Analysis for a Java-like Language. 212-227Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar:
Formal Analysis of Optical Waveguides in HOL. 228-243Peter V. Homeier:
The HOL-Omega Logic. 244-259Brian Huffman:
A Purely Definitional Universal Domain. 260-275Rafal Kolanski, Gerwin Klein:
Types, Maps and Separation Logic. 276-292Stéphane Le Roux:
Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence. 293-309Andreas Lochbihler:
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. 310-326François Garillot, Georges Gonthier, Assia Mahboubi, Laurence Rideau:
Packaging Mathematical Structures. 327-342Andrew McCreight:
Practical Tactics for Separation Logic. 343-358Magnus O. Myreen, Michael J. C. Gordon:
Verified LISP Implementations on ARM, x86 and PowerPC. 359-374Keiko Nakata, Tarmo Uustalu:
Trace-Based Coinductive Operational Semantics for While. 375-390Scott Owens, Susmit Sarkar, Peter Sewell:
A Better x86 Memory Model: x86-TSO. 391-407Nicolas Julien, Ioana Pasca:
Formal Verification of Exact Computations Using Newton's Method. 408-423Alexander Schimpf, Stephan Merz, Jan-Georg Smaus:
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. 424-439Wouter Swierstra:
A Hoare Logic for the State Monad. 440-451René Thiemann, Christian Sternagel:
Certification of Termination Proofs Using CeTA. 452-468Thomas Tuerk:
A Formalisation of Smallfoot in HOL. 469-484Jinshuang Wang, Huabing Yang, Xingyuan Zhang:
Liveness Reasoning with Isabelle/HOL. 485-499Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish:
Mind the Gap. 500-515
last updated on 2019-07-23 22:47 CEST by the dblp team
data released under the ODC-BY 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
