1@string{CUCL="Computer Laboratory, University of Cambridge"} 2@string{CUP="Cambridge University Press"} 3 4@TechReport{camilleri92, 5 author = {J. Camilleri and T. F. Melham}, 6 title = {Reasoning with Inductively Defined Relations in the 7 {HOL} Theorem Prover}, 8 institution = CUCL, 9 year = 1992, 10 number = 265, 11 month = Aug} 12 13@InProceedings{paulin-tlca, 14 author = {Christine Paulin-Mohring}, 15 title = {Inductive Definitions in the System {Coq}: Rules and 16 Properties}, 17 crossref = {tlca93}, 18 pages = {328-345}} 19 20@Proceedings{tlca93, 21 title = {Typed Lambda Calculi and Applications}, 22 booktitle = {Typed Lambda Calculi and Applications}, 23 editor = {M. Bezem and J.F. Groote}, 24 year = 1993, 25 publisher = {Springer}, 26 series = {LNCS 664}} 27 28@InCollection{szasz93, 29 author = {Nora Szasz}, 30 title = {A Machine Checked Proof that {Ackermann's} Function is not 31 Primitive Recursive}, 32 crossref = {huet-plotkin93}, 33 pages = {317-338}} 34 35@book{huet-plotkin93, 36 editor = {{G{\'e}rard} Huet and Gordon Plotkin}, 37 title = {Logical Environments}, 38 booktitle = {Logical Environments}, 39 publisher = CUP, 40 year = 1993} 41 42@book{mendelson, 43 Author = {E. Mendelson}, 44 Edition = {Fourth}, 45 Publisher = {Chapman \& Hall}, 46 Title = {Introduction to Mathematical Logic}, 47 Year = {1997}} 48 49