Theorem Proving in Higher Order Logics 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Grundy, Jim (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Newey, Malcolm (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1998.
• Έκδοση: 1st ed. 1998.
• Σειρά: Lecture Notes in Computer Science, 1479
• Θέματα: Computer logic.; Artificial intelligence.; Software engineering.; Mathematical logic.; Logic design.; Logics and Meanings of Programs.; Artificial Intelligence.; Software Engineering/Programming and Operating Systems.; Mathematical Logic and Formal Languages.; Software Engineering.; Logic Design.

This book constitutes the refereed proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '98, held in Canberra, Australia, in September/October 1998. The 26 revised full papers presented were carefully reviewed and selected from a total of 52 submiss...

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

• Verified lexical analysis
• Extending window inference
• Program abstraction in a higher-order logic framework
• The village telephone system: A case study in formal software engineering
• Generating embeddings from denotational descriptions
• An interface between CLAM and HOL
• Classical propositional decidability via Nuprl proof extraction
• A comparison of PVS and Isabelle/HOL
• Adding external decision procedures to HOL90 securely
• Formalizing basic first order model theory
• Formalizing Dijkstra
• Mechanical verification of total correctness through diversion verification conditions
• A type annotation scheme for Nuprl
• Verifying a garbage collection algorithm
• Hot: A concurrent automated theorem prover based on higher-order tableaux
• Free variables and subexpressions in higher-order meta logic
• An LPO-based termination ordering for higher-order terms without ?-abstraction
• Proving isomorphism of first-order logic proof systems in HOL
• Exploiting parallelism in interactive theorem provers
• I/O automata and beyond: Temporal logic and abstraction in Isabelle
• Object-oriented verification based on record subtyping in Higher-Order Logic
• On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system
• Co-inductive axiomatization of a synchronous language
• Formal specification and theorem proving breakthroughs in geometric modeling
• A tool for data refinement
• Mechanizing relevant logics with HOL
• Case studies in meta-level theorem proving
• Formalization of graph search algorithms and its applications.