Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Date: Wed, 25 Aug 93 9:00:30 MET DST
From: schneide <schneide@ira.uka.de>
To: info-hol@dworshak.cs.uidaho.edu
Subject: HUG92/HUG93 in bibtex
Message-Id: <"iraun1.ira.503:25.07.93.06.58.36"@ira.uka.de>

Hi,
 I have created bibtex files of the last two HOL
workshops. If anybody has done the same for the
workshop in 1991, I would like to have the bibtex
file. 
 If anybody finds a typo in the files below, I 
would be happy to know about it.

Klaus


- - ------------% HUG92 %--------------------

@proceedings{HUG92,
   address = {Leuven, Belgium},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {HUG92},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Higher Order Logic Theorem Proving and its Applications},
   volume = {A-20},
   year = {1992}
}

@inproceedings{AaLe92,
   author = {{M. Aargaard} and {M. Leeser}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {AaLe92},
   pages = {177-196},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Methodology for Reusable Hardware Proofs},
   volume = {A-20},
   year = {1992}
}

@inproceedings{AnCD92,
   author = {{C. Angelo} and {L. Claesen} and {H. DeMan}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {AnCD92},
   pages = {375-394},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {The Formal Semantics Definition of a Multi-Rate {DSP} Specification Language},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Alve92,
   author = {{J. Alves-Foss}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Alve92},
   pages = {295-306},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Modelling Non-Deterministic System in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{ArFY92,
   author = {{M. Archer} and {G. Fink} and {L. Yang}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {ArFY92},
   pages = {539-548},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Linking Other Theorem Provers to {HOL} Using {PM}: Proof Manager},
   volume = {A-20},
   year = {1992}
}

@inproceedings{BoCZ92,
   author = {{M. Bombana} and {P. Cavalloro} and {G. Zaza}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {BoCZ92},
   pages = {475-486},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Specification and Formal Synthesis of Digital Circuits},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Boul92a,
   author = {{R. Boulton}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Boul92a},
   pages = {19-38},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Lazy Approach to Fully-Expansive Theorem Proving},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Boul92b,
   author = {{R. Boulton}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Boul92b},
   pages = {133-145},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {{B}oyer-{M}oore Automation for the {HOL} System},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Busc92,
   author = {{H. Busch}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Busc92},
   pages = {97-116},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Unification Based Induction},
   volume = {A-20},
   year = {1992}
}

@inproceedings{CaHH92,
   author = {{R. Cardell-Oliver} and {R. Hale} and {J. Herbert}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {CaHH92},
   pages = {263-278},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {An Embedding of Timed Transition Systems in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Chou92a,
   author = {{C. Chou}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Chou92a},
   pages = {59-70},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Note on Interactive Theorem Proving with Theorem Continuation Functions},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Chou92b,
   author = {{C. Chou}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Chou92b},
   pages = {71-80},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Sequent Formulation of a Logic of Predicates in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Day92,
   author = {{N. Day}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Day92},
   pages = {247-262},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Comparison between Statecharts and State Transition Assertions},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Curz92,
   author = {{P. Curzon}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Curz92},
   pages = {327-346},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Deriving Correctness Properties of Compiled Code},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Goos92,
   author = {{K.G.W. Goossens} and {}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Goos92},
   pages = {487-506},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Operational Semantics Based on Formal Symbolic Simulation},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Gunt92,
   author = {{E. Gunter}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Gunt92},
   pages = {561-568},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Why we can't have {SML}-style datatype Declarations in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{HaAL92,
   author = {{W.L. Harrison} and {M. Archer} and {K.N. Levitt}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {HaAL92},
   pages = {347-358},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A {HOL} Mechanisation of the Axiomatic Semantics of a Simple Distributed Programming Language},
   volume = {A-20},
   year = {1992}
}

