The Resource Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds
Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds
Resource Information
The item Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, 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 : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, 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 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an uptodate report on the state of the art in this increasingly active field
 Language
 eng
 Extent
 1 online resource (viii, 446 pages)
 Contents

 Translating specifications in VDMSL to PVS
 A comparison of HOL and ALF formalizations of a categorical coherence theorem
 Modeling a hardware synthesis methodology in isabelle
 Inference rules for programming languages with side effects in expressions
 Deciding cryptographic protocol adequacy with HOL: The implementation
 Proving liveness of fair transition systems
 Program derivation using the refinement calculator
 A proof tool for reasoning about functional programs
 Coq and hardware verification: A case study
 Elements of mathematical analysis in PVS
 Implementation issues about the embedding of existing high level synthesis algorithms in HOL
 Five axioms of alphaconversion
 Set theory, higher order logic or both?
 A mizar mode for HOL
 Stålmarck's algorithm as a HOL derived rule
 Towards applying the composition principle to verify a microkernel operating system
 A modular coding of UNITY in COQ
 Importing mathematics from HOL into Nuprl
 A structure preserving encoding of Z in isabelle/HOL
 Improving the result of highlevel synthesis using interactive transformational design
 Using lattice theory in higher order logic
 Formal verification of algorithm W: The monomorphic case
 Verification of compiler correctness for the WAM
 Synthetic domain theory in type theory: Another logic of computable functions
 Function definition in higherorder logic
 Higherorder annotated terms for proof search
 A comparison of MDG and HOL for hardware verification
 A mechanisation of computability theory in HOL
 Isbn
 9783540706410
 Label
 Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings
 Title
 Theorem proving in higher order logics
 Title remainder
 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings
 Statement of responsibility
 J. von Wright, J. Grundy, J. Harrison, eds
 Title variation
 TPHOLs '96
 Subject

 Automatic theorem proving
 Automatic theorem proving  Congresses
 Automatische bewijsvoering
 Automatisches Beweisverfahren
 Computer Science
 Conference papers and proceedings
 Conference papers and proceedings
 Engineering & Applied Sciences
 HOL
 Kongress
 Logica
 Théorèmes  Démonstration automatique  Congrès
 Turku (1996)
 Automatic theorem proving
 Language
 eng
 Summary
 This book constitutes the refereed proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOL '96, held in Turku, Finland, in August 1996. The 27 revised full papers included together with one invited paper were carefully selected from a total of 46 submissions. The topics addressed are theorem proving technology, proof automation and decision procedures, mechanized theorem proving, extensions of higher order logics, integration of external tools, novel applications, and others. All in all, the volume is an uptodate report on the state of the art in this increasingly active field
 Action
 digitized
 Cataloging source
 OCLCE
 Dewey number
 004/.01/5113
 Illustrations
 illustrations
 Index
 index present
 LC call number
 QA76.9.A96
 LC item number
 I577 1996
 Literary form
 non fiction
 http://bibfra.me/vocab/lite/meetingDate
 1996
 http://bibfra.me/vocab/lite/meetingName
 TPHOLs
 Nature of contents

 dictionaries
 bibliography
 http://library.link/vocab/relatedWorkOrContributorDate

 1955
 1968
 1966
 http://library.link/vocab/relatedWorkOrContributorName

 Wright, J. von
 Grundy, J.
 Harrison, J.
 Series statement
 Lecture notes in computer science,
 Series volume
 1125
 http://library.link/vocab/subjectName

 Automatic theorem proving
 Automatic theorem proving
 Automatisches Beweisverfahren
 Logica
 Automatische bewijsvoering
 Computer Science
 Engineering & Applied Sciences
 Théorèmes
 HOL
 Label
 Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds
 Antecedent source
 file reproduced from original
 Bibliography note
 Includes bibliographical references and index
 Carrier category
 online resource
 Carrier category code

 cr
 Carrier MARC source
 rdacarrier
 Color
 black and white
 Content category
 text
 Content type code

 txt
 Content type MARC source
 rdacontent
 Contents
 Translating specifications in VDMSL to PVS  A comparison of HOL and ALF formalizations of a categorical coherence theorem  Modeling a hardware synthesis methodology in isabelle  Inference rules for programming languages with side effects in expressions  Deciding cryptographic protocol adequacy with HOL: The implementation  Proving liveness of fair transition systems  Program derivation using the refinement calculator  A proof tool for reasoning about functional programs  Coq and hardware verification: A case study  Elements of mathematical analysis in PVS  Implementation issues about the embedding of existing high level synthesis algorithms in HOL  Five axioms of alphaconversion  Set theory, higher order logic or both?  A mizar mode for HOL  Stålmarck's algorithm as a HOL derived rule  Towards applying the composition principle to verify a microkernel operating system  A modular coding of UNITY in COQ  Importing mathematics from HOL into Nuprl  A structure preserving encoding of Z in isabelle/HOL  Improving the result of highlevel synthesis using interactive transformational design  Using lattice theory in higher order logic  Formal verification of algorithm W: The monomorphic case  Verification of compiler correctness for the WAM  Synthetic domain theory in type theory: Another logic of computable functions  Function definition in higherorder logic  Higherorder annotated terms for proof search  A comparison of MDG and HOL for hardware verification  A mechanisation of computability theory in HOL
 Control code
 681302677
 Dimensions
 unknown
 Extent
 1 online resource (viii, 446 pages)
 Form of item
 online
 Isbn
 9783540706410
 Level of compression

 lossless
 lossy
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code

 c
 Other control number
 10.1007/BFb0105392.
 Other physical details
 illustrations.
 Reformatting quality

 preservation
 access
 Reproduction note
 Electronic reproduction.
 Specific material designation
 remote
 System control number
 (OCoLC)681302677
 System details
 Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002.
 Label
 Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds
 Antecedent source
 file reproduced from original
 Bibliography note
 Includes bibliographical references and index
 Carrier category
 online resource
 Carrier category code

 cr
 Carrier MARC source
 rdacarrier
 Color
 black and white
 Content category
 text
 Content type code

 txt
 Content type MARC source
 rdacontent
 Contents
 Translating specifications in VDMSL to PVS  A comparison of HOL and ALF formalizations of a categorical coherence theorem  Modeling a hardware synthesis methodology in isabelle  Inference rules for programming languages with side effects in expressions  Deciding cryptographic protocol adequacy with HOL: The implementation  Proving liveness of fair transition systems  Program derivation using the refinement calculator  A proof tool for reasoning about functional programs  Coq and hardware verification: A case study  Elements of mathematical analysis in PVS  Implementation issues about the embedding of existing high level synthesis algorithms in HOL  Five axioms of alphaconversion  Set theory, higher order logic or both?  A mizar mode for HOL  Stålmarck's algorithm as a HOL derived rule  Towards applying the composition principle to verify a microkernel operating system  A modular coding of UNITY in COQ  Importing mathematics from HOL into Nuprl  A structure preserving encoding of Z in isabelle/HOL  Improving the result of highlevel synthesis using interactive transformational design  Using lattice theory in higher order logic  Formal verification of algorithm W: The monomorphic case  Verification of compiler correctness for the WAM  Synthetic domain theory in type theory: Another logic of computable functions  Function definition in higherorder logic  Higherorder annotated terms for proof search  A comparison of MDG and HOL for hardware verification  A mechanisation of computability theory in HOL
 Control code
 681302677
 Dimensions
 unknown
 Extent
 1 online resource (viii, 446 pages)
 Form of item
 online
 Isbn
 9783540706410
 Level of compression

 lossless
 lossy
 Media category
 computer
 Media MARC source
 rdamedia
 Media type code

 c
 Other control number
 10.1007/BFb0105392.
 Other physical details
 illustrations.
 Reformatting quality

 preservation
 access
 Reproduction note
 Electronic reproduction.
 Specific material designation
 remote
 System control number
 (OCoLC)681302677
 System details
 Master and use copy. Digital master created according to Benchmark for Faithful Digital Reproductions of Monographs and Serials, Version 1. Digital Library Federation, December 2002.
Subject
 Automatic theorem proving
 Automatic theorem proving  Congresses
 Automatische bewijsvoering
 Automatisches Beweisverfahren
 Computer Science
 Conference papers and proceedings
 Conference papers and proceedings
 Engineering & Applied Sciences
 HOL
 Kongress
 Logica
 Théorèmes  Démonstration automatique  Congrès
 Turku (1996)
 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/Theoremprovinginhigherorderlogics9th/pLKlWaZEMY/" 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/Theoremprovinginhigherorderlogics9th/pLKlWaZEMY/">Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, 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 : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, 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/Theoremprovinginhigherorderlogics9th/pLKlWaZEMY/" 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/Theoremprovinginhigherorderlogics9th/pLKlWaZEMY/">Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 2630, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, 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>