20. TPHOLs 2007: Kaiserslautern, Germany

• Constance L. Heitmeyer:
  On the Utility of Formal Methods in the Development and Certification of Software. 1-2
  
• Peter Liggesmeyer:
  Formal Techniques in Software Engineering: Correct Software and Safe Systems. 3-4
  
• Andrew W. Appel, Sandrine Blazy:
  Separation Logic for Small-Step cminor. 5-21
  
• David Aspinall, Jaroslav Sevcík:
  Formalising Java's Data Race Free Guarantee. 22-37
  
• Lukas Bulwahn, Alexander Krauss, Tobias Nipkow:
  Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. 38-53
  
• Jeremy E. Dawson:
  Formalising Generalised Substitutions. 54-69
  
• David Delahaye, Catherine Dubois, Jean-Frédéric Étienne:
  Extracting Purely Functional Contents from Logical Inductive Types. 70-85
  
• Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry:
  A Modular Formalisation of Finite Group Theory. 86-101
  
• John Harrison:
  Verifying Nonlinear Real Formulas Via Sums of Squares. 102-118
  
• Osman Hasan, Sofiène Tahar:
  Verification of Expectation Properties for Discrete Random Variables in HOL. 119-134
  
• José-Antonio Alonso, Joaquín Borrego-Díaz, María-José Hidalgo, Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina:
  A Formally Verified Prover for the ALC Description Logic. 135-150
  
• Joe Hurd:
  Proof Pearl: The Termination Analysis of Terminator. 151-156
  
• Eunsuk Kang, Mark Aagaard:
  Improving the Usability of HOL Through Controlled Automation Tactics. 157-172
  
• Yasuhiko Minamide:
  Verified Decision Procedures on Context-Free Grammars. 173-188
  
• Zhaozhong Ni, Dachuan Yu, Zhong Shao:
  Using XCAP to Certify Realistic Systems Code: Machine Context Management. 189-206
  
• Michael Norrish, René Vestergaard:
  Proof Pearl: De Bruijn Terms Really Do Work. 207-222
  
• Steven Obua:
  Proof Pearl: Looping Around the Orbit. 223-231
  
• Lawrence C. Paulson, Kong Woei Susanto:
  Source-Level Proof Reconstruction for Interactive Theorem Proving. 232-245
  
• Brigitte Pientka:
  Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF. 246-261
  
• James Reynolds:
  Automatically Translating Type and Function Definitions from HOL to ACL2. 262-277
  
• Tom Ridge:
  Operational Reasoning for Concurrent Caml Programs and Weak Memory Models. 278-293
  
• Matt Kaufmann, Konrad Slind:
  Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon ₀. 294-301
  
• Christoph Sprenger, David A. Basin:
  A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. 302-318
  
• Laurent Théry, Guillaume Hanrot:
  Primality Proving with Elliptic Curves. 319-333
  
• Norbert Völker:
  HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism. 334-351
  
• Makarius Wenzel, Burkhart Wolff:
  Building Formal Method Tools in the Isabelle/Isar Framework. 352-367
  
• François Garillot, Benjamin Werner:
  Simple Types in Type Theory: Deep and Shallow Encodings. 368-382
  
• Freek Wiedijk:
  Mizar's Soft Type System. 383-399