Theorem Proving in Higher Order Logics
9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings
Editors: Wright, Joakim von, Grundy, Jim, Harrison, John (Eds.)
Free PreviewBuy this book
- About this book
-
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.
- Table of contents (28 chapters)
-
-
Translating specifications in VDM-SL to PVS
Pages 1-16
-
A comparison of HOL and ALF formalizations of a categorical coherence theorem
Pages 17-32
-
Modeling a hardware synthesis methodology in isabelle
Pages 33-50
-
Inference rules for programming languages with side effects in expressions
Pages 51-60
-
Deciding cryptographic protocol adequacy with HOL: The implementation
Pages 61-76
-
Table of contents (28 chapters)
Recommended for you

Bibliographic Information
- Bibliographic Information
-
- Book Title
- Theorem Proving in Higher Order Logics
- Book Subtitle
- 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings
- Editors
-
- Joakim von Wright
- Jim Grundy
- John Harrison
- Series Title
- Lecture Notes in Computer Science
- Series Volume
- 1125
- Copyright
- 1996
- Publisher
- Springer-Verlag Berlin Heidelberg
- Copyright Holder
- Springer-Verlag Berlin Heidelberg
- eBook ISBN
- 978-3-540-70641-0
- DOI
- 10.1007/BFb0105392
- Series ISSN
- 0302-9743
- Edition Number
- 1
- Number of Pages
- VIII, 447
- Topics