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