9. TPHOLs 1996:
Turku, Finland
Joakim von Wright, Jim Grundy, John Harrison (Eds.):
Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings.
Lecture Notes in Computer Science 1125 Springer 1996, ISBN 3-540-61587-3 
- Sten Agerholm:
Translating Specifications in VDM-SL to PVS.
1-16
- Sten Agerholm, Ilya Beylin, Peter Dybjer:
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem.
17-32
- David A. Basin, Stefan Friedrich:
Modeling a Hardware Synthesis Methodology in Isabelle.
33-50
- Paul E. Black, Phillip J. Windley:
Inference Rules for Programming Languages with Side Effects in Expressions.
51-60
- Stephen H. Brackin:
Deciding Cryptographic Protocol Adequacy with HOL: The Implementation.
61-76
- Holger Busch:
Proving Liveness of Fair Transition Systems.
77-92
- Michael J. Butler, Thomas Långbacka:
Program Derivation Using the Refinement Calculator.
93-108
- Graham Collins:
A Proof Tool for Reasoning About Functional Programs.
109-124
- Solange Coupet-Grimal, Line Jakubiec:
Coq and Hardware Verification: A Case Study.
125-139
- Bruno Dutertre:
Elements of Mathematical Analysis in PVS.
141-156
- Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar:
Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL.
157-172
- Andrew D. Gordon, Thomas F. Melham:
Five Axioms of Alpha-Conversion.
173-190
- Michael J. C. Gordon:
Set Theory, Higher Order Logic or Both?
191-201
- John Harrison:
A Mizar Mode for HOL.
203-220
- John Harrison:
Stålmarck's Algorithm as a HOL Derived Rule.
221-234
- Mark Heckman, Cui Zhang, Brian R. Becker, Dave Peticolas, Karl N. Levitt, Ronald A. Olsson:
Towards Applying the Composition Principle to Verify a Microkernel Operating System.
235-250
- Barbara Heyd, Pierre Crégut:
A Modular Coding of UNITY in COQ.
251-266
- Douglas J. Howe:
Importing Mathematics from HOL into Nuprl.
267-281
- Kolyang, Thomas Santen, Burkhart Wolff:
A Structure Preserving Encoding of Z in Isabelle/HOL.
283-298
- Mats Larsson:
Improving the Result of High-Level Synthesis Using Interactive Transformational Design.
299-314
- Linas Laibinis:
Using Lattice Theory in Higher Order Logic.
315-330
- Dieter Nazareth, Tobias Nipkow:
Formal Verification of Algorithm W: The Monomorphic Case.
331-345
- Cornelia Pusch:
Verification of Compiler Correctness for the WAM.
347-361
- Bernhard Reus:
Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions.
365-380
- Konrad Slind:
Function Definition in Higher-Order Logic.
381-397
- Alan Smaill, Ian Green:
Higher-Order Annotated Terms for Proof Search.
399-413
- Sofiène Tahar, Paul Curzon:
A Comparison of MDG and HOL for Hardware Verification.
415-430
- Vincent Zammit:
A Mechanisation of Computability Theory in HOL.
431-446
Last update Sun May 26 03:46:02 2013
CET by the DBLP Team — 
Data released under the ODC-BY 1.0 license — See also our legal information page
