doc-src/IsarAdvanced/Classes/classes.bib
author obua
Mon, 09 Jul 2007 17:36:25 +0200
changeset 23663 84b5c89b8b49
parent 20946 75b56e51fade
permissions -rw-r--r--
new version of computing oracle
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20946
75b56e51fade initial draft
haftmann
parents:
diff changeset
     1
75b56e51fade initial draft
haftmann
parents:
diff changeset
     2
@InProceedings{Ballarin:2004,
75b56e51fade initial draft
haftmann
parents:
diff changeset
     3
  author = 	 {Clemens Ballarin},
75b56e51fade initial draft
haftmann
parents:
diff changeset
     4
  title = 	 {Locales and Locale Expressions in {Isabelle/Isar}},
75b56e51fade initial draft
haftmann
parents:
diff changeset
     5
  booktitle =	 {Types for Proofs and Programs (TYPES 2003)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
     6
  year =	 2004,
75b56e51fade initial draft
haftmann
parents:
diff changeset
     7
  editor =	 {Stefano Berardi and others},
75b56e51fade initial draft
haftmann
parents:
diff changeset
     8
  series =	 {LNCS 3085}
75b56e51fade initial draft
haftmann
parents:
diff changeset
     9
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    10
75b56e51fade initial draft
haftmann
parents:
diff changeset
    11
@InProceedings{Ballarin:2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    12
  author = 	 {Clemens Ballarin},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    13
  title = 	 {Interpretation of Locales in {Isabelle}: Theories and Proof Contexts},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    14
  booktitle =	 {Mathematical Knowledge Management (MKM 2006)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    15
  year =	 2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    16
  editor =	 {J.M. Borwein and W.M. Farmer},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    17
  series =	 {LNAI 4108}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    18
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    19
75b56e51fade initial draft
haftmann
parents:
diff changeset
    20
@InProceedings{Berghofer-Nipkow:2000,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    21
  author =       {Stefan Berghofer and Tobias Nipkow},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    22
  title =        {Proof terms for simply typed higher order logic},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    23
  booktitle     = {Theorem Proving in Higher Order Logics ({TPHOLs} 2000)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    24
  editor        = {J. Harrison and M. Aagaard},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    25
  series        = {LNCS 1869},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    26
  year          = 2000
75b56e51fade initial draft
haftmann
parents:
diff changeset
    27
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    28
75b56e51fade initial draft
haftmann
parents:
diff changeset
    29
@Manual{Coq-Manual:2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    30
  title =        {The {Coq} Proof Assistant Reference Manual, version 8},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    31
  author =       {B. Barras and others},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    32
  organization = {INRIA},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    33
  year =         2006
75b56e51fade initial draft
haftmann
parents:
diff changeset
    34
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    35
75b56e51fade initial draft
haftmann
parents:
diff changeset
    36
@Article{Courant:2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    37
  author = 	 {Judica{\"e}l Courant},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    38
  title = 	 {{$\mathcal{MC}_2$: A Module Calculus for Pure Type Systems}},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    39
  journal = 	 {The Journal of Functional Programming},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    40
  year = 	 2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    41
  note =	 {To appear},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    42
  abstract = {Several proof-assistants rely on the very formal basis
75b56e51fade initial draft
haftmann
parents:
diff changeset
    43
    of Pure Type Systems (PTS) as their foundations.  We are concerned
75b56e51fade initial draft
haftmann
parents:
diff changeset
    44
    with the issues involved in the development of large proofs in
75b56e51fade initial draft
haftmann
parents:
diff changeset
    45
    these provers such as namespace management, development of
75b56e51fade initial draft
haftmann
parents:
diff changeset
    46
    reusable proof libraries and separate verification. Although
75b56e51fade initial draft
haftmann
parents:
diff changeset
    47
    implementations offer many features to address them, few
75b56e51fade initial draft
haftmann
parents:
diff changeset
    48
    theoretical foundations have been laid for them up to now. This is
75b56e51fade initial draft
haftmann
parents:
diff changeset
    49
    a problem as features dealing with modularity may have harmful,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    50
    unsuspected effects on the reliability or usability of an
75b56e51fade initial draft
haftmann
parents:
diff changeset
    51
    implementation.
75b56e51fade initial draft
haftmann
parents:
diff changeset
    52
    
75b56e51fade initial draft
haftmann
parents:
diff changeset
    53
    In this paper, we propose an extension of Pure Type Systems with a
75b56e51fade initial draft
haftmann
parents:
diff changeset
    54
    module system, MC2, adapted from SML-like module systems for
75b56e51fade initial draft
haftmann
parents:
diff changeset
    55
    programming languages.  This system gives a theoretical framework
75b56e51fade initial draft
haftmann
parents:
diff changeset
    56
    addressing the issues mentioned above in a quite uniform way.  It
75b56e51fade initial draft
haftmann
parents:
diff changeset
    57
    is intended to be a theoretical foundation for the module systems
75b56e51fade initial draft
haftmann
parents:
diff changeset
    58
    of proof-assistants such as Coq or Agda.  We show how reliability
75b56e51fade initial draft
haftmann
parents:
diff changeset
    59
    and usability can be formalized as metatheoretical properties and
75b56e51fade initial draft
haftmann
parents:
diff changeset
    60
    prove they hold for MC2.}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    61
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    62
75b56e51fade initial draft
haftmann
parents:
diff changeset
    63
@PhdThesis{Jacek:2004,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    64
  author = 	 {Jacek Chrz\c{a}szcz},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    65
  title = 	 {Modules in type theory with generative definitions},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    66
  school = 	 {Universit{\'e} Paris-Sud},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    67
  year = 	 {2004},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    68
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    69
75b56e51fade initial draft
haftmann
parents:
diff changeset
    70
@InProceedings{Kamm-et-al:1999,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    71
  author =       {Florian Kamm{\"u}ller and Markus Wenzel and
75b56e51fade initial draft
haftmann
parents:
diff changeset
    72
                  Lawrence C. Paulson},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    73
  title =        {Locales: A Sectioning Concept for {Isabelle}},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    74
  booktitle     = {Theorem Proving in Higher Order Logics ({TPHOLs} '99)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    75
  editor        = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
75b56e51fade initial draft
haftmann
parents:
diff changeset
    76
                  Paulin, C. and Thery, L.},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    77
  series        = {LNCS 1690},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    78
  year          = 1999
75b56e51fade initial draft
haftmann
parents:
diff changeset
    79
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    80
75b56e51fade initial draft
haftmann
parents:
diff changeset
    81
@InProceedings{Nipkow-Prehofer:1993,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    82
  author =       {T. Nipkow and C. Prehofer},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    83
  title =        {Type checking type classes},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    84
  booktitle =    {ACM Symp.\ Principles of Programming Languages},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    85
  year =         1993
75b56e51fade initial draft
haftmann
parents:
diff changeset
    86
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    87
75b56e51fade initial draft
haftmann
parents:
diff changeset
    88
@Book{Nipkow-et-al:2002:tutorial,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    89
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    90
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    91
  series	= {LNCS 2283},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    92
  year		= 2002
75b56e51fade initial draft
haftmann
parents:
diff changeset
    93
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
    94
75b56e51fade initial draft
haftmann
parents:
diff changeset
    95
@InCollection{Nipkow:1993,
75b56e51fade initial draft
haftmann
parents:
diff changeset
    96
  author =       {T. Nipkow},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    97
  title =        {Order-Sorted Polymorphism in {Isabelle}},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    98
  booktitle =    {Logical Environments},
75b56e51fade initial draft
haftmann
parents:
diff changeset
    99
  publisher =    {Cambridge University Press},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   100
  year =         1993,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   101
  editor =       {G. Huet and G. Plotkin}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   102
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   103
75b56e51fade initial draft
haftmann
parents:
diff changeset
   104
@InProceedings{Nipkow:2002,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   105
  author = 	 {Tobias Nipkow},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   106
  title = 	 {Structured Proofs in {Isar/HOL}},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   107
  booktitle = 	 {Types for Proofs and Programs (TYPES 2002)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   108
  year =	 2003,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   109
  editor =	 {H. Geuvers and F. Wiedijk},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   110
  series =	 {LNCS 2646}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   111
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   112
75b56e51fade initial draft
haftmann
parents:
diff changeset
   113
@InCollection{Paulson:1990,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   114
  author =       {L. C. Paulson},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   115
  title =        {Isabelle: the next 700 theorem provers},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   116
  booktitle =    {Logic and Computer Science},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   117
  publisher =    {Academic Press},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   118
  year =         1990,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   119
  editor =       {P. Odifreddi}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   120
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   121
75b56e51fade initial draft
haftmann
parents:
diff changeset
   122
@BOOK{Pierce:TypeSystems,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   123
  AUTHOR = {B.C. Pierce},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   124
  TITLE = {Types and Programming Languages},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   125
  PUBLISHER = {MIT Press},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   126
  YEAR = 2002,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   127
  PLCLUB = {Yes},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   128
  BCP = {Yes},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   129
  KEYS = {books},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   130
  HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/tapl},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   131
  ERRATA = {http://www.cis.upenn.edu/~bcpierce/tapl/errata.txt}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   132
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   133
75b56e51fade initial draft
haftmann
parents:
diff changeset
   134
@Book{Schmidt-Schauss:1989,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   135
  author	= {Manfred Schmidt-Schau{\ss}},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   136
  title		= {Computational Aspects of an Order-Sorted Logic with Term Declarations},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   137
  series	= {LNAI 395},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   138
  year		= 1989
75b56e51fade initial draft
haftmann
parents:
diff changeset
   139
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   140
75b56e51fade initial draft
haftmann
parents:
diff changeset
   141
@InProceedings{Wenzel:1997,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   142
  author =       {M. Wenzel},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   143
  title =        {Type Classes and Overloading in Higher-Order Logic},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   144
  booktitle =    {Theorem Proving in Higher Order Logics ({TPHOLs} '97)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   145
  editor =       {Elsa L. Gunter and Amy Felty},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   146
  series =       {LNCS 1275},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   147
  year =         1997}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   148
75b56e51fade initial draft
haftmann
parents:
diff changeset
   149
@article{hall96type,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   150
  author = "Cordelia Hall and Kevin Hammond and Peyton Jones, S. and Philip Wadler",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   151
  title = "Type Classes in {Haskell}",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   152
  journal = "ACM Transactions on Programming Languages and Systems",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   153
  volume = "18",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   154
  number = "2",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   155
  publisher = "ACM Press",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   156
  year = "1996"
75b56e51fade initial draft
haftmann
parents:
diff changeset
   157
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   158
75b56e51fade initial draft
haftmann
parents:
diff changeset
   159
@inproceedings{hindleymilner,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   160
  author = {L. Damas and H. Milner},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   161
  title = {Principal type schemes for functional programs},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   162
  booktitle = {ACM Symp. Principles of Programming Languages},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   163
  year = 1982
75b56e51fade initial draft
haftmann
parents:
diff changeset
   164
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   165
75b56e51fade initial draft
haftmann
parents:
diff changeset
   166
@manual{isabelle-axclass,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   167
  author	= {Markus Wenzel},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   168
  title		= {Using Axiomatic Type Classes in {I}sabelle},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   169
  institution	= {TU Munich},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   170
  year          = 2005,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   171
  note          = {\url{http://isabelle.in.tum.de/doc/axclass.pdf}}}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   172
75b56e51fade initial draft
haftmann
parents:
diff changeset
   173
@InProceedings{krauss:2006:functions,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   174
  author = 	 {A. Krauss},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   175
  title = 	 {Partial Recursive Functions in Higher-Order Logic},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   176
  booktitle = 	 {Int. Joint Conference on Automated Reasoning (IJCAR 2006)},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   177
  year =	 2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   178
  editor =	 {Ulrich Furbach and Natarajan Shankar},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   179
  series =	 {LNCS}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   180
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   181
75b56e51fade initial draft
haftmann
parents:
diff changeset
   182
@inproceedings{peterson93implementing,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   183
  author = "J. Peterson and Peyton Jones, S.",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   184
  title = "Implementing Type Classes",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   185
  booktitle = "{SIGPLAN} Conference on Programming Language Design and Implementation",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   186
  year = 1993
75b56e51fade initial draft
haftmann
parents:
diff changeset
   187
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   188
75b56e51fade initial draft
haftmann
parents:
diff changeset
   189
@inproceedings{wadler89how,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   190
  author = {P. Wadler and S. Blott},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   191
  title = {How to make ad-hoc polymorphism less ad-hoc},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   192
  booktitle = {ACM Symp.\ Principles of Programming Languages},
75b56e51fade initial draft
haftmann
parents:
diff changeset
   193
  year = 1989
75b56e51fade initial draft
haftmann
parents:
diff changeset
   194
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   195
75b56e51fade initial draft
haftmann
parents:
diff changeset
   196
@misc{jones97type,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   197
  author = "S. Jones and M. Jones and E. Meijer",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   198
  title = "Type classes: an exploration of the design space",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   199
  text = "Simon Peyton Jones, Mark Jones, and Erik Meijer. Type classes: an exploration
75b56e51fade initial draft
haftmann
parents:
diff changeset
   200
    of the design space. In Haskell Workshop, June 1997.",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   201
  year = "1997",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   202
  url = "citeseer.ist.psu.edu/peytonjones97type.html"
75b56e51fade initial draft
haftmann
parents:
diff changeset
   203
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   204
75b56e51fade initial draft
haftmann
parents:
diff changeset
   205
@article{haftmann_wenzel2006classes,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   206
  author = "Florian Haftmann and Makarius Wenzel",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   207
  title =  "Constructive Type Classes in Isabelle",
75b56e51fade initial draft
haftmann
parents:
diff changeset
   208
  year =   2006,
75b56e51fade initial draft
haftmann
parents:
diff changeset
   209
  note =   {To appear}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   210
}
75b56e51fade initial draft
haftmann
parents:
diff changeset
   211