Quelle root.bib Sprache: Latech

@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-isar-ref,
  author = {Markus Wenzel},
  title  = {The {Isabelle/Isar} Reference Manual},
  institution = TUM}

@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}

quality96%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.