% Proceedings of the 6th 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{HUG93:AaLW,
   author = {M. D. Aagaard and M. E. Leeser and P. J. Windley},
   title = {Toward a Super Duper Hardware Tactic},
   pages = {399--412},
   crossref = {HUG93}}

@InProceedings{HUG93:Ager,
   author = {S. Agerholm},
   title = {Domain Theory in {HOL}},
   pages = {295--309},
   crossref = {HUG93}}

@InProceedings{HUG93:AnPP,
   author = {F. Andersen and K. D. Petersen and J. S. Pettersson},
   title = {Program Verification using {HOL-UNITY}},
   pages = {1--15},
   crossref = {HUG93}}

@InProceedings{HUG93:AINP,
   author = {P. B. Andrews and M. Bishop and S. Issar and D. Nesmith and
             F. Pfenning and H. Xi},
   title = {{TPS}: An Interactive and Automatic Tool for Proving Theorems of
            Type Theory},
   pages = {366--370},
   crossref = {HUG93}}

@InProceedings{HUG93:AnCD,
   author = {C. M. Angelo and L. Claesen and De Man, H.},
   title = {Degrees of Formality in Shallow Embedding Hardware Description
            Languages in {HOL}},
   pages = {89--100},
   crossref = {HUG93}}

@InProceedings{HUG93:ALLS,
   author = {T. Arora and T. Leung and K. Levitt and T. Schubert and
             P. Windley},
   title = {Report on the {UCD} Microcoded {Viper} Verification Project},
   pages = {239--252},
   crossref = {HUG93}}

@InProceedings{HUG93:BrCh,
   author = {S. H. Brackin and S.-K. Chin},
   title = {Server-Process Restrictiveness in {HOL}},
   pages = {450--463},
   crossref = {HUG93}}

@InProceedings{HUG93:Carr,
   author = {V. A. Carre\~no},
   title = {Verification in Higher Order Logic of Mutual Exclusion Algorithm},
   pages = {501--513},
   crossref = {HUG93}}

@InProceedings{HUG93:Chou,
   author = {C.-T. Chou},
   title = {Predicates, Temporal Logic, and Simulations},
   pages = {310--323},
   crossref = {HUG93}}

@InProceedings{HUG93:DaJo,
   author = {N. Day and J. J. Joyce},
   title = {The Semantics of Statecharts in {HOL}},
   pages = {338--351},
   crossref = {HUG93}}

@InProceedings{HUG93:EiSK,
   author = {D. Eisenbiegler and K. Schneider and R. Kumar},
   title = {A Functional Approach for Formalizing Regular Hardware Structures},
   pages = {101--114},
   crossref = {HUG93}}

@InProceedings{HUG93:FuWS,
   author = {D. A. Fura and P. J. Windley and A. K. Somani},
   title = {Abstraction Techniques for Modeling Real-World Interface Chips},
   pages = {267--280},
   crossref = {HUG93}}

@InProceedings{HUG93:Goos,
   author = {K. G. W. Goossens},
   title = {Structure and Behaviour in Hardware Verification},
   pages = {75--88},
   crossref = {HUG93}}

@InProceedings{HUG93:Gord,
   author = {A. D. Gordon},
   title = {A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion},
   pages = {413--425},
   crossref = {HUG93}}

@InProceedings{HUG93:Gunt,
   author = {E. L. Gunter},
   title = {A Broader Class of Trees for Recursive Type Definitions for {HOL}},
   pages = {141--154},
   crossref = {HUG93}}

@InProceedings{HUG93:Harr,
   author = {J. Harrison},
   title = {A {HOL} Decision Procedure for Elementary Real Algebra},
   pages = {426--436},
   crossref = {HUG93}}