@inproceedings{HaWi92,
   author = {{K.M. Hall} and {P. Windley}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {HaWi92},
   pages = {507-526},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Simulating Microprocessors from Formal Specifications},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Harr92,
   author = {{J. Harrison}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Harr92},
   pages = {145-164},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Constructing the real numbers in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{HFFM92,
   author = {{R.B. Hughes} and {M.D. Francis} and {S.P. Finn} and {G. Musgrave}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {HFFM92},
   pages = {459-475},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Formal Tools in Tri-State Design in Busses},
   volume = {A-20},
   year = {1992}
}

@inproceedings{HuMu92,
   author = {{R.B. Hughes} and {G. Musgrave}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {HuMu92},
   pages = {395-406},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Desing-Flow Graph Partitioning},
   volume = {A-20},
   year = {1992}
}

@inproceedings{KaAL92,
   author = {{S. Kalwala} and {M. Archer} and {K. Levitt}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {KaAL92},
   pages = {407-426},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Implementation and Use of Annotations in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Loew92,
   author = {{P. Loewenstein}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Loew92},
   pages = {227-246},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Formal Theory of Simulations Between Infinite Automata},
   volume = {A-20},
   year = {1992}
}

@inproceedings{McAl92,
   author = {{M. McAllister}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {McAl92},
   pages = {211-226},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Machine Abstraction in Microprocessor Specification},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Melh92,
   author = {{T.F. Melham}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Melh92},
   pages = {3-18},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {The {HOL} Logic Extended with Quantification over Type Variables},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Nesi92,
   author = {{M. Nesi}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Nesi92},
   pages = {279-294},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Formalizing a Modal Logic for {CSS} in the {HOL} Theorem Prover},
   volume = {A-20},
   year = {1992}
}

@inproceedings{PLAK92,
   author = {{J. Pan} and {K. Levitt} and {M. Archer} and {S. Kalwala}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {PLAK92},
   pages = {427-448},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Pott92,
   author = {{G. Pottinger}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Pott92},
   pages = {81-96},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Classical Type Theory with Transfinite Types},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Raja92,
   author = {{P.S. Rajan}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Raja92},
   pages = {527-538},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Executing {HOL} Specifications: Towards an Evalutation Semantics for Classical Higher Order Logic},
   volume = {A-20},
   year = {1992}
}

@inproceedings{ScKK92a,
   author = {{K. Schneider} and {R. Kumar} and {Th. Kropf}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {ScKK92b},
   pages = {39-58},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Efficient Representation and Computation of Tableau Proofs},
   volume = {A-20},
   year = {1992}
}

@inproceedings{ScKK92b,
   author = {{K. Schneider} and {R. Kumar} and {Th. Kropf}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {ScKK92c},
   pages = {165-176},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Modelling generic Hardware Structures by  Abstract Datatypes},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Slin92,
   author = {{K. Slind}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Slin92},
   pages = {549-561},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Adding New Rules to an {LCF}-style Logic Implementation},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Tass92b,
   author = {{J.P. van Tassel}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Tass92b},
   pages = {359-374},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {A Formalisation of the {VHDL} Simulation Cycle},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Voor92,
   author = {{M. van der Voort}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Voor92},
   pages = {117-132},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Introducing well-founded function definitions in {HOL}},
   volume = {A-20},
   year = {1992}
}

@inproceedings{WHLL92,
   author = {{J. von Wright} and {J. Hekanaho} and {P. Luostarinen} and {T. Langbacka}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {WHLL92},
   pages = {307-326},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Mechanising some Advanced Refinement Concepts},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Wang92,
   author = {{L. Wang}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Wang92},
   pages = {449-458},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Deriving a Correct Computer},
   volume = {A-20},
   year = {1992}
}

@inproceedings{Wind92,
   author = {{P. Windley}},
   address = {Leuven, Belgium},
   booktitle = {Higher Order Logic Theorem Proving and its Applications},
   crossref = {HUG92},
   editor = {{L.J.M. Claesen} and {M.J.C. Gordon}},
   key = {Wind92},
   pages = {197-210},
   publisher = {North-Holland},
   series = {IFIP Transactions},
   title = {Abstract Theories in {HOL}},
   volume = {A-20},
   year = {1992}
}


- - ---------------------% HUG93 %-----------------

