20. TPHOLs 2007:
Kaiserslautern, Germany
Klaus Schneider, Jens Brandt (Eds.):
Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings.
Lecture Notes in Computer Science 4732 Springer 2007, ISBN 978-3-540-74590-7 
- 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 0.
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
Last update Sun May 26 03:46:09 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
