@phdthesis{Bailey1998,
author = "Anthony Bailey",
title = "The machine-checked literate formalisation of algebra in type theory",
school = "University of Manchester",
month = jan,
year = 1998,
available = { CB }
}
@phdthesis{Kammuller1999a,
author = "Florian Kamm{\"u}ller",
title = "Modular Reasoning in {Isabelle}",
school = "University of Cambridge, Computer Laboratory",
note = "Available as Technical Report No. 470.",
month = aug,
year = 1999,
available = { CB }
}
% TYPES 98
@inproceedings{Kammuller1999b,
author = "Florian Kamm{\"u}ller",
title = "Modular Structures as Dependent Types in {Isabelle}",
pages = "121--132",
crossref = "AltenkirchEtAl1999",
available = { CB }
}
@proceedings{AltenkirchEtAl1999,
editor = "Thorsten Altenkirch and Wolfgang Naraschewski and Bernhard Reus",
title = "Types for Proofs and Programs: International Workshop, {TYPES} '98, {Kloster Irsee, Germany, March 27--31, 1998}, Selected Papers",
booktitle = "TYPES '98",
publisher = "Springer",
series = "LNCS 1657",
year = 1999
}
% CADE-17
@inproceedings{Kammuller2000,
author = "Florian Kamm{\"u}ller",
title = "Modular Reasoning in {Isabelle}",
pages = "99--114",
crossref = "McAllester2000",
available = { CB }
}
@proceedings{McAllester2000,
editor = "David McAllester",
title = "17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17--20, 2000: Proceedings",
booktitle = "CADE 17",
publisher = "Springer",
series = "LNCS 1831",
year = 2000
}
@book{NipkowEtAl2002,
author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
title = "{Isabelle/HOL}: A Proof Assistant for Higher-Order Logic",
publisher = "Springer",
series = "LNCS 2283",
year = 2002,
available = { CB }
}
% TYPES 2002
@inproceedings{Nipkow2003,
author = "Tobias Nipkow",
title = "Structured Proofs in {Isar/HOL}",
pages = "259--278",
crossref = "GeuversWiedijk2003"
}
@proceedings{GeuversWiedijk2003,
editor = "H. Geuvers and F. Wiedijk",
title = "Types for Proofs and Programs (TYPES 2002)",
booktitle = "TYPES 2002",
publisher = "Springer",
series = "LNCS 2646",
year = 2003
}
@phdthesis{Wenzel2002a,
author = "Markus Wenzel",
title = "{Isabelle/Isar} --- a versatile environment for human-readable formal proof documents",
school = "Technische Universit{\"a}t M{\"u}nchen",
note = "Electronically published as http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html.",
year = 2002
}
@unpublished{Wenzel2002b,
author = "Markus Wenzel",
title = "Using locales in {Isabelle/Isar}",
note = "Part of the Isabelle2003 distribution, file src/HOL/ex/Locales.thy. Distribution of Isabelle available at http://isabelle.in.tum.de",
year = 2002
}
@unpublished{Wenzel2003,
author = "Markus Wenzel",
title = "The {Isabelle/Isar} Reference Manual",
note = "Part of the Isabelle2003 distribution, available at http://isabelle.in.tum.de",
year = 2003
}
% TPHOLs 2003
@inproceedings{Chrzaszcz2003,
author = "Jacek Chrz{\c{a}}szcz",
title = "Implementing Modules in the {Coq} System",
pages = "270--286",
crossref = "BasinWolff2003",
available = { CB }
}
@proceedings{BasinWolff2003,
editor = "David Basin and Burkhart Wolff",
title = "Theorem proving in higher order logics: 16th International Conference, TPHOLs 2003, Rome, Italy, September 2003: proceedings",
booktitle = "TPHOLs 2003",
publisher = "Springer",
series = "LNCS 2758",
year = 2003
}
@PhdThesis{Klein2003,
author = "Gerwin Klein",
title = "Verified Java Bytecode Verification",
school = "Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen",
year = 2003
}
% TACAS 2000
@inproceedings{Aspinall2000,
author = "David Aspinall",
title = "Proof General: A Generic Tool for Proof Development",
pages = "38--42",
crossref = "GrafSchwartzbach2000"
}
@proceedings{GrafSchwartzbach2000,
editor = {Susanne Graf and Michael I. Schwartzbach},
title = {Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000, Berlin, Germany, March 25 -- April 2, 2000, Proceedings},
booktitle = "TACAS 2000",
publisher = {Springer},
series = {LNCS 1785},
year = {2000},
}
% TYPES 2004
@inproceedings{Ballarin2004a,
author = "Clemens Ballarin",
title = "Locales and Locale Expressions in {Isabelle/Isar}",
pages = "34--50",
crossref = "BerardiEtAl2004"
}
@inproceedings{Chrzaszcz2004,
author = "Jacek Chrz{\c{a}}szcz",
title = "Modules in {Coq} Are and Will Be Correct",
pages = "130--136",
crossref = "BerardiEtAl2004",
available = { CB }
}
@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
}