@string{TYPES="Types for Proofs and Programs"}
@string{prg = "Programming Research Group"}
@string{oucl = "Oxford University Computing Laboratory"}
@string{cucl = "University of Cambridge, Computer Laboratory"}
@string{oxford = "Parks Road, Oxford, UK"}
@string{uk = "UK"}
@string{lncs = "Lecture Notes in Computer Science"}

@inproceedings{Herbert88,
  author = {J. M. J. Herbert},
  title = {Temporal Abstraction of Digital Designs},
  editor = {G. J. Milne},
  booktitle = {Proceedings of the IFIP WG 10.2 Working
    Conference},
  month = {Glasgow, July,},
  year = "1988",
  publisher = "North-Holland",
  pages = {1-25}
}



@InCollection{WhyHOL,
  author        = "M. J. C. Gordon",
  title         = "Why higher-order logic is a good formalism for specifying
                   and verifying hardware",  
  crossref      = {milne86},
  pages         = "153--177"}


@book{HOLbook,
  editor = {M. J. C. Gordon and T. F. Melham},
  title = {Introduction to {HOL}: 
    A Theorem-proving Environment for {Higher-Order Logic}},
  publisher = {Cambridge University Press},
  year = 1993
}


@book{Melhambook,
  editor = {T. F. Melham},
  title = {Higher Order Logic and Hardware Verification},
  publisher = {Cambridge University Press},
  series = {Cambridge Tracts in Theoretical Computer Science 31},
  year = 1993
}

@misc{SMVdocs,
 author = "K. L. McMillan",
 title = "The {SMV} Language",
 institution = "Cadence",
 month  = "June",
 year = 1998,
 note = "Available on the WWW at:
          {\tt http://www-cad.eecs.berkeley.edu/${\sim}$kenmcmil/psdoc.html}"}


@misc{GhoshGordon,
 author = "M. J. C. Gordon and A. Ghosh",
 title = "Language Independent {RTL} Semantics",
 note = "Draft of an invited
           contribution to the 
           1998 IEEE CS Annual Workshop on VLSI: System Level Design in Orlando Florida. 
           The paper was not presented, due to flights into Orlando being full!
           Available on the WWW at: 
           {\tt http://www.cl.cam.ac.uk/users/mjcg/OrlandoPaper.ps}"}

@misc{EventCycle,
 author = "M. J. C. Gordon",
 title = "Event and Cycle Semantics of Hardware Description Languages",
 note = "Unpublished draft paper. Available on the WWW at: 
           {\tt http://www.cl.cam.ac.uk/users/mjcg/Verilog/V/HDLpaper.ps}"}

@misc{LUSTRE,
 author  = "Nicolas Halbwachs",
 note = "LUSTRE is a functional stream-based synchronous declarative language for programming 
         reactive systems: 
           {\tt http://www-verimag.imag.fr//SYNCHRONE/lustre-english.html}"}

@misc{VFE,
 author = "M. J. C. Gordon",
 note = "Various draft papers on the formal semantics of Verilog HDL arising from the VFE project. 
         Available on the web at:
           {\tt http://www.cl.cam.ac.uk/users/mjcg/Verilog/V/V.html}"}


@misc{MyraVerilog,
 author = "Myra Van Inwegen",
 note = "Two reports: one on Verilog's expression evaluation and 
         one on Verilog's expression normalization.
         Available on the web at:
         {\tt http://www.cl.cam.ac.uk/users/mvi20/handel/verilog.html}"}

@book{McMillanBook,
 author = {Kenneth L. McMillan},
 title = {Symbolic Model Checking},
 publisher = {Kluwer Academic Publishers},
 year = 1993
}


@Manual{Synopsys,
 title = {HDL Compiler for Verilog Reference Manual, Version 3.5},
 organization = {Synopsys, Inc.},
 month = "September",
 year = "1996"
}

@Book{ThomasMoorby,
 Author = "Donald E. Thomas and Philip R. Moorby",
 Title = "The {Verilog} Hardware Description Language",
 Publisher = "Kluwer Academic Publishers",
 Year = "1996",
 Edition = {3rd}
}