--- a/doc-src/IsarAdvanced/Classes/classes.bib Tue Jul 24 15:20:53 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,211 +0,0 @@
-
-@InProceedings{Ballarin:2004,
- author = {Clemens Ballarin},
- title = {Locales and Locale Expressions in {Isabelle/Isar}},
- booktitle = {Types for Proofs and Programs (TYPES 2003)},
- year = 2004,
- editor = {Stefano Berardi and others},
- series = {LNCS 3085}
-}
-
-@InProceedings{Ballarin:2006,
- author = {Clemens Ballarin},
- title = {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts},
- booktitle = {Mathematical Knowledge Management (MKM 2006)},
- year = 2006,
- editor = {J.M. Borwein and W.M. Farmer},
- series = {LNAI 4108}
-}
-
-@InProceedings{Berghofer-Nipkow:2000,
- author = {Stefan Berghofer and Tobias Nipkow},
- title = {Proof terms for simply typed higher order logic},
- booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} 2000)},
- editor = {J. Harrison and M. Aagaard},
- series = {LNCS 1869},
- year = 2000
-}
-
-@Manual{Coq-Manual:2006,
- title = {The {Coq} Proof Assistant Reference Manual, version 8},
- author = {B. Barras and others},
- organization = {INRIA},
- year = 2006
-}
-
-@Article{Courant:2006,
- author = {Judica{\"e}l Courant},
- title = {{$\mathcal{MC}_2$: A Module Calculus for Pure Type Systems}},
- journal = {The Journal of Functional Programming},
- year = 2006,
- note = {To appear},
- abstract = {Several proof-assistants rely on the very formal basis
- of Pure Type Systems (PTS) as their foundations. We are concerned
- with the issues involved in the development of large proofs in
- these provers such as namespace management, development of
- reusable proof libraries and separate verification. Although
- implementations offer many features to address them, few
- theoretical foundations have been laid for them up to now. This is
- a problem as features dealing with modularity may have harmful,
- unsuspected effects on the reliability or usability of an
- implementation.
-
- In this paper, we propose an extension of Pure Type Systems with a
- module system, MC2, adapted from SML-like module systems for
- programming languages. This system gives a theoretical framework
- addressing the issues mentioned above in a quite uniform way. It
- is intended to be a theoretical foundation for the module systems
- of proof-assistants such as Coq or Agda. We show how reliability
- and usability can be formalized as metatheoretical properties and
- prove they hold for MC2.}
-}
-
-@PhdThesis{Jacek:2004,
- author = {Jacek Chrz\c{a}szcz},
- title = {Modules in type theory with generative definitions},
- school = {Universit{\'e} Paris-Sud},
- year = {2004},
-}
-
-@InProceedings{Kamm-et-al:1999,
- author = {Florian Kamm{\"u}ller and Markus Wenzel and
- Lawrence C. Paulson},
- title = {Locales: A Sectioning Concept for {Isabelle}},
- 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
-}
-
-@InProceedings{Nipkow-Prehofer:1993,
- author = {T. Nipkow and C. Prehofer},
- title = {Type checking type classes},
- booktitle = {ACM Symp.\ Principles of Programming Languages},
- year = 1993
-}
-
-@Book{Nipkow-et-al:2002:tutorial,
- author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
- title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
- series = {LNCS 2283},
- year = 2002
-}
-
-@InCollection{Nipkow:1993,
- author = {T. Nipkow},
- title = {Order-Sorted Polymorphism in {Isabelle}},
- booktitle = {Logical Environments},
- publisher = {Cambridge University Press},
- year = 1993,
- editor = {G. Huet and G. Plotkin}
-}
-
-@InProceedings{Nipkow:2002,
- author = {Tobias Nipkow},
- title = {Structured Proofs in {Isar/HOL}},
- booktitle = {Types for Proofs and Programs (TYPES 2002)},
- year = 2003,
- editor = {H. Geuvers and F. Wiedijk},
- series = {LNCS 2646}
-}
-
-@InCollection{Paulson:1990,
- author = {L. C. Paulson},
- title = {Isabelle: the next 700 theorem provers},
- booktitle = {Logic and Computer Science},
- publisher = {Academic Press},
- year = 1990,
- editor = {P. Odifreddi}
-}
-
-@BOOK{Pierce:TypeSystems,
- AUTHOR = {B.C. Pierce},
- TITLE = {Types and Programming Languages},
- PUBLISHER = {MIT Press},
- YEAR = 2002,
- PLCLUB = {Yes},
- BCP = {Yes},
- KEYS = {books},
- HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl},
- ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
-}
-
-@Book{Schmidt-Schauss:1989,
- author = {Manfred Schmidt-Schau{\ss}},
- title = {Computational Aspects of an Order-Sorted Logic with Term Declarations},
- series = {LNAI 395},
- year = 1989
-}
-
-@InProceedings{Wenzel:1997,
- author = {M. Wenzel},
- title = {Type Classes and Overloading in Higher-Order Logic},
- booktitle = {Theorem Proving in Higher Order Logics ({TPHOLs} '97)},
- editor = {Elsa L. Gunter and Amy Felty},
- series = {LNCS 1275},
- year = 1997}
-
-@article{hall96type,
- author = "Cordelia Hall and Kevin Hammond and Peyton Jones, S. and Philip Wadler",
- title = "Type Classes in {Haskell}",
- journal = "ACM Transactions on Programming Languages and Systems",
- volume = "18",
- number = "2",
- publisher = "ACM Press",
- year = "1996"
-}
-
-@inproceedings{hindleymilner,
- author = {L. Damas and H. Milner},
- title = {Principal type schemes for functional programs},
- booktitle = {ACM Symp. Principles of Programming Languages},
- year = 1982
-}
-
-@manual{isabelle-axclass,
- author = {Markus Wenzel},
- title = {Using Axiomatic Type Classes in {I}sabelle},
- institution = {TU Munich},
- year = 2005,
- note = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
-
-@InProceedings{krauss:2006:functions,
- author = {A. Krauss},
- title = {Partial Recursive Functions in Higher-Order Logic},
- booktitle = {Int. Joint Conference on Automated Reasoning (IJCAR 2006)},
- year = 2006,
- editor = {Ulrich Furbach and Natarajan Shankar},
- series = {LNCS}
-}
-
-@inproceedings{peterson93implementing,
- author = "J. Peterson and Peyton Jones, S.",
- title = "Implementing Type Classes",
- booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
- year = 1993
-}
-
-@inproceedings{wadler89how,
- author = {P. Wadler and S. Blott},
- title = {How to make ad-hoc polymorphism less ad-hoc},
- booktitle = {ACM Symp.\ Principles of Programming Languages},
- year = 1989
-}
-
-@misc{jones97type,
- author = "S. Jones and M. Jones and E. Meijer",
- title = "Type classes: an exploration of the design space",
- text = "Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration
- of the design space. In Haskell Workshop, June 1997.",
- year = "1997",
- url = "citeseer.ist.psu.edu/peytonjones97type.html"
-}
-
-@article{haftmann_wenzel2006classes,
- author = "Florian Haftmann and Makarius Wenzel",
- title = "Constructive Type Classes in Isabelle",
- year = 2006,
- note = {To appear}
-}
-