22. TPHOLs 2009: Munich, Germany

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, 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

• Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi:
  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, 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
  
• 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, 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
  
• Keiko Nakata, Tarmo Uustalu:
  Trace-Based Coinductive Operational Semantics for While. 375-390
  
• Scott Owens, Susmit Sarkar, Peter Sewell:
  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, Christian Sternagel:
  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, Thomas Sewell, June Andronick, David Cock, Michael Norrish:
  Mind the Gap. 500-515