% Proceedings of the 5th International Workshop on % Higher Order Logic Theorem Proving and its Applications % % The entry for the full proceedings is at the end of the file. @InProceedings{HUG92:AaLe, author = {M. Aargaard and M. Leeser}, title = {A Methodology for Reusable Hardware Proofs}, pages = {177--196}, crossref = {HUG92}} @InProceedings{HUG92:AnCD, author = {C. Angelo and L. Claesen and De Man, H.}, title = {The Formal Semantics Definition of a Multi-Rate {DSP} Specification Language}, pages = {375--394}, crossref = {HUG92}} @InProceedings{HUG92:Alve, author = {J. Alves-Foss}, title = {Modelling Non-Deterministic System in {HOL}}, pages = {295--306}, crossref = {HUG92}} @InProceedings{HUG92:ArFY, author = {M. Archer and G. Fink and L. Yang}, title = {Linking Other Theorem Provers to {HOL} Using {PM}: Proof Manager}, pages = {539--548}, crossref = {HUG92}} @InProceedings{HUG92:BoCZ, author = {M. Bombana and P. Cavalloro and G. Zaza}, title = {Specification and Formal Synthesis of Digital Circuits}, pages = {475--486}, crossref = {HUG92}} @InProceedings{HUG92:Boul1, author = {R. J. Boulton}, title = {A Lazy Approach to Fully-Expansive Theorem Proving}, pages = {19--38}, crossref = {HUG92}} @InProceedings{HUG92:Boul2, author = {R. J. Boulton}, title = {{Boyer}-{Moore} Automation for the {HOL} System}, pages = {133--145}, crossref = {HUG92}} @InProceedings{HUG92:Busc, author = {H. Busch}, title = {Unification Based Induction}, pages = {97--116}, crossref = {HUG92}} @InProceedings{HUG92:CaHH, author = {R. Cardell-Oliver and R. Hale and J. Herbert}, title = {An Embedding of Timed Transition Systems in {HOL}}, pages = {263--278}, crossref = {HUG92}} @InProceedings{HUG92:Chou1, author = {C.-T. Chou}, title = {A Note on Interactive Theorem Proving with Theorem Continuation Functions}, pages = {59--70}, crossref = {HUG92}} @InProceedings{HUG92:Chou2, author = {C.-T. Chou}, title = {A Sequent Formulation of a Logic of Predicates in {HOL}}, pages = {71--80}, crossref = {HUG92}} @InProceedings{HUG92:Day92, author = {N. Day}, title = {A Comparison between Statecharts and State Transition Assertions}, pages = {247--262}, crossref = {HUG92}} @InProceedings{HUG92:Curz, author = {P. Curzon}, title = {Deriving Correctness Properties of Compiled Code}, pages = {327--346}, crossref = {HUG92}} @InProceedings{HUG92:Goos, author = {K. G. W. Goossens}, title = {Operational Semantics Based on Formal Symbolic Simulation}, pages = {487--506}, crossref = {HUG92}} @InProceedings{HUG92:Gunt, author = {E. Gunter}, title = {Why we can't have {SML}-style datatype Declarations in {HOL}}, pages = {561--568}, crossref = {HUG92}} @InProceedings{HUG92:HaAL, author = {W. L. Harrison and M. Archer and K. N. Levitt}, title = {A {HOL} Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language}, pages = {347--358}, crossref = {HUG92}} @InProceedings{HUG92:HaWi, author = {K. M. Hall and P. Windley}, title = {Simulating Microprocessors from Formal Specifications}, pages = {507--526}, crossref = {HUG92}} @InProceedings{HUG92:Harr, author = {J. Harrison}, title = {Constructing the real numbers in {HOL}}, pages = {145--164}, crossref = {HUG92}} @InProceedings{HUG92:HFFM, author = {R. B. Hughes and M. D. Francis and S. P. Finn and G. Musgrave}, title = {Formal Tools in Tri-State Design in Busses}, pages = {459--475}, crossref = {HUG92}} @InProceedings{HUG92:HuMu, author = {R. B. Hughes and G. Musgrave}, title = {Design-Flow Graph Partitioning}, pages = {395--406}, crossref = {HUG92}} @InProceedings{HUG92:KaAL, author = {S. Kalvala and M. Archer and K. Levitt}, title = {Implementation and Use of Annotations in {HOL}}, pages = {407--426}, crossref = {HUG92}} @InProceedings{HUG92:Loew, author = {P. Loewenstein}, title = {A Formal Theory of Simulations Between Infinite Automata}, pages = {227--246}, crossref = {HUG92}} @InProceedings{HUG92:McAl, author = {M. McAllister}, title = {Machine Abstraction in Microprocessor Specification}, pages = {211--226}, crossref = {HUG92}} @InProceedings{HUG92:Melh, author = {T. F. Melham}, title = {The {HOL} Logic Extended with Quantification over Type Variables}, pages = {3--18}, crossref = {HUG92}} @InProceedings{HUG92:Nesi, author = {M. Nesi}, title = {Formalizing a Modal Logic for {CSS} in the {HOL} Theorem Prover}, pages = {279--294}, crossref = {HUG92}} @InProceedings{HUG92:PLAK, author = {J. Pan and K. Levitt and M. Archer and S. Kalvala}, title = {Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit}, pages = {427--448}, crossref = {HUG92}} @InProceedings{HUG92:Pott, author = {G. Pottinger}, title = {A Classical Type Theory with Transfinite Types}, pages = {81--96}, crossref = {HUG92}} @InProceedings{HUG92:Raja, author = {P. S. Rajan}, title = {Executing {HOL} Specifications: Towards an Evaluation Semantics for Classical Higher Order Logic}, pages = {527--538}, crossref = {HUG92}} @InProceedings{HUG92:ScKK1, author = {K. Schneider and R. Kumar and T. Kropf}, title = {Efficient Representation and Computation of Tableau Proofs}, pages = {39--58}, crossref = {HUG92}} @InProceedings{HUG92:ScKK2, author = {K. Schneider and R. Kumar and T. Kropf}, title = {Modelling generic Hardware Structures by Abstract Datatypes}, pages = {165--176}, crossref = {HUG92}} @InProceedings{HUG92:Slin, author = {K. Slind}, title = {Adding New Rules to an {LCF}-style Logic Implementation}, pages = {549--561}, crossref = {HUG92}} @InProceedings{HUG92:VanT, author = {Van Tassel, J. P.}, title = {A Formalisation of the {VHDL} Simulation Cycle}, pages = {359--374}, crossref = {HUG92}} @InProceedings{HUG92:Voor, author = {M. van der Voort}, title = {Introducing well-founded function definitions in {HOL}}, pages = {117--132}, crossref = {HUG92}} @InProceedings{HUG92:WHLL, author = {J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka}, title = {Mechanising some Advanced Refinement Concepts}, pages = {307--326}, crossref = {HUG92}} @InProceedings{HUG92:Wang, author = {L. Wang}, title = {Deriving a Correct Computer}, pages = {449--458}, crossref = {HUG92}} @InProceedings{HUG92:Wind, author = {P. Windley}, title = {Abstract Theories in {HOL}}, pages = {197--210}, crossref = {HUG92}} @Proceedings{HUG92, title = {Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 Workshop}, booktitle = {Higher Order Logic Theorem Proving and its Applications: Proceedings of the IFIP TC10/WG10.2 Workshop}, series = {{IFIP} Transactions}, volume = {A-20}, year = {1992}, editor = {L. J. M. Claesen and M. J. C. Gordon}, publisher = {North-Holland/Elsevier}, address = {Leuven, Belgium}, month = {September}}