The Resource Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 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 27October 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 2 library branches.
Resource Information
The item Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 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 2 library branches.
 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
 viii, 496 pages
 Contents

 Verified lexical analysis
 Extending window inference
 Program abstraction in a higherorder 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 higherorder tableaux
 Free variables and subexpressions in higherorder meta logic
 An LPObased termination ordering for higherorder terms without?abstraction
 Proving isomorphism of firstorder logic proof systems in HOL
 Exploiting parallelism in interactive theorem provers
 I/O automata and beyond: Temporal logic and abstraction in Isabelle
 Objectoriented verification based on record subtyping in HigherOrder Logic
 On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a highlevel synthesis system
 Coinductive 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 metalevel theorem proving
 Formalization of graph search algorithms and its applications
 Isbn
 9783540649878
 Label
 Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 1, 1998 : proceedings
 Title
 Theorem proving in higher order logics
 Title remainder
 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 1, 1998 : proceedings
 Statement of responsibility
 Jim Grundy, Malcolm Newey, (eds.)
 Subject

 Automatic theorem proving
 Automatic theorem proving  Congresses
 Canberra (1998)
 Conference papers and proceedings
 Conference papers and proceedings
 Informatique
 Logic, Symbolic and mathematical
 Logic, Symbolic and mathematical
 Logic, Symbolic and mathematical  Congresses
 Logique symbolique et mathématique  Congrès
 TPHOLs
 Théorèmes  Démonstration automatique  Congrès
 higher order logics
 theorem proving
 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
 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
 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
 11479
 http://library.link/vocab/subjectName

 Automatic theorem proving
 Logic, Symbolic and mathematical
 Automatic theorem proving
 Logic, Symbolic and mathematical
 Théorèmes
 Logique symbolique et mathématique
 Informatique
 Label
 Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
 Bibliography note
 Includes bibliographical references and index
 Carrier category
 volume
 Carrier category code

 nc
 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 higherorder 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 higherorder tableaux  Free variables and subexpressions in higherorder meta logic  An LPObased termination ordering for higherorder terms without?abstraction  Proving isomorphism of firstorder logic proof systems in HOL  Exploiting parallelism in interactive theorem provers  I/O automata and beyond: Temporal logic and abstraction in Isabelle  Objectoriented verification based on record subtyping in HigherOrder Logic  On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a highlevel synthesis system  Coinductive 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 metalevel theorem proving  Formalization of graph search algorithms and its applications
 Control code
 190833527
 Dimensions
 24 cm.
 Extent
 viii, 496 pages
 Isbn
 9783540649878
 Lccn
 98039442
 Media category
 unmediated
 Media MARC source
 rdamedia
 Media type code

 n
 Other physical details
 illustrations
 System control number
 (OCoLC)190833527
 Label
 Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 1, 1998 : proceedings, Jim Grundy, Malcolm Newey, (eds.)
 Bibliography note
 Includes bibliographical references and index
 Carrier category
 volume
 Carrier category code

 nc
 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 higherorder 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 higherorder tableaux  Free variables and subexpressions in higherorder meta logic  An LPObased termination ordering for higherorder terms without?abstraction  Proving isomorphism of firstorder logic proof systems in HOL  Exploiting parallelism in interactive theorem provers  I/O automata and beyond: Temporal logic and abstraction in Isabelle  Objectoriented verification based on record subtyping in HigherOrder Logic  On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a highlevel synthesis system  Coinductive 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 metalevel theorem proving  Formalization of graph search algorithms and its applications
 Control code
 190833527
 Dimensions
 24 cm.
 Extent
 viii, 496 pages
 Isbn
 9783540649878
 Lccn
 98039442
 Media category
 unmediated
 Media MARC source
 rdamedia
 Media type code

 n
 Other physical details
 illustrations
 System control number
 (OCoLC)190833527
Subject
 Automatic theorem proving
 Automatic theorem proving  Congresses
 Canberra (1998)
 Conference papers and proceedings
 Conference papers and proceedings
 Informatique
 Logic, Symbolic and mathematical
 Logic, Symbolic and mathematical
 Logic, Symbolic and mathematical  Congresses
 Logique symbolique et mathématique  Congrès
 TPHOLs
 Théorèmes  Démonstration automatique  Congrès
 higher order logics
 theorem proving
 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 faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Theoremprovinginhigherorderlogics11th/4wkRsEIGprM/" 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/Theoremprovinginhigherorderlogics11th/4wkRsEIGprM/">Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 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 27October 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 faexternallinksquare fafw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Theoremprovinginhigherorderlogics11th/4wkRsEIGprM/" 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/Theoremprovinginhigherorderlogics11th/4wkRsEIGprM/">Theorem proving in higher order logics : 11th international conference, TPHOLs '98, Canberra, Australia, September 27October 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>