author | immler |
Sun, 27 Oct 2019 21:51:14 -0400 | |
changeset 71035 | 6fe5a0e1fa8e |
parent 67298 | fee3ed06a281 |
permissions | -rw-r--r-- |
67298 | 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 |
||
58623 | 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 |
||
58638
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
42 |
@book{mendelson, |
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
43 |
Author = {E. Mendelson}, |
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
44 |
Edition = {Fourth}, |
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
45 |
Publisher = {Chapman \& Hall}, |
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
46 |
Title = {Introduction to Mathematical Logic}, |
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
47 |
Year = {1997}} |
5855b9b3d6a3
proper @{cite} with bibtex entry (unchecked comment);
wenzelm
parents:
58623
diff
changeset
|
48 |