@book{Birkhoff79,
author = {Garret Birkhoff},
title = {Lattice Theory},
publisher = {American Mathematical Society},
year=1979
}
@Book{davenport92,
author = {H. Davenport},
title = {The Higher Arithmetic},
publisher = {Cambridge University Press},
year = 1992
}
@book{GKP_CM,
author = {Graham, Ronald L. and Knuth, Donald E. and Patashnik, Oren},
title = {Concrete Mathematics: A Foundation for Computer Science},
year = {1994},
isbn = {0201558025},
edition = {2nd},
publisher = {Addison--Wesley},
address = {Boston, MA, USA},
}
@techreport{Gordon-TR68,
author = "Mike Gordon",
title = "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic",
institution = "University of Cambridge, Computer Laboratory",
number = 68,
year = 1985
}
@book{card-book,
title = {Introduction to {C}ardinal {A}rithmetic},
author = {M. Holz and K. Steffens and E. Weitz},
publisher = "Birkh{\"{a}}user",
year = 1999,
}
@book{Nipkow-et-al:2002:tutorial,
author = {T. Nipkow and L. C. Paulson and M. Wenzel},
title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
series = {LNCS},
volume = 2283,
year = 2002,
publisher = {Springer-Verlag}
}
@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}}