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. Springer 1996 Lecture Notes in Computer Science 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
- 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
- Graham Collins: A Proof Tool for Reasoning About Functional Programs. 109-124
- 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
- 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
- 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
- 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
- Vincent Zammit: A Mechanisation of Computability Theory in HOL. 431-446
data released under the ODC-BY 1.0 license. See also our legal information page
last updated on 2013-06-19T203413 by the dblp team