@string{CUCL="Comp. Lab., Univ. Camb."}
@string{CUP="Cambridge University Press"}
@string{Springer="Springer-Verlag"}
@string{TUM="TU Munich"}
@article{church40, author = "Alonzo Church", title = "A Formulation of the Simple Theory of Types", journal = "Journal of Symbolic Logic", year = 1940, volume = 5, pages = "56-68"}
@Book{Concrete-Math, author = {R. L. Graham and D. E. Knuth and O. Patashnik}, title = {Concrete Mathematics}, publisher = {Addison-Wesley}, year = 1989
}
@InProceedings{Naraschewski-Wenzel:1998:HOOL, author = {Wolfgang Naraschewski and Markus Wenzel}, title = {Object-Oriented Verification based on Record Subtyping in
{H}igher-{O}rder {L}ogic},
crossref = {tphols98}}
@Article{Nipkow:1998:Winskel, author = {Tobias Nipkow}, title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook}, journal = {Formal Aspects of Computing}, year = 1998, volume = 10, pages = {171--186}
}
@InProceedings{Wenzel:1999:TPHOL, author = {Markus Wenzel}, title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
crossref = {tphols99}}
@Book{Winskel:1993, author = {G. Winskel}, title = {The Formal Semantics of Programming Languages}, publisher = {MIT Press}, year = 1993
}
@Book{davey-priestley, author = {B. A. Davey and H. A. Priestley}, title = {Introduction to Lattices and Order}, publisher = CUP, year = 1990}
@TechReport{Gordon:1985:HOL, author = {M. J. C. Gordon}, title = {{HOL}: A machine oriented formulation of higher order logic},
institution = {University of Cambridge Computer Laboratory}, year = 1985, number = 68
}
@manual{isabelle-HOL, author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, title = {{Isabelle}'s Logics: {HOL}},
institution = {Institut f\"ur Informatik, Technische Universi\"at
M\"unchen and Computer Laboratory, University of Cambridge}}
@manual{isabelle-intro, author = {Lawrence C. Paulson}, title = {Introduction to {Isabelle}},
institution = CUCL}
@manual{isabelle-ref, author = {Lawrence C. Paulson}, title = {The {Isabelle} Reference Manual},
institution = CUCL}
@Book{paulson-isa-book, author = {Lawrence C. Paulson}, title = {Isabelle: A Generic Theorem Prover}, publisher = {Springer}, year = 1994,
note = {LNCS 828}}
@TechReport{paulson-mutilated-board, author = {Lawrence C. Paulson}, title = {A Simple Formalization and Proof for the Mutilated Chess Board},
institution = CUCL, year = 1996, number = 394,
note = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Reports/mutil.pdf}}
}
@Proceedings{tphols98, title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98}, editor = {Jim Grundy and Malcom Newey},
series = {LNCS}, volume = 1479, year = 1998}
@Proceedings{tphols99, title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
Paulin, C. and Thery, L.},
series = {LNCS 1690}, year = 1999}
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
