Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Turku, Finland, August 26 - 30, 1996, Proceedings, Volume 9

Front Cover
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.

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

Translating Specifications in VDMSL to PVS
1
S Agerholm
15
Modeling a Hardware Synthesis Methodology in Isabelle
33
Inference Rules for Programming Languages with
51
Proving Liveness of Fair Transition Systems
77
H Busch
92
Butler T Långbacka
107
A Case Study
125
Towards Applying the Composition Principle to Verify
235
R Heckman C Zhang B R Becker D Peticolas K N Levitt
250
Importing Mathematics from HOL into Nuprl
267
A Structure Preserving Encoding of Z in IsabelleHOL
283
Improving the Result of HighLevel Synthesis
299
Using Lattice Theory in Higher Order Logic
315
The Monomorphic Case
331
Nazareth T Nipkow
345

Elements of Mathematical Analysis in PVS
141
B Dutertre
156
Five Axioms of AlphaConversion
173
Set Theory Higher Order Logic or Both?
191
J Harrison
219
Stålmarcks Algorithm as a HOL Derived Rule
221
B Reus
379
Higher Order Annotated Terms for Proof Search
399
A Comparison of MDG and HOL for Hardware Verification
415
A Mechanisation of Computability Theory in HOL
431
Zammit
445
Copyright

About the author (1996)

John Harrison has been growing food for his family for over thirty years. He is the author of the bestselling Vegetables Growing Month by Month, The Essential Allotment Guide, and Low-Cost Living. He lives in England with his wife Val, co-author of several of his books.