Coverart for item
The Resource Theorem Proving in Higher Order Logics : 10th International Conference, TPHOLs '97 Murray Hill, NJ, USA, August 19–22, 1997 Proceedings, edited by Elsa L. Gunter, Amy Felty, (electronic resource)

Theorem Proving in Higher Order Logics : 10th International Conference, TPHOLs '97 Murray Hill, NJ, USA, August 19–22, 1997 Proceedings, edited by Elsa L. Gunter, Amy Felty, (electronic resource)

Label
Theorem Proving in Higher Order Logics : 10th International Conference, TPHOLs '97 Murray Hill, NJ, USA, August 19–22, 1997 Proceedings
Title
Theorem Proving in Higher Order Logics
Title remainder
10th International Conference, TPHOLs '97 Murray Hill, NJ, USA, August 19–22, 1997 Proceedings
Statement of responsibility
edited by Elsa L. Gunter, Amy Felty
Creator
Contributor
Editor
Provider
Subject
Language
eng
Summary
This book constitutes the refereed proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '97, held in Murray Hill, NJ, USA, in August 1997. The volume presents 19 carefully revised full papers selected from 32 submissions during a thorough reviewing process. The papers cover work related to all aspects of theorem proving in higher order logics, particularly based on secure mechanization of those logics; the theorem proving systems addressed include Coq, HOL, Isabelle, LEGO, and PVS
Member of
http://library.link/vocab/creatorName
Gunter, Elsa L
Image bit depth
0
LC call number
QA8.9-QA10.3
Literary form
non fiction
http://library.link/vocab/relatedWorkOrContributorName
  • Felty, Amy.
  • SpringerLink
Series statement
Lecture Notes in Computer Science,
Series volume
1275
http://library.link/vocab/subjectName
  • Computer science
  • Logic design
  • Software engineering
  • Logic, Symbolic and mathematical
  • Computer Science
  • Mathematical Logic and Formal Languages
  • Logic Design
  • Software Engineering
  • Logics and Meanings of Programs
  • Mathematical Logic and Foundations
Label
Theorem Proving in Higher Order Logics : 10th International Conference, TPHOLs '97 Murray Hill, NJ, USA, August 19–22, 1997 Proceedings, edited by Elsa L. Gunter, Amy Felty, (electronic resource)
Instantiates
Publication
Antecedent source
mixed
Carrier category
online resource
Carrier category code
cr
Carrier MARC source
rdacarrier
Color
not applicable
Content category
text
Content type code
txt
Content type MARC source
rdacontent
Contents
An Isabelle-based theorem prover for VDM-SL -- Executing formal specifications by translation to higher order logic programming -- Human-style theorem proving using PVS -- A hybrid approach to verifying liveness in a symmetric multi-processor -- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis -- ML programming in constructive type theory -- Possibly infinite sequences in theorem provers: A comparative study -- Proof normalization for a first-order formulation of higher-order logic -- Using a PVS embedding of CSP to verify authentication protocols -- Verifying the accuracy of polynomial approximations in HOL -- A full formalisation of ?-calculus theory in the calculus of constructions -- Rewriting, decision procedures and lemma speculation for automated hardware verification -- Refining reactive systems in HOL using action systems -- On formalization of bicategory theory -- Towards an object-oriented progification language -- Verification for robust specification -- A theory of structured model-based specifications in Isabelle/HOL -- Proof presentation for Isabelle -- Derivation and use of induction schemes in higher-order logic -- Higher order quotients and their implementation in Isabelle HOL -- Type classes and overloading in higher-order logic -- A comparative study of Coq and HOL
Dimensions
unknown
Extent
X, 346 p.
File format
multiple file formats
Form of item
electronic
Isbn
9783540695264
Level of compression
uncompressed
Media category
computer
Media MARC source
rdamedia
Media type code
c
Other control number
10.1007/BFb0028381
Other physical details
online resource.
Quality assurance targets
absent
Reformatting quality
access
Specific material designation
remote
System control number
(DE-He213)978-3-540-69526-4
Label
Theorem Proving in Higher Order Logics : 10th International Conference, TPHOLs '97 Murray Hill, NJ, USA, August 19–22, 1997 Proceedings, edited by Elsa L. Gunter, Amy Felty, (electronic resource)
Publication
Antecedent source
mixed
Carrier category
online resource
Carrier category code
cr
Carrier MARC source
rdacarrier
Color
not applicable
Content category
text
Content type code
txt
Content type MARC source
rdacontent
Contents
An Isabelle-based theorem prover for VDM-SL -- Executing formal specifications by translation to higher order logic programming -- Human-style theorem proving using PVS -- A hybrid approach to verifying liveness in a symmetric multi-processor -- Formal verification of concurrent programs in Lp and in Coq: A comparative analysis -- ML programming in constructive type theory -- Possibly infinite sequences in theorem provers: A comparative study -- Proof normalization for a first-order formulation of higher-order logic -- Using a PVS embedding of CSP to verify authentication protocols -- Verifying the accuracy of polynomial approximations in HOL -- A full formalisation of ?-calculus theory in the calculus of constructions -- Rewriting, decision procedures and lemma speculation for automated hardware verification -- Refining reactive systems in HOL using action systems -- On formalization of bicategory theory -- Towards an object-oriented progification language -- Verification for robust specification -- A theory of structured model-based specifications in Isabelle/HOL -- Proof presentation for Isabelle -- Derivation and use of induction schemes in higher-order logic -- Higher order quotients and their implementation in Isabelle HOL -- Type classes and overloading in higher-order logic -- A comparative study of Coq and HOL
Dimensions
unknown
Extent
X, 346 p.
File format
multiple file formats
Form of item
electronic
Isbn
9783540695264
Level of compression
uncompressed
Media category
computer
Media MARC source
rdamedia
Media type code
c
Other control number
10.1007/BFb0028381
Other physical details
online resource.
Quality assurance targets
absent
Reformatting quality
access
Specific material designation
remote
System control number
(DE-He213)978-3-540-69526-4

Library Locations

  • African Studies LibraryBorrow it
    771 Commonwealth Avenue, 6th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Alumni Medical LibraryBorrow it
    72 East Concord Street, Boston, MA, 02118, US
    42.336388 -71.072393
  • Astronomy LibraryBorrow it
    725 Commonwealth Avenue, 6th Floor, Boston, MA, 02445, US
    42.350259 -71.105717
  • Fineman and Pappas Law LibrariesBorrow it
    765 Commonwealth Avenue, Boston, MA, 02215, US
    42.350979 -71.107023
  • Frederick S. Pardee Management LibraryBorrow it
    595 Commonwealth Avenue, Boston, MA, 02215, US
    42.349626 -71.099547
  • Howard Gotlieb Archival Research CenterBorrow it
    771 Commonwealth Avenue, 5th Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Mugar Memorial LibraryBorrow it
    771 Commonwealth Avenue, Boston, MA, 02215, US
    42.350723 -71.108227
  • Music LibraryBorrow it
    771 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350723 -71.108227
  • Pikering Educational Resources LibraryBorrow it
    2 Silber Way, Boston, MA, 02215, US
    42.349804 -71.101425
  • School of Theology LibraryBorrow it
    745 Commonwealth Avenue, 2nd Floor, Boston, MA, 02215, US
    42.350494 -71.107235
  • Science & Engineering LibraryBorrow it
    38 Cummington Mall, Boston, MA, 02215, US
    42.348472 -71.102257
  • Stone Science LibraryBorrow it
    675 Commonwealth Avenue, Boston, MA, 02445, US
    42.350103 -71.103784
Processing Feedback ...