default search action
20. 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 - Lukas Bulwahn, Alexander Krauss, Tobias Nipkow:
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL. 38-53 - 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 - 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 - Eunsuk Kang, Mark Aagaard:
Improving the Usability of HOL Through Controlled Automation Tactics. 157-172 - Zhaozhong Ni, Dachuan Yu, Zhong Shao:
Using XCAP to Certify Realistic Systems Code: Machine Context Management. 189-206 - 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 - 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 - 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
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2015-03-02 23:58 CET by the dblp team