| author | wenzelm |
| Thu, 13 Mar 2025 11:19:27 +0100 | |
| changeset 82266 | cca7113dcafc |
| parent 77812 | fb3d81bd9803 |
| permissions | -rw-r--r-- |
|
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
1 |
@book{Birkhoff79,
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
2 |
author = {Garret Birkhoff},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
3 |
title = {Lattice Theory},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
4 |
publisher = {American Mathematical Society},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
5 |
year=1979 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
6 |
} |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
7 |
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
8 |
@Book{davenport92,
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
9 |
author = {H. Davenport},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
10 |
title = {The Higher Arithmetic},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
11 |
publisher = {Cambridge University Press},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
12 |
year = 1992 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
13 |
} |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
14 |
|
| 67299 | 15 |
@book{GKP_CM,
|
16 |
author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren},
|
|
17 |
title = {Concrete Mathematics: A Foundation for Computer Science},
|
|
18 |
year = {1994},
|
|
19 |
isbn = {0201558025},
|
|
20 |
edition = {2nd},
|
|
21 |
publisher = {Addison--Wesley},
|
|
22 |
address = {Boston, MA, USA},
|
|
23 |
} |
|
24 |
||
|
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
25 |
@techreport{Gordon-TR68,
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
26 |
author = "Mike Gordon", |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
27 |
title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
28 |
institution = "University of Cambridge, Computer Laboratory", |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
29 |
number = 68, |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
30 |
year = 1985 |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
31 |
} |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
32 |
|
| 58623 | 33 |
@book{card-book,
|
34 |
title = {Introduction to {C}ardinal {A}rithmetic},
|
|
35 |
author = {M. Holz and K. Steffens and E. Weitz},
|
|
36 |
publisher = "Birkh{\"{a}}user",
|
|
37 |
year = 1999, |
|
38 |
} |
|
39 |
||
|
66893
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
40 |
@book{Nipkow-et-al:2002:tutorial,
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
41 |
author = {T. Nipkow and L. C. Paulson and M. Wenzel},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
42 |
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
43 |
series = {LNCS},
|
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
44 |
volume = 2283, |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
45 |
year = 2002, |
|
ced164fe3bbd
derived axiom iffI as a lemma (thanks to Alexander Maletzky)
nipkow
parents:
58623
diff
changeset
|
46 |
publisher = {Springer-Verlag}
|
| 58623 | 47 |
} |
48 |
||
49 |
@InProceedings{paulin-tlca,
|
|
50 |
author = {Christine Paulin-Mohring},
|
|
51 |
title = {Inductive Definitions in the System {Coq}: Rules and
|
|
52 |
Properties}, |
|
53 |
crossref = {tlca93},
|
|
54 |
pages = {328-345}}
|
|
55 |
||
56 |
@Proceedings{tlca93,
|
|
57 |
title = {Typed Lambda Calculi and Applications},
|
|
58 |
booktitle = {Typed Lambda Calculi and Applications},
|
|
59 |
editor = {M. Bezem and J.F. Groote},
|
|
60 |
year = 1993, |
|
61 |
publisher = {Springer},
|
|
62 |
series = {LNCS 664}}
|
|
| 77812 | 63 |
|
64 |
@article{leijen01,
|
|
65 |
author = {Leijen, Daan},
|
|
66 |
title = {Division and Modulus for Computer Scientists},
|
|
67 |
year = 2001, |
|
68 |
url = {https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/divmodnote-letter.pdf}}
|