@string{CUCL="Computer Laboratory, University of Cambridge"}
@string{CUP="Cambridge University Press"}
@TechReport{camilleri92,
author = {J. Camilleri and T. F. Melham},
title = {Reasoning with Inductively Defined Relations in the
{HOL} Theorem Prover},
institution = CUCL,
year = 1992,
number = 265,
month = Aug}
@InProceedings{paulin-tlca,
author = {Christine Paulin-Mohring},
title = {Inductive Definitions in the System {Coq}: Rules and
Properties},
crossref = {tlca93},
pages = {328-345}}
@Proceedings{tlca93,
title = {Typed Lambda Calculi and Applications},
booktitle = {Typed Lambda Calculi and Applications},
editor = {M. Bezem and J.F. Groote},
year = 1993,
publisher = {Springer},
series = {LNCS 664}}
@InCollection{szasz93,
author = {Nora Szasz},
title = {A Machine Checked Proof that {Ackermann's} Function is not
Primitive Recursive},
crossref = {huet-plotkin93},
pages = {317-338}}
@book{huet-plotkin93,
editor = {{G{\'e}rard} Huet and Gordon Plotkin},
title = {Logical Environments},
booktitle = {Logical Environments},
publisher = CUP,
year = 1993}
@book{mendelson,
Author = {E. Mendelson},
Edition = {Fourth},
Publisher = {Chapman \& Hall},
Title = {Introduction to Mathematical Logic},
Year = {1997}}