@proceedings{HUG93,
   address = {Vancouver, Canada},
   key = {HUG93},
   publisher = {Springer Verlag},
   series = {Lecture Notes in Computer Sciences},
   title = {{HOL} User's Group Workshop},
   year = {1993}
}

@inproceedings{AINP93,
   author = {{P. Andrews} and {M. Bishop} and {S. Issar} and {D. Nesmith} and {F. Pfenning} and {H. Xi}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {AINP93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {{TPS}: An Interactive and Automatic Tool for Proving Theorems of Type Theory},
   year = {1993}
}

@inproceedings{ALLS93,
   author = {{T. Arora} and {T. Leung} and {K. Levitt} and {T. Schubert} and {P. Windley}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {ALLS93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Report on the {UCD} Microcoded {V}iper Verification Project},
   year = {1993}
}

@inproceedings{AaLW93,
   author = {{M. Aargaard} and {M. Leeser} and {P. Windley}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {AaLW93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Toward a Super Duper Hardware Tactic},
   year = {1993}
}

@inproceedings{Ager93,
   author = {{S. Agerholm}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Ager93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Domain Theory in {HOL}},
   year = {1993}
}

@inproceedings{AnCD93,
   author = {{C.M. Angelo} and {L. Claesen} and {H. De Man}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {AnCD93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Degrees of Formality in Shallow Embedding Hardware Description Languages in {HOL}},
   year = {1993}
}

@inproceedings{AnPP93,
   author = {{F. Andersen} and {K.D. Petersen} and {J.S. Pettersson}},
   address = {Vancouver, Canada},
   booktitle = {{HOL} User's Group Workshop},
   crossref = {HUG93},
   key = {AnPP93},
   publisher = {Springer Verlag},
   series = {Lecture Notes in Computer Sciences},
   month = aug,
   title = {Program Verification using {HOL-UNITY}},
   year = {1993}
}

@inproceedings{Brac93,
   author = {{S. Brackin}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Brac93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Server-Process Restrictiveness in {HOL}},
   year = {1993}
}

@inproceedings{Carr93,
   author = {{V. Carreno}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Carr93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Verification in Higher-Order Logic of Mutual Exclusion Algorithm},
   year = {1993}
}

@inproceedings{Chou93,
   author = {{C.T. Chou}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Chou93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Predicates, Temporal Logic, and Simulations},
   year = {1993}
}

@inproceedings{DaJo93,
   author = {{N. Day} and {J. Joyce}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {DaJo93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {The Semantics of Statecharts in {HOL}},
   year = {1993}
}

@inproceedings{EiSK93,
   author = {{D. Eisenbiegler} and {K. Schneider} and {R. Kumar}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {EiSK93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A Functional Approach for Formalizing Regular Hardware Structures},
   year = {1993}
}

@inproceedings{FuWS93,
   author = {{D.A. Fura} and {P. Windley} and {A.K. Somani}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {FuWS93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Abstraction Techniques for Modeling Real-World Interface Chips},
   year = {1993}
}

@inproceedings{Goos93,
   author = {{K. Goossens}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Goos93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Structure and Behaviour in Hardware Verification},
   year = {1993}
}

@inproceedings{Gord93,
   author = {{A. Gordon}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Gord93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion},
   year = {1993}
}

@inproceedings{Gunt93,
   author = {{E. Gunther}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Gunt93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A Broader Class of Trees for Recursive Type Definitions for {HOL}},
   year = {1993}
}

@inproceedings{HaTh93,
   author = {{J. Harrison} and {L. Thery}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {HaTh93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Extending the {HOL} Theorem Prover with a Computer Algebra System to Reason about the Reals},
   year = {1993}
}

@inproceedings{Harr93,
   author = {{J. Harrison}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Harr93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A Decision Procedure for Elementary Real Algebra},
   year = {1993}
}

@inproceedings{JoSe93,
   author = {{J.Joyce} and {C. Seger}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {JoSe93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {The {HOL}-{V}oss System: Model-Checking inside a General-Purpose Theorem-Prover},
   year = {1993}
}

@inproceedings{Kalv93,
   author = {{S. Kalvala}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Kalv93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Using {I}sabelle to Prove Simple Theorems},
   year = {1993}
}

@inproceedings{LuCh93,
   author = {{J. Lu} and {S. Chin}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {LuCh93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Linking {HOL} to a {VLSI} {CAD} System},
   year = {1993}
}

@inproceedings{McIs93,
   author = {{A. McIsaac}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {McIs93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A Formalization of Abstraction in {LAMBDA}},
   year = {1993}
}

@inproceedings{Morl93,
   author = {{M.J. Morley}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Morl93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Safety in Railway Signaling Data: A Behavioural Analysis},
   year = {1993}
}

@inproceedings{Nesi93,
   author = {{M. Nesi}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Nesi93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Value-{P}assing {CCS} in {HOL}},
   year = {1993}
}

@inproceedings{Parn93,
   author = {{D. Parnas}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Parn93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Some Theorems We Should Prove},
   year = {1993}
}

@inproceedings{Pete93,
   author = {{K.D. Petersen}},
   address = {Vancouver, Canada},
   booktitle = {{HOL} User's Group Workshop},
   crossref = {HUG93},
   key = {Pete93},
   publisher = {Springer Verlag},
   series = {Lecture Notes in Computer Sciences},
   month = aug,
   title = {Graph model of {LAMBDA} in Higher-Order Logic},
   year = {1993}
}

@inproceedings{Pras93a,
   author = {{W. Prasetya}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Pras93a},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {On the Style of Mechanical Proving},
   year = {1993}
}

@inproceedings{Pras93b,
   author = {{W. Prasetya}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Pras93b},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Formalization of Variables Access Constraints to Support Compositionality of Liveness Properties},
   year = {1993}
}

@inproceedings{RaJS93,
   author = {{S. Rajan} and {J. Joyce} and {C. Seger}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {RaSe93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   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},
   year = {1993}
}

@inproceedings{Roxa93,
   author = {{R. Roxas}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Roxa93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A {HOL} package for Reasoning about Relations Defined by Mutual Induction},
   year = {1993}
}

@inproceedings{RuSr93,
   author = {{J. Rushby} and {M. Srivas}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {RuSr93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Using {PVS} to Prove Some Theorems Of {D}avid {P}arnas},
   year = {1993}
}

@inproceedings{ScKK93a,
   author = {{K. Schneider} and {R. Kumar} and {T. Kropf}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {ScKK93a},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Alternative Proof Procedures for Finite-State Machines in Higher-Order Logic},
   year = {1993}
}

@inproceedings{ScKK93b,
   author = {{K. Schneider} and {R. Kumar} and {Th. Kropf}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {ScKK93b},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Eliminating Higher-Order Quantifiers to Obtain Decision Procedures for Hardware Verification},
   year = {1993}
}

@inproceedings{Slin93,
   author = {{K. Slind}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Slin93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {{AC} Unification in {HOL90}},
   year = {1993}
}

@inproceedings{Syme93,
   author = {{D. Syme}},
   address = {Vancouver, Canada},
   booktitle = {{HOL} User's Group Workshop},
   crossref = {HUG93},
   key = {Syme93},
   publisher = {Springer Verlag},
   series = {Lecture Notes in Computer Sciences},
   month = aug,
   title = {Reasoning with the Formal Definition of Standard {ML} in {HOL}},
   year = {1993}
}

@inproceedings{TaKu93,
   author = {{S. Tahar} and {R. Kumar}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {TaKu93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Implementing a Methodology for Formally Verifying {RISC} Processors in {HOL}},
   year = {1993}
}

@inproceedings{Ther93,
   author = {{L. Thery}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Ther93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {A Proof Development System for {HOL}},
   year = {1993}
}

@inproceedings{VaGu93,
   author = {{M. Van{I}nwegen} and {E. Gunter}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {VaGu93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   series = {Lecture Notes in Computer Sciences},
   month = aug,
   title = {{HOL-ML}},
   year = {1993}
}

@inproceedings{Wind93,
   author = {{P.J. Windley}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Wind93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Abstraction Techniques for Modeling Real-World Interface Chips},
   year = {1993}
}

@inproceedings{Wong93,
   author = {{W. Wong}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {Wong93},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Modelling Bit Vectors in {HOL}: the {\tt word} Library},
   year = {1993}
}

@inproceedings{ZSOL93,
   author = {{C. Zhang} and {R. Shaw} and {R. Olsson} and {K. Levitt} and {M. Archer} and {M. Heckman} and {G. Benson}},
   address = {Vancouver, Canada},
   booktitle = {{HOL} User's Group Workshop},
   crossref = {HUG93},
   key = {ZSOL93},
   publisher = {Springer Verlag},
   series = {Lecture Notes in Computer Sciences},
   month = aug,
   title = {Mechanizing a Programming Logic for the Concurrent Programming Language micro{SR} in {HOL}},
   year = {1993}
}

@inproceedings{ZhJS93,
   author = {{Z. Zhu} and {J. Joyce} and {C. Seger}},
   address = {Vancouver, Canada},
   crossref = {HUG93},
   key = {ZhJS9},
   booktitle = {{HOL} User's Group Workshop},
   publisher = {Springer Verlag},
   month = aug,
   title = {Verification of the {T}amarack-3 Microprocessor in a Hybrid Verification Environment},
   year = {1993}
}