% Proceedings of the 4th International Workshop on
% the HOL Theorem Proving System and its Applications
%
% The entry for the full proceedings is at the end of the file.

% Tutorial Papers
% ===============

@InProceedings{HUG91:Tut:Card,
   author = {R. Cardell-Oliver},
   title = {On the use of the {HOL} system for Protocol Verification},
   pages = {59--62},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Chin,
   author = {S.-K. Chin},
   title = {Verifying Arithmetic Hardware in Higher-Order Logic},
   pages = {22--31},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Gord,
   author = {M. Gordon},
   title = {Introduction to the {HOL} System},
   pages = {2--3},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Hale,
   author = {R. Hale},
   title = {Reasoning About Software},
   pages = {52--58},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:HarL,
   author = {W. L. Harrison and K. N. Levitt},
   title = {Mechanizing Security in {HOL}},
   pages = {63--66},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Herb,
   author = {J. Herbert},
   title = {Dealing With Temporal Complexity in Hardware Verification},
   pages = {13--21},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Kalv,
   author = {S. Kalvala},
   title = {{HOL} Around the World},
   pages = {4--12},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Loew,
   author = {P. Loewenstein},
   title = {Learning to use {HOL}},
   pages = {67--74},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Schu,
   author = {E. T. Schubert},
   title = {Verification of Integrated Subsystems},
   pages = {38--51},
   crossref = {HUG91}}

@InProceedings{HUG91:Tut:Wind,
   author = {P. J. Windley},
   title = {The Practical Verification of Microprocessor Designs},
   pages = {32--37},
   crossref = {HUG91}}

% Workshop Papers
% ===============

@InProceedings{HUG91:Ager,
   author = {S. Agerholm},
   title = {Mechanizing Program Verification in {HOL}},
   pages = {208--222},
   crossref = {HUG91}}

@InProceedings{HUG91:AlLe,
   author = {J. Alves-Foss and K. Levitt},
   title = {Mechanical Verification of Secure Distributed Systems in Higher
            Order Logic},
   pages = {263--278},
   crossref = {HUG91}}

@InProceedings{HUG91:AnPe,
   author = {F. Andersen and K. D. Petersen},
   title = {Recursive Boolean Functions in {HOL}},
   pages = {367--377},
   crossref = {HUG91}}

@InProceedings{HUG91:AVCD,
   author = {C. M. Angelo and D. Verkest and L. Claesen and De Man, H.},
   title = {Formal Hardware Verification in {HOL} and in {Boyer-Moore}:
            A Comparative Analysis},
   pages = {340--347},
   crossref = {HUG91}}

@InProceedings{HUG91:Arth,
   author = {R. D. Arthan},
   title = {A Report on {ICL} {HOL}},
   pages = {280--283},
   crossref = {HUG91}}

@InProceedings{HUG91:BaCF,
   author = {S. Bainbridge and A. Camilleri and R. Fleming},
   title = {Industrial Application of Theorem Proving to System Level Design},
   pages = {130--142},
   crossref = {HUG91}}

@InProceedings{HUG91:deBa,
   author = {de Barros Lucena, E.},
   title = {Reasoning about {Petri} Nets in {HOL}},
   pages = {384--394},
   crossref = {HUG91}}

@InProceedings{HUG91:ChBi,
   author = {S.-K. Chin and G. Birtwistle},
   title = {Implementing and Verifying Finite-State Machines Using Types in
            Higher-Order Logic},
   pages = {121--129},
   crossref = {HUG91}}

@InProceedings{HUG91:Curz,
   author = {P. Curzon},
   title = {A Verified Compiler for a Structured Assembly Language},
   pages = {253--262},
   crossref = {HUG91}}

@InProceedings{HUG91:FiAY,
   author = {G. Fink and M. Archer and L. Yang},
   title = {{PM}: A Proof Manager for {HOL} and Other Provers},
   pages = {286--304},
   crossref = {HUG91}}

@InProceedings{HUG91:GaWi,
   author = {J. W. Gambles and P. J. Windley},
   title = {An {HOL} Theory for Logic States with Indeterminate Strengths},
   pages = {96--103},
   crossref = {HUG91}}

@InProceedings{HUG91:GeGL,
   author = {R. Gerber and E. L. Gunter and I. Lee},
   title = {Implementing a Real-Time Process Algebra in {HOL}},
   pages = {144--154},
   crossref = {HUG91}}