@InProceedings{HUG93:HaTh,
   author = {J. Harrison and L. Th\'ery},
   title = {Extending the {HOL} Theorem Prover with a Computer Algebra System
            to Reason About the Reals},
   pages = {174--184},
   crossref = {HUG93}}

@InProceedings{HUG93:JoSe,
   author = {J. Joyce and C. Seger},
   title = {The {HOL-Voss} System:
            Model-Checking inside a General-Purpose Theorem-Prover},
   pages = {185--198},
   crossref = {HUG93}}

@InProceedings{HUG93:Kalv,
   author = {S. Kalvala},
   title = {Using {Isabelle} to Prove Simple Theorems},
   pages = {514--517},
   crossref = {HUG93}}

@InProceedings{HUG93:LuCh,
   author = {J.-Y. Lu and S.-K. Chin},
   title = {Linking Higher Order Logic to a {VLSI} {CAD} System},
   pages = {199--212},
   crossref = {HUG93}}

@InProceedings{HUG93:McIs,
   author = {A. McIsaac},
   title = {A Formalization of Abstraction in {LAMBDA}},
   pages = {227--238},
   crossref = {HUG93}}

@InProceedings{HUG93:Morl,
   author = {M. J. Morley},
   title = {Safety in Railway Signalling Data: A Behavioural Analysis},
   pages = {464--474},
   crossref = {HUG93}}

@InProceedings{HUG93:Nesi,
   author = {M. Nesi},
   title = {Value-Passing {CCS} in {HOL}},
   pages = {352--365},
   crossref = {HUG93}}

@InProceedings{HUG93:Parn,
   author = {D. L. Parnas},
   title = {Some Theorems We Should Prove},
   pages = {155--162},
   crossref = {HUG93}}

@InProceedings{HUG93:Pete,
   author = {K. D. Petersen},
   title = {Graph Model of {LAMBDA} in Higher Order Logic},
   pages = {16--28},
   crossref = {HUG93}}

@InProceedings{HUG93:Pras1,
   author = {I. S. W. B. Prasetya},
   title = {Formalization of Variables Access Constraints to Support
            Compositionality of Liveness Properties},
   pages = {324--337},
   crossref = {HUG93}}

@InProceedings{HUG93:Pras2,
   author = {I. S. W. B. Prasetya},
   title = {On the Style of Mechanical Proving},
   pages = {475--488},
   crossref = {HUG93}}

@InProceedings{HUG93:RaJS,
   author = {S. Rajan and J. Joyce and C.-J. Seger},
   title = {From Abstract Data Types to Shift Registers:
            A Case Study in Formal Specification and Verification at
            Differing Levels of Abstraction using Theorem Proving and
            Symbolic Simulation},
   pages = {489--500},
   crossref = {HUG93}}

@InProceedings{HUG93:Roxa,
   author = {R. E. O. Roxas},
   title = {A {HOL} Package for Reasoning about Relations Defined by
            Mutual Induction},
   pages = {129--140},
   crossref = {HUG93}}

@InProceedings{HUG93:RuSr,
   author = {J. Rushby and M. Srivas},
   title = {Using {PVS} to Prove Some Theorems of {David Parnas}},
   pages = {163--173},
   crossref = {HUG93}}

@InProceedings{HUG93:ScKK1,
   author = {K. Schneider and R. Kumar and T. Kropf},
   title = {Alternative Proof Procedures for Finite-State Machines in
            Higher-Order Logic},
   pages = {213--226},
   crossref = {HUG93}}

@InProceedings{HUG93:ScKK2,
   author = {K. Schneider and R. Kumar and T. Kropf},
   title = {Eliminating Higher-Order Quantifiers to Obtain Decision Procedures
            for Hardware Verification},
   pages = {385--398},
   crossref = {HUG93}}

@InProceedings{HUG93:Slin,
   author = {K. Slind},
   title = {{AC} Unification in {HOL90}},
   pages = {437--449},
   crossref = {HUG93}}

@InProceedings{HUG93:Syme,
   author = {D. Syme},
   title = {Reasoning with the Formal Definition of {Standard ML} in {HOL}},
   pages = {43--60},
   crossref = {HUG93}}

@InProceedings{HUG93:TaKu,
   author = {S. Tahar and R. Kumar},
   title = {Implementing a Methodology for Formally Verifying {RISC}
            Processors in {HOL}},
   pages = {281--294},
   crossref = {HUG93}}

@InProceedings{HUG93:Ther,
   author = {L. Th\'ery},
   title = {A Proof Development System for the {HOL} Theorem Prover},
   pages = {115--128},
   crossref = {HUG93}}

@InProceedings{HUG93:VaGu,
   author = {M. VanInwegen and E. Gunter},
   title = {{HOL-ML}},
   pages = {61--74},
   crossref = {HUG93}}

@InProceedings{HUG93:Wong,
   author = {W. Wong},
   title = {Modelling Bit Vectors in {HOL}: the {\tt word} Library},
   pages = {371--384},
   crossref = {HUG93}}

@InProceedings{HUG93:ZSOL,
   author = {C. Zhang and R. Shaw and R. A. Olsson and K. Levitt and
             M. Archer and M. R. Heckman and G. D. Benson},
   title = {Mechanizing a Programming Logic for the Concurrent Programming
            Language {microSR} in {HOL}},
   pages = {29--42},
   crossref = {HUG93}}

@InProceedings{HUG93:ZhJS,
   author = {Z. Zhu and J. Joyce and C. Seger},
   title = {Verification of the {Tamarack-3} Microprocessor in a
            Hybrid Verification Environment},
   pages = {253--266},
   crossref = {HUG93}}

@Proceedings{HUG93,
   title = {Proceedings of the 6th International Workshop on Higher Order
            Logic Theorem Proving and its Applications ({HUG}'93)},
   booktitle = {Proceedings of the 6th International Workshop on Higher Order
                Logic Theorem Proving and its Applications ({HUG}'93)},
   year = {1993},
   series = {Lecture Notes in Computer Science},
   volume = {780},
   editor = {J. J. Joyce and C.-J. H. Seger},
   publisher = {Springer-Verlag, 1994},
   address = {Vancouver, B.C., Canada},
   month = {August}}