% Bibliography for "Z & HOL" paper.
% November 1993

@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"}


@article{Church,
 author = {A. Church},
 title = {A Formulation of the Simple Theory of Types},
 journal = {The Journal of Symbolic Logic},
 year = {1940},
 volume = {5},
 pages = {56-68}
}

@book{Andrews,
 author = {P. D. Andrews},
 title = {An Introduction to Mathematical Logic and Type Theory:
   To Truth through Proof},
 series = {Computer Science and Applied Mathematics Series},
 publisher = {Academic Press},
 year = {1986}
}

@manual{Z:Spiv92b,
  author = {J. M. Spivey},
  title = {The {\large\it f\kern0.1em}{\normalsize\sc uzz} Manual},
  organization = {Computing Science Consultancy},
  address = {2 Willow Close, Garsington, Oxford OX9 9AN, UK},
  length = {68},
  edition = {2nd},
  year = {1992},
  price = {
    \pounds500 (\$1,000) for single user licence,
    \pounds500 (\$1,000) for academic site licence,
    \pounds1,500 (\$3,000) for commercial site licence,
    \pounds5 (\$10) for additional copies of the documentation.},
  other = {E-mail: \verb"<Mike.Spivey@comlab.ox.ac.uk>".},
  annote = {
    A Z type-checker and ``\verb"fuzz.sty"'' style option for
    \LaTeX\ documents \cite{Z:Lamp86}.  The package is compatible with
    the book, {\em The Z Notation: A Reference Manual} by the same
    author \cite{Z:Spiv92}.
    Technical enquiries can be sent to Mike Spivey at 2 Willow
    Close, Garsington, Oxford OX9 9AN, UK, or by e-mail at
    \verb"<Mike.Spivey@comlab.ox.ac.uk>".
    An order form is available via electronic mail by sending a message
    containing the command ``{\tt send z fuzz}'' to the PRG archive
    server \cite{Z:Zarc} on \verb"<archive-server@comlab.ox.ac.uk>".}
}