@InProceedings{HUG91:Grun,
   author = {J. Grundy},
   title = {Window Inference in the {HOL} System},
   pages = {177--189},
   crossref = {HUG91}}

@InProceedings{HUG91:Kalv,
   author = {S. Kalvala},
   title = {Developing an Interface for {HOL}},
   pages = {305--317},
   crossref = {HUG91}}

@InProceedings{HUG91:Kauf,
   author = {M. Kaufmann},
   title = {An Informal Discussion of Issues in Mechanically-Assisted
            Reasoning},
   pages = {318--337},
   crossref = {HUG91}}

@InProceedings{HUG91:Keut,
   author = {K. Keutzer},
   title = {The Need for Formal Verification in Hardware Design and
            What Formal Verification Has Not Done for Me Lately},
   pages = {77--86},
   crossref = {HUG91}}

@InProceedings{HUG91:KuKS1,
   author = {R. Kumar and T. Kropf and K. Schneider},
   title = {Integrating a First-Order Automatic Prover in the {HOL}
            Environment},
   pages = {170--176},
   crossref = {HUG91}}

@InProceedings{HUG91:KuKS2,
   author = {R. Kumar and T. Kropf and K. Schneider},
   title = {First Steps Towards Automating Hardware Proofs in {HOL}},
   pages = {190--193},
   crossref = {HUG91}}

@InProceedings{HUG91:MaTo,
   author = {D. F. Martin and R. J. Toal},
   title = {Case Studies in Compiler Correctness Using {HOL}},
   pages = {242--252},
   crossref = {HUG91}}

@InProceedings{HUG91:Melh,
   author = {T. F. Melham},
   title = {A Package for Inductive Relation Definitions in {HOL}},
   pages = {350--357},
   crossref = {HUG91}}

@InProceedings{HUG91:Newe,
   author = {M. C. Newey},
   title = {Proof Based Computation},
   pages = {380--383},
   crossref = {HUG91}}

@InProceedings{HUG91:PlCD,
   author = {W. Ploegaerts and L. Claesen and De Man, H.},
   title = {Defining Recursive Functions in {HOL}},
   pages = {358--366},
   crossref = {HUG91}}

@InProceedings{HUG91:RoNe,
   author = {R. Roxas and M. Newey},
   title = {Proof of Program Transformations},
   pages = {223--230},
   crossref = {HUG91}}

@InProceedings{HUG91:Rush,
   author = {J. Rushby},
   title = {Design Choices in Specification Languages and Verification
            Systems},
   pages = {195--204},
   crossref = {HUG91}}

@InProceedings{HUG91:Schu,
   author = {E. T. Schubert},
   title = {Verification of Composed Hardware Systems Using {CCS}},
   pages = {88--95},
   crossref = {HUG91}}

@InProceedings{HUG91:Shep,
   author = {D. Shepherd},
   title = {Using {HOL} to produce custom verification tools},
   pages = {162--169},
   crossref = {HUG91}}

@InProceedings{HUG91:WaSt,
   author = {X. Wang and E. P. Stabler},
   title = {Formalization of {VHDL} Synthesis Procedure in Higher-Order Logic},
   pages = {106--120},
   crossref = {HUG91}}

@InProceedings{HUG91:Wong,
   author = {W. Wong},
   title = {A Simple Graph Theory and Its Application in Railway Signalling},
   pages = {395--409},
   crossref = {HUG91}}

@InProceedings{HUG91:vonW,
   author = {J. von Wright},
   title = {Mechanising the Temporal Logic of Actions in {HOL}},
   pages = {155--159},
   crossref = {HUG91}}

@InProceedings{HUG91:vWSe,
   author = {J. von Wright and K. Sere},
   title = {Program Transformations and Refinements in {HOL}},
   pages = {231--239},
   crossref = {HUG91}}

@Proceedings{HUG91,
   title = {Proceedings of the 1991 International Workshop on the
            {HOL} Theorem Proving System and its Applications},
   booktitle = {Proceedings of the 1991 International Workshop on the
                {HOL} Theorem Proving System and its Applications},
   year = {1991},
   editor = {M. Archer and J. J. Joyce and K. N. Levitt and P. J. Windley},
   publisher = {IEEE Computer Society Press, 1992},
   address = {Davis, California, USA},
   month = {August}}