Theorem Proving in Higher Order Logics 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings
Other Authors: | , |
---|---|
Format: | eBook |
Language: | English |
Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
2007, 2007
|
Edition: | 1st ed. 2007 |
Series: | Theoretical Computer Science and General Issues
|
Subjects: | |
Online Access: | |
Collection: | Springer eBooks 2005- - Collection details see MPG.ReNa |
Table of Contents:
- On the Utility of Formal Methods in the Development and Certification of Software
- Formal Techniques in Software Engineering: Correct Software and Safe Systems
- Separation Logic for Small-Step cminor
- Formalising Java’s Data Race Free Guarantee
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Formalising Generalised Substitutions
- Extracting Purely Functional Contents from Logical Inductive Types
- A Modular Formalisation of Finite Group Theory
- Verifying Nonlinear Real Formulas Via Sums of Squares
- Verification of Expectation Properties for Discrete Random Variables in HOL
- A Formally Verified Prover for the Description Logic
- Proof Pearl: The Termination Analysis of Terminator
- Improving the Usability of HOL Through Controlled Automation Tactics
- Verified Decision Procedures on Context-Free Grammars
- Using XCAP to Certify Realistic Systems Code: Machine Context Management
- Proof Pearl: De Bruijn Terms Really Do Work
- Proof Pearl: Looping Around the Orbit
- Source-Level Proof Reconstruction for Interactive Theorem Proving
- Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
- Automatically Translating Type and Function Definitions from HOL to ACL2
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- Proof Pearl: Wellfounded Induction on the Ordinals Up to ? 0
- A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
- Primality Proving with Elliptic Curves
- HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism
- Building Formal Method Tools in the Isabelle/Isar Framework
- Simple Types in Type Theory: Deep and Shallow Encodings
- Mizar’s Soft Type System