Quellcode-Bibliothek root.bib Sprache: Latech

@unpublished{IsarRef,
  author = "Markus Wenzel",
  title = "The {Isabelle/Isar} Reference Manual",
  note = "Part of the Isabelle distribution, \url{https://isabelle.in.tum.de/doc/isar-ref.pdf}."
}

@book {Jacobson1985,
  author = "Nathan Jacobson",
  title = "Basic Algebra",
  volume = "I",
  publisher = "Freeman",
  edition = "2nd",
  year = 1985,
  available = { CB }
}

% TYPES 2006

@inproceedings{HaftmannWenzel2007,
  author = "Florian Haftmann and Makarius Wenzel",
  title = "Constructive Type Classes in {Isabelle}",
  pages = "160--174",
  crossref = "AltenkirchMcBride2007",
  available = { CB }
}

@proceedings{AltenkirchMcBride2007,
  editor = "Thorsten Altenkirch and Connor McBride",
  title = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
  booktitle = "Types for Proofs and Programs, TYPES 2006, Nottingham, UK",
  publisher = "Springer",
  series = "LNCS 4502",
  year = 2007
}

@techreport{Ballarin2006a,
  author = "Clemens Ballarin",
  title = "Interpretation of Locales in {Isabelle}: Managing Dependencies between Locales",
  institution = "Technische Universit{\"a}t M{\"u}nchen",
  number = "TUM-I0607",
  year = 2006
}

% TYPES 2003

@inproceedings{Ballarin2004a,
  author = "Clemens Ballarin",
  title = "Locales and Locale Expressions in {Isabelle/Isar}",
  pages = "34--50",
  crossref = "BerardiEtAl2004"
}

@proceedings{BerardiEtAl2004,
  editor = "Stefano Berardi and Mario Coppo and Ferruccio Damiani",
  title = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
  booktitle = "Types for Proofs and Programs, TYPES 2003, Torino, Italy",
  publisher = "Springer",
  series = "LNCS 3085",
  year = 2004
}

% TYPES 2008

@inproceedings{HaftmannWenzel2009,
  author = "Florian Haftmann and Makarius Wenzel",
  title = "Local theory specifications in {Isabelle}/{Isar}",
  pages = "153--168",
  crossref = "BerardiEtAl2009"
}

@proceedings{BerardiEtAl2009,
  editor = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
  title = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
  booktitle = "Types for Proofs and Programs, TYPES 2008, Torino, Italy",
  series = "LNCS 5497",
  publisher = "Springer",
  year = 2009
}

% MKM 2006

@inproceedings{Ballarin2006b,
  author = "Clemens Ballarin",
  title = "Interpretation of Locales in {Isabelle}: Theories and Proof Contexts",
  pages = "31--43",
  crossref = "BorweinFarmer2006"
}

@proceedings{BorweinFarmer2006,
  editor = "Jonathan M. Borwein and William M. Farmer",
  title = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
  booktitle = "Mathematical knowledge management, MKM 2006, Wokingham, UK",
  series = "LNCS 4108",
  publisher = "Springer",
  year = 2006,
  available = { CB }
}

% TPHOLs 1999

@inproceedings{KammullerEtAl1999,
  author = "Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson",
  title = "Locales: A Sectioning Concept for {Isabelle}",
  pages = "149--165",
  crossref = "BertotEtAl1999",
  available = { CB }
}

@book{BertotEtAl1999,
  editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
  title = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
  booktitle = "Theorem Proving in Higher Order Logics: TPHOLs'99, Nice, France",
  publisher = "Springer",
  series = "LNCS 1690",
  year = 1999
}

quality100%

¤ 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.0.13Bemerkung: (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.