Borrow it
Coverart for item
The Resource Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 26-30, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds

Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 26-30, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds

Creator
Contributor
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 up-to-date report on the state of the art in this increasingly active field
Language
eng
Work
Publication
Extent
1 online resource (viii, 446 pages)
Contents
  • Translating specifications in VDM-SL 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 alpha-conversion
  • 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 high-level 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 higher-order logic
  • Higher-order annotated terms for proof search
  • A comparison of MDG and HOL for hardware verification
  • A mechanisation of computability theory in HOL
Isbn
9783540706410
Instance
Label
Theorem proving in higher order logics : 9th international conference, TPHOLs '96, Turku, Finland, August 26-30, 1996 : proceedings
Title
Theorem proving in higher order logics
Title remainder
9th international conference, TPHOLs '96, Turku, Finland, August 26-30, 1996 : proceedings
Statement of responsibility
J. von Wright, J. Grundy, J. Harrison, eds
Title variation
TPHOLs '96
Creator
Contributor
Subject
Genre
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 up-to-date report on the state of the art in this increasingly active field
Member of
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 26-30, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds
Instantiates
Publication
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 VDM-SL 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 alpha-conversion -- 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 high-level 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 higher-order logic -- Higher-order 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 26-30, 1996 : proceedings, J. von Wright, J. Grundy, J. Harrison, eds
Publication
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 VDM-SL 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 alpha-conversion -- 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 high-level 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 higher-order logic -- Higher-order 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

Genre

Member of

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012

Library Links

Structured data from the Bibframe namespace is licensed under the Creative Commons Attribution 4.0 International License by University of Missouri Libraries. Additional terms may apply to data associated with third party namespaces.
Processing Feedback ...