default search action
20th TPHOLs 2007: Kaiserslautern, Germany
- Klaus Schneider
, Jens Brandt
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
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
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 D. 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
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
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
Simple Types in Type Theory: Deep and Shallow Encodings. 368-382 - Freek Wiedijk:
Mizar's Soft Type System. 383-399
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2024-12-26 01:01 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: