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 BibTeX

@proceedings{DBLP:conf/tphol/1996,
  editor    = {Joakim von Wright and
               Jim Grundy and
               John Harrison},
  title     = {Theorem Proving in Higher Order Logics, 9th International Conference,
               TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings},
  booktitle = {TPHOLs},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1125},
  year      = {1996},
  isbn      = {3-540-61587-3},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Sten Agerholm: Translating Specifications in VDM-SL to PVS. 1-16 BibTeX
Sten Agerholm, Ilya Beylin, Peter Dybjer: A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. 17-32 BibTeX
David A. Basin, Stefan Friedrich: Modeling a Hardware Synthesis Methodology in Isabelle. 33-50 BibTeX
Paul E. Black, Phillip J. Windley: Inference Rules for Programming Languages with Side Effects in Expressions. 51-60 BibTeX
Stephen H. Brackin: Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. 61-76 BibTeX
Holger Busch: Proving Liveness of Fair Transition Systems. 77-92 BibTeX
Michael J. Butler, Thomas Långbacka: Program Derivation Using the Refinement Calculator. 93-108 BibTeX
Graham Collins: A Proof Tool for Reasoning About Functional Programs. 109-124 BibTeX
Solange Coupet-Grimal, Line Jakubiec: Coq and Hardware Verification: A Case Study. 125-139 BibTeX
Bruno Dutertre: Elements of Mathematical Analysis in PVS. 141-156 BibTeX
Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar: Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL. 157-172 BibTeX
Andrew D. Gordon, Thomas F. Melham: Five Axioms of Alpha-Conversion. 173-190 BibTeX
Michael J. C. Gordon: Set Theory, Higher Order Logic or Both? 191-201 BibTeX
John Harrison: A Mizar Mode for HOL. 203-220 BibTeX
John Harrison: Stålmarck's Algorithm as a HOL Derived Rule. 221-234 BibTeX
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 BibTeX
Barbara Heyd, Pierre Crégut: A Modular Coding of UNITY in COQ. 251-266 BibTeX
Douglas J. Howe: Importing Mathematics from HOL into Nuprl. 267-281 BibTeX
Kolyang, Thomas Santen, Burkhart Wolff: A Structure Preserving Encoding of Z in Isabelle/HOL. 283-298 BibTeX
Mats Larsson: Improving the Result of High-Level Synthesis Using Interactive Transformational Design. 299-314 BibTeX
Linas Laibinis: Using Lattice Theory in Higher Order Logic. 315-330 BibTeX
Dieter Nazareth, Tobias Nipkow: Formal Verification of Algorithm W: The Monomorphic Case. 331-345 BibTeX
Cornelia Pusch: Verification of Compiler Correctness for the WAM. 347-361 BibTeX
Bernhard Reus: Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions. 365-380 BibTeX
Konrad Slind: Function Definition in Higher-Order Logic. 381-397 BibTeX
Alan Smaill, Ian Green: Higher-Order Annotated Terms for Proof Search. 399-413 BibTeX
Sofiène Tahar, Paul Curzon: A Comparison of MDG and HOL for Hardware Verification. 415-430 BibTeX
Vincent Zammit: A Mechanisation of Computability Theory in HOL. 431-446 BibTeX