Theorem Proving in Higher Order Logics 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings
This volume constitutes the proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), which was held during22–25August2005inOxford,UK.TPHOLscoversallaspectsoftheorem proving in higher order logics as well as related topics in theorem proving and veri?c...
Other Authors: | , |
---|---|
Format: | eBook |
Language: | English |
Published: |
Berlin, Heidelberg
Springer Berlin Heidelberg
2005, 2005
|
Edition: | 1st ed. 2005 |
Series: | Theoretical Computer Science and General Issues
|
Subjects: | |
Online Access: | |
Collection: | Springer eBooks 2005- - Collection details see MPG.ReNa |
Table of Contents:
- Invited Papers
- On the Correctness of Operating System Kernels
- Alpha-Structural Recursion and Induction
- Regular Papers
- Shallow Lazy Proofs
- Mechanized Metatheory for the Masses: The PoplMark Challenge
- A Structured Set of Higher-Order Problems
- Formal Modeling of a Slicing Algorithm for Java Event Spaces in PVS
- Proving Equalities in a Commutative Ring Done Right in Coq
- A HOL Theory of Euclidean Space
- A Design Structure for Higher Order Quotients
- Axiomatic Constructor Classes in Isabelle/HOLCF
- Meta Reasoning in ACL2
- Reasoning About Java Programs with Aliasing and Frame Conditions
- Real Number Calculations and Theorem Proving
- Verifying a Secure Information Flow Analyzer
- Proving Bounds for Real Linear Programs in Isabelle/HOL
- Essential Incompleteness of Arithmetic Verified by Coq
- Verification of BDD Normalization
- Extensionality in the Calculus of Constructions
- A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
- A Generic Network on Chip Model
- Formal Verification of a SHA-1 Circuit Core Using ACL2
- From PSL to LTL: A Formal Validation in HOL
- Proof Pearls
- Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2
- Proof Pearl: Dijkstra’s Shortest Path Algorithm Verified with ACL2
- Proof Pearl: Defining Functions over Finite Sets
- Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof