Theorem Proving in Higher Order Logics 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Hurd, Joe (Επιμελητής έκδοσης), Melham, Tom (Επιμελητής έκδοσης)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg, 2005.
• Σειρά: Lecture Notes in Computer Science, 3603
• Θέματα: Computer science.; Architecture, Computer.; Software engineering.; Computers.; Computer logic.; Mathematical logic.; Artificial intelligence.; Computer Science.; Theory of Computation.; Computer System Implementation.; Mathematical Logic and Formal Languages.; Logics and Meanings of Programs.; Software Engineering.; Artificial Intelligence (incl. Robotics).

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

Πίνακας περιεχομένων:

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