22. TPHOLs 2009: Munich, Germany
Stefan Berghofer, Tobias Nipkow, Christian Urban, Makarius Wenzel (Eds.): Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Springer 2009 Lecture Notes in Computer Science 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
- Ana Bove, Peter Dybjer, Ulf Norell: A Brief Overview of Agda - A Functional Language with Dependent Types. 73-78
- Carsten Schürmann: The Twelf Proof Assistant. 79-83
Regular Papers
- 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
- Jeremy E. Dawson, Alwen Tiu: 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, Sanaz Khan Afshar, Sofiène Tahar: 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
- 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, Georges Gonthier, Assia Mahboubi, Laurence Rideau: 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
- 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
- Thomas Tuerk: A Formalisation of Smallfoot in HOL. 469-484
- Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, Michael Norrish: Mind the Gap. 500-515
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T201401 by the dblp team