% Proceedings of the 9th International Conference on
% Theorem Proving in Higher Order Logics
%
% The entry for the full proceedings is at the end of the file.

@InProceedings{TPHOLs96:Ager,
   author = {S. Agerholm},
   title = {Translating Specifications in {VDM-SL} to {PVS}},
   pages = {1--16},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:AgBD,
   author = {S. Agerholm and I. Beylin and P. Dybjer},
   title = {A Comparison of {HOL} and {ALF} Formalizations of a Categorical
            Coherence Theorem},
   pages = {17--32},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:BaFr,
   author = {D. Basin and S. Friedrich},
   title = {Modeling a Hardware Synthesis Methodology in {Isabelle}},
   pages = {33--50},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:BlWi,
   author = {P. E. Black and P. J. Windley},
   title = {Inference Rules for Programming Languages with Side Effects in
            Expressions},
   pages = {51--60},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Brac,
   author = {S. H. Brackin},
   title = {Deciding Cryptographic Protocol Adequacy with {HOL}:
            The Implementation},
   pages = {61--76},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Busc,
   author = {H. Busch},
   title = {Proving Liveness of Fair Transition Systems},
   pages = {77--92},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:BuLa,
   author = {M. Butler and T. L{\aa}ngbacka},
   title = {Program Derivation Using the {Refinement Calculator}},
   pages = {93--108},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Coll,
   author = {G. Collins},
   title = {A Proof Tool for Reasoning About Functional Programs},
   pages = {109--124},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:CoJa,
   author = {S. Coupet-Grimal and L. Jakubiec},
   title = {{Coq} and Hardware Verification: A Case Study},
   pages = {125--139},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Dute,
   author = {B. Dutertre},
   title = {Elements of Mathematical Analysis in {PVS}},
   pages = {141--156},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:EiBK,
   author = {D. Eisenbiegler and C. Blumenr\"ohr and R. Kumar},
   title = {Implementation Issues About the Embedding of Existing High Level
            Synthesis Algorithms in {HOL}},
   pages = {157--172},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:GoMe,
   author = {A. D. Gordon and T. Melham},
   title = {Five Axioms of Alpha-Conversion},
   pages = {173--190},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Gord,
   author = {M. Gordon},
   title = {Set Theory, Higher Order Logic or Both?},
   pages = {191--201},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Harr1,
   author = {J. Harrison},
   title = {A {Mizar} Mode for {HOL}},
   pages = {203--220},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Harr2,
   author = {J. Harrison},
   title = {{St{\aa}lmarck}'s Algorithm as a {HOL} Derived Rule},
   pages = {221--234},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:HZBPLO,
   author = {M. R. Heckman and C. Zhang and B. R. Becker and D. Peticolas and
             K. N. Levitt and R. A. Olsson},
   title = {Towards Applying the Composition Principle to Verify a Microkernel
            Operating System},
   pages = {235--250},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:HeCr,
   author = {B. Heyd and P. Cr\'egut},
   title = {A Modular Coding of {Unity} in {Coq}},
   pages = {251--266},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Howe,
   author = {D. J. Howe},
   title = {Importing Mathematics from {HOL} into {Nuprl}},
   pages = {267--281},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:KoSW,
   author = {Kolyang and T. Santen and B. Wolff},
   title = {A Structure Preserving Encoding of {Z} in {Isabelle}/{HOL}},
   pages = {283--298},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Lars,
   author = {M. Larsson},
   title = {Improving the Result of High-Level Synthesis Using Interactive
            Transformational Design},
   pages = {299--314},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Laib,
   author = {L. Laibinis},
   title = {Using Lattice Theory in Higher Order Logic},
   pages = {315--330},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:NaNi,
   author = {D. Nazareth and T. Nipkow},
   title = {Formal Verification of Algorithm {W}: The Monomorphic Case},
   pages = {331--345},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Pusc,
   author = {C. Pusch},
   title = {Verification of Compiler Correctness for the {WAM}},
   pages = {347--361},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Reus,
   author = {B. Reus},
   title = {Synthetic Domain Theory in Type Theory: Another Logic of
            Computable Functions},
   pages = {363--380},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Slin,
   author = {K. Slind},
   title = {Function Definition in Higher-Order Logic},
   pages = {381--397},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:SmGr,
   author = {A. Smaill and I. Green},
   title = {Higher-Order Annotated Terms for Proof Search},
   pages = {399--413},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:TaCu,
   author = {S. Tahar and P. Curzon},
   title = {A Comparison of {MDG} and {HOL} for Hardware Verification},
   pages = {415--430},
   crossref = {TPHOLs96}}

@InProceedings{TPHOLs96:Zamm,
   author = {V. Zammit},
   title = {A Mechanisation of Computability Theory in {HOL}},
   pages = {431--446},
   crossref = {TPHOLs96}}

@Proceedings{TPHOLs96,
   title = {Proceedings of the 9th International Conference on
            Theorem Proving in Higher Order Logics (TPHOLs'96)},
   booktitle = {Proceedings of the 9th International Conference on
                Theorem Proving in Higher Order Logics (TPHOLs'96)},
   year = {1996},
   series = {Lecture Notes in Computer Science},
   volume = {1125},
   editor = {J. von Wright and J. Grundy and J. Harrison},
   publisher = {Springer},
   address = {Turku, Finland},
   month = {August}}