The Resource Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
Resource Information
The item Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.This item is available to borrow from 1 library branch.
Resource Information
The item Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.
This item is available to borrow from 1 library branch.
- Summary
- 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 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed
- Language
- eng
- Extent
- 1 online resource (viii, 496 pages)
- Contents
-
- 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
- Isbn
- 9783540498018
- Label
- Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings
- Title
- Theorem proving in higher order logics
- Title remainder
- 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings
- Statement of responsibility
- Jim Grundy, Malcolm Newey, (eds.)
- Subject
-
- Automatic theorem proving
- Automatic theorem proving -- Congresses
- Automatische bewijsvoering
- Automatisches Beweisverfahren
- Canberra (1998)
- Conference papers and proceedings
- Conference papers and proceedings
- Conference papers and proceedings
- HOL
- Hauptverband des Osnabrücker Landvolkes
- Informatique
- Inteligencia artificial
- Kongress
- Logic, Symbolic and mathematical
- Logic, Symbolic and mathematical
- Logic, Symbolic and mathematical -- Congresses
- Logica
- Logique symbolique et mathématique -- Congrès
- Théorèmes -- Démonstration automatique | Congrès
- Automatic theorem proving
- Language
- eng
- Summary
- 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 submissions. Also included are two invited papers. The papers address all current aspects of theorem proving in higher order logics and formal verification and program analysis. Besides the HOL system, the theorem provers Coq, Isabelle, LAMBDA, LEGO, NuPrl, and PVS are discussed
- Cataloging source
- DLC
- Dewey number
- 004/.01/5113
- Illustrations
- illustrations
- Index
- index present
- Language note
- English
- LC call number
- QA76.9.A96
- LC item number
- T655 1998
- Literary form
- non fiction
- http://bibfra.me/vocab/lite/meetingDate
- 1998
- http://bibfra.me/vocab/lite/meetingName
- TPHOLs
- Nature of contents
-
- dictionaries
- bibliography
- http://library.link/vocab/relatedWorkOrContributorDate
- 1968-
- http://library.link/vocab/relatedWorkOrContributorName
-
- Grundy, J.
- Newey, Malcolm Charles
- Series statement
- Lecture notes in computer science,
- Series volume
- 1479
- http://library.link/vocab/subjectName
-
- Automatic theorem proving
- Logic, Symbolic and mathematical
- Hauptverband des Osnabrücker Landvolkes
- Automatic theorem proving
- Logic, Symbolic and mathematical
- Automatisches Beweisverfahren
- Kongress
- Logica
- Automatische bewijsvoering
- Inteligencia artificial
- Théorèmes
- Logique symbolique et mathématique
- Informatique
- HOL
- Label
- Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
- Bibliography note
- Includes bibliographical references and index
- Carrier category
- online resource
- Carrier category code
-
- cr
- Carrier MARC source
- rdacarrier
- Content category
- text
- Content type code
-
- txt
- Content type MARC source
- rdacontent
- Contents
- 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
- Control code
- 39655214
- Dimensions
- unknown
- Extent
- 1 online resource (viii, 496 pages)
- Form of item
- online
- Isbn
- 9783540498018
- Media category
- computer
- Media MARC source
- rdamedia
- Media type code
-
- c
- Other control number
- 10.1007/BFb0055125
- Other physical details
- illustrations.
- Specific material designation
- remote
- System control number
- (OCoLC)39655214
- Label
- Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
- Bibliography note
- Includes bibliographical references and index
- Carrier category
- online resource
- Carrier category code
-
- cr
- Carrier MARC source
- rdacarrier
- Content category
- text
- Content type code
-
- txt
- Content type MARC source
- rdacontent
- Contents
- 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
- Control code
- 39655214
- Dimensions
- unknown
- Extent
- 1 online resource (viii, 496 pages)
- Form of item
- online
- Isbn
- 9783540498018
- Media category
- computer
- Media MARC source
- rdamedia
- Media type code
-
- c
- Other control number
- 10.1007/BFb0055125
- Other physical details
- illustrations.
- Specific material designation
- remote
- System control number
- (OCoLC)39655214
Subject
- Automatic theorem proving
- Automatic theorem proving -- Congresses
- Automatische bewijsvoering
- Automatisches Beweisverfahren
- Canberra (1998)
- Conference papers and proceedings
- Conference papers and proceedings
- Conference papers and proceedings
- HOL
- Hauptverband des Osnabrücker Landvolkes
- Informatique
- Inteligencia artificial
- Kongress
- Logic, Symbolic and mathematical
- Logic, Symbolic and mathematical
- Logic, Symbolic and mathematical -- Congresses
- Logica
- Logique symbolique et mathématique -- Congrès
- Théorèmes -- Démonstration automatique | Congrès
- Automatic theorem proving
Genre
Member of
Library Links
Embed
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa fa-external-link-square fa-fw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Theorem-proving-in-higher-order-logics--11th/v2NU6H5Y9_w/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Theorem-proving-in-higher-order-logics--11th/v2NU6H5Y9_w/">Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)</a></span> - <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data - Experimental
Data Citation of the Item Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa fa-external-link-square fa-fw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Theorem-proving-in-higher-order-logics--11th/v2NU6H5Y9_w/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Theorem-proving-in-higher-order-logics--11th/v2NU6H5Y9_w/">Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27-October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)</a></span> - <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
