doc-src/IsarAdvanced/Classes/classes.bib

mk_atomize: careful matching against rules admits overloading;

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