Cover Image
Read Now

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...

Full description

Bibliographic Details
Other Authors: Hurd, Joe (Editor), Melham, Tom (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2005, 2005
Edition:1st ed. 2005
Series:Theoretical Computer Science and General Issues
Subjects:
Computer Systems
Computer Science Logic And Foundations Of Programming
Software Engineering
Computer Science
Computer System Implementation
Artificial Intelligence
Formal Languages And Automata Theory
Machine Theory
Theory Of Computation
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

Similar Items