@manual{Z:ZTC,
  author = {Xiaoping Jia},
  title = {ZTC: A Type Checker for Z User's Guide},
  organization = {Institute for Software Engineering},
  address = {Department of Computer Science and Information Systems,
             DePaul University, Chicago, IL 60604, U.S.A.
             (E-mail: \verb"jia@cs.depaul.edu")},
  length = {54},
  year = {1994},
  price = {Free},
  other = {E-mail: \verb"jia@cs.depaul.edu".},
  annote = {ZTC is a type checker for the Z specification language. ZTC accepts
            two forms of input: \LaTeX with \verb"zed" style option and ZSL, an
            ASCII version of Z. ZTC can also perform translations between the two
            input forms. This document is intended to serve as both a user's 
            guide and a reference manual for ZTC.
            ZTC can be obtained via anonymous FTP at \verb"ise.cs.depaul.edu"
           (140.192.32.117): User name: \verb"ftp",  Password:  your e-mail 
           address, File: \verb"/ftp/dist/ZTC1.2.tar.Z".}
}

@book{Z:Spiv88b,
  author = {J. M. Spivey},
  title = {Understanding {Z}:
    A Specification Language and its Formal Semantics},
  publisher = {Cambridge University Press},
  series = {Cambridge Tracts in Theoretical Computer Science},
  volume = {3},
  length = {131},
  month = {January},
  year = {1988},
  isbn = {0-521-33429-2},
  annote = {Published version of 1985 DPhil thesis.}
}

@article{Z:Spiv89b,
  author = {J. M. Spivey},
  title = {An Introduction to {Z} and Formal Specifications},
  journal = {IEE/BCS Software Engineering Journal},
  volume = {4},
  number = {1},
  pages = {40-50},
  month = {January},
  year = {1989}
}

@book{Z:Spiv92,
  author = {J. M. Spivey},
  title = {The {Z} Notation: A Reference Manual},
  publisher = {Prentice Hall
    International Series in Computer Science},
  edition = {2nd},
  length = {150},
  year = {1992},
  note = {(1st edition, 1989)},
  isbn = {13-978529-9},
  price = {\pounds18.99 (\$32.00) paperback},
  annote = {
    This is the 2nd edition of the first widely available reference
    manual on Z originally published in 1989. The Reference Manual
    provides a complete and definitive guide to the use of Z in
    specifying information systems, writing specifications and
    designing implementations.
    See also the new draft Z standard \cite{Z:Brie92}.}
}

@misc{ProofPower-server,
  howpublished = {ProofPower server},
  note = {Send email to {ProofPower-server@win.icl.co.uk}},
  key = {ProofPower}
}

@article{ProofPower,
  author = {R. B. Jones},
  title = {{ICL ProofPower}},
  journal = {BCS FACS FACTS},
  series = {III},
  volume = 1,
  number = 1,
  pages = {10-13},
  month = {Winter},
  year = 1992,
  note = {Series III}
}

@book{Z:Dill90,
  author = {A. Diller},
  title = {{Z}: An Introduction to Formal Methods},
  publisher = {Wiley},
  location = {Chichester, UK},
  month = {June},
  year = {1990},
  length = {332},
  price = {\pounds19.95},
  isbn = {0-471-92489-X}
}

@book{Z:Pott90,
  author = {B. F. Potter and J. E. Sinclair and D. Till},
  title = {An Introduction to Formal Specification and {Z}},
  publisher = {Prentice Hall
    International Series in Computer Science},
  year = {1990},
  length = {300},
  price = {\pounds18.95 (\$33.95) paperback},
  isbn = {13-478702-1}
}

@techreport{Z:Brie92,
  author = {S. M. Brien and J. E. Nicholls},
  title = {{Z} Base Standard},
  institution = oucl,
  address = uk,
  type = {Technical Monograph},
  number = {PRG-107},
  ISBN = {0-902928-84-8},
  month = {November},
  year = {1992},
  note = {Accepted for ISO standardization, ISO/IEC JTC1/SC22.},
  annote = {
    The first publicly available version of the proposed BSI/ISO Z
    Standard, obtainable from the OUCL Librarian.  This has also been
    produced as a ZIP Project Report ZIP/PRG/92/121, SRC
    Document:  132, Version 1.0.  An electronic copy is available from
    the PRG archive server \cite{Z:Zarc}.  See also \cite{Z:Spiv92} for
    the current most widely available Z reference manual.}
}

@techreport{Balzac,
  author = {W. T. Harwood},
  title = {Proof Rules for {Balzac}},
  institution = {Imperial Software Technology},
  address = {Cambridge, UK},
  type = {Technical Report},
  number = {{WTH/P7/001}},
  year = {1991}
}

@techreport{Collinson,
  author = {Rodger Collinson},
  title = {A Simple Demonstration of {Balzac}},
  institution = {GCHQ},
  address = {Fiddlers Green Lane, Cheltenham, Gloucestershire},
  type = {Technical Report},
  year = {1992}
}

@techreport{Zpatt,
  author = {R. Macdonald and G. P. Randell and C. T. Sennett},
  title = {Pattern Matching in {ML}: A Case Study in Refinement},
  institution = {RSRE (now DRA)},
  address = {Defence Research Agency,
    St.~Andrews Road, Malvern,
    Worcs WR14 3PS, UK},
  type = {Report},
  number = {No.\ 89004},
  month = {May},
  year = {1989},
}

@techreport{EVES:Report,
  author = {M. Saaltink},
  title = {{Z} and {EVES}},
  institution = {Odyyssey Research Associates},
  address = {265 Carling Avenue, Suite 506, Ottawa,
    Ontario K1S 2E1, Canada},
  type = {Technical Report},
  number = {TR-91-5449-02},
  month = {October},
  year = {1991},
}

@inproceedings{EVES:Paper,
  author = {M. Saaltink},
  title = {{Z} and {Eves}},
  booktitle = {{Z} User Workshop, {York} 1991},
  editor = {J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {223-242},
  year = {1992}
}

@inproceedings{Z:Neil91,
  author = {D. Neilson},
  title = {Machine Support for {Z}: the {zedB} Tool},
  booktitle = {{Z} User Workshop, {Oxford} 1990},
  editor = {J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {105-128},
  year = {1991}
}

@inproceedings{Z:Neil92,
  author = {D. Neilson and D. Prasad},
  title = {{zedB}:  A Proof Tool for {Z} Built on {B}},
  booktitle = {{Z} User Workshop, {York} 1991},
  editor = {J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {243-258},
  year = {1992}
}

@techreport{paulson-fixedpt,
  author = {L. C. Paulson},
  title = {A Fixedpoint Approach to Implementing
    (Co-)Inductive Definitions},
  institution =  cucl,
  type = {Technical Report},
  note = {Draft},
  year = 1993
}

@book{StandardML,
 author = {R. Milner and M. Tofte and R. Harper},
 title = {The Definition of {Standard ML}},
 publisher = {The MIT Press},
 year = {1990}
}

@mastersthesis{Mah90,
author = {Savitri Maharaj},
title = {Implementing {Z} in {LEGO}},
school = {University of Edinburgh},
year = 1990
}

@inproceedings{Z:Bard92,
  author = {R. Barden and S. Stepney and D. Cooper},
  title = {The Use of {Z}},
  booktitle = {{Z} User Workshop, {York} 1991},
  editor = {J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {99-124},
  year = {1992}
}

@techreport{Z:Aust93,
  author = {S. Austin and G. I. Parkin},
  title = {Formal Methods: A Survey},
  institution = {National Physical Laboratory},
  address = {Queens Road, Teddington, Middlesex, TW11 0LW, UK},
  month = {March},
  year = {1993}
}

@inproceedings{Z:Smit92,
  author = {A. Smith},
  title = {On Recursive Free Types in {Z}},
  booktitle = {{Z} User Workshop, {York} 1991},
  editor = {J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {3-39},
  year = {1992}
}

@techreport{Smith,
  author = {A. Smith},
  title = {Proving Theorems in {Z}},
  institution = {Defence Research Agency},
  address = {St.~Andrews Road, Malvern,
    Worcs WR14 3PS, UK},
  type = {Report},
  number = {No.\ 92006},
  month = {March},
  year = {1992},
}

@inproceedings{Z:Wood92,
  author = {J. C. P. Woodcock and S. M. Brien},
  title = {{$\cal W$}:  A Logic for {Z}},
  booktitle = {{Z} User Workshop, {York} 1991},
  editor = {J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {77-96},
  year = {1992}
}

@inproceedings{Maharaj,
  author = {Savitri Maharaj},
  title = {Encoding {Z} Schemas in Type theory},
  booktitle = {Informal Proceedings of the
    1993 Workshop on Types for Proofs and Programs},
  editor = {H. Geuves},
  note = {Distributed electronically},
  pages = {209-218},
  year = {1993}
}


@book{HOL,
 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}
}

@inproceedings{Melham,
  author = {T. Melham},
  title = {Using Recursive Types to Reason about Hardware in
    {Higher Order Logic}},
  editor = {G. J. Milne},
  booktitle = {The Fusion of Hardware Design and Verification},
  series = {Proceedings of the IFIP WG10.2 Working Conference}, 
  publisher = {North-Holland}, 
  location = {Glasgow},
  month = {July},
  year = {1988},
  pages = {27-50}
}

@inproceedings{Embedding,
  title = {Experience with Embedding Hardware Description
    Languages in {HOL}},
  author = {R. J. Boulton and A. D. Gordon and J. R. Harrison and
    J. M. J. Herbert and J. {Van Tassel}},
  editor = {V. Stavridou and T. F. Melham and R. T. Boute},
  booktitle = {Theorem Provers in Circuit Design: Theory, Practice and
    Experience: Proceedings of the IFIP TC10/WG 10.2 International
    Conference}, 
  publisher = {North-Holland}, 
  series = {IFIP Transactions A-10},
  location = {Nijmegen}, 
  month = {June},
  year = {1992},
  pages = {129-156}
}

@inproceedings{Z:Mart93,
  author = {A. Martin},
  title = {Encoding {$\cal W$}: A Logic for {Z} in {2OBJ}},
  editor = {J. C. P. Woodcock and P. G. Larsen},
  booktitle = {FME'93: Industrial-Strength Formal Methods},
  location = {Odense, Denmark, 19--23 April 1993},
  publisher = {Springer-Verlag},
  series = lncs,
  volume = 670,
  pages = {462-481},
  year = 1993,
}

@manual{HOL-manual,
  key = {HOL},
  title = {The {HOL} System: Description, Tutorial, Libraries,
    Reference Manual},
  organization = {SRI International Cambridge Research Center
    and DSTO Australia},
  publisher = {Cambridge Computer Science Research Center,
    SRI International},
  note = {Revised version, four volumes},
  year = {1991}
}

@book{CamLCF,
  author = {L. C. Paulson},
  title = {Logic and Computation:
    Interactive Proof with {Cambridge LCF}},
  series = {Cambridge Tracts in Theoretical Computer Science},
  volume = 2,
  publisher = {Cambridge University Press},
  year = {1987}
}

@book{EdinLCF,
  author = {M. J. C. Gordon and  R. Milner and C. P. Wadsworth},
  title = {{Edinburgh LCF}: A Mechanised Logic of Computation},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {78},
  year = {1979}
}

@techreport{Jape,
  author = {B. A. Sufrin and R. Bornat},
  title = {The Gist of {Jape}},
  institution = oucl,
  address = uk,
  year = 1993,
  note = {Jape is available via anonymous FTP under the directory
    {\tt ftp.comlab.ox.ac.uk:pub/Packages/JAPE}.}
}

@inproceedings{Z:Bowe93,
  author = {J. P. Bowen},
  title = {{Comp.specification.z} and {Z FORUM}
    Frequently Asked Questions},
  booktitle = {{Z} User Workshop, {London} 1992},
  editor = {J. P. Bowen and J. E. Nicholls},
  publisher = {Springer-Verlag},
  series = {Workshops in Computing},
  pages = {342-347},
  year = {1993},
  annote = {
    This is a published version of the message that is maintained and
    sent out monthly on the \verb"comp.specification.z" {\sc usenet}
    newsgroup and ZFORUM electronic mailing list.}
}

@techreport{Z:Park91,
  author = {C. E. Parker},
  title = {{Z} Tools Catalogue},
  institution = {British Aerospace, Software Technology Dept.},
  address = {Warton PR4 1AX, UK},
  type = {ZIP project report},
  number = {ZIP/BAe/90/020},
  month = {May},
  year = {1991}
}