path: root/docs/opt-coercion/fc-normalization-rta.bib

@string{proc = "Proceedings of the\ "}

@string{cmu-cs = "Carnegie Mellon University, School of Computer Science"}
@string{cornell-cs = "Department of Computer Science, Cornell University"}
@string{dec-src = "Digital Equipment Corporation, Systems Research Center"}
@string{edin-cs = "Department of Computer Science, University of Edinburgh"}
@string{inria = "Institut National de Recherche en Informatique et Automatique (INRIA)"}
@string{yale-cs = "Yale University, Department of Computer Science"}


%% Conferences
@string{cade = "International Conference on Automated Deduction"}
@string{csl = "International Workshop on Computer Science Logic"}
@string{esop = "European Symposium on Programming"}
@string{fool = "Foundations of Object-Oriented Languages Workshop"}
@string{fpca = "Conference on Functional Programming Languages and Computer Architecture"}
@string{icalp = "International Colloquium on Automata, Languages, and Programming"}
@string{icfp = "{ACM SIGPLAN} International Conference on Functional Programming"}
@string{lfp = "{ACM} Conference on {Lisp} and Functional Programming"}
@string{lics = "{IEEE} Symposium on Logic in Computer Science"}
@string{mfps = "Mathematical Foundations of Programming Semantics"}
@string{osdi = "Symposium on Operating Systems Design and Implementation"}
@string{pldi = "{ACM SIGPLAN} Conference on Programming Language Design and Implementation"}
@string{popl = "{ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages"}
@string{sosp = "{ACM} Symposium on Operating Systems Principles"}
@string{tacs = "Theoretical Aspects of Computer Software"}
@string{tlca = "International Conference on Typed Lambda Calculi and Applications"}
@string{tldi = "{ACM SIGPLAN} Workshop in Types in Language Design and Implementation"}
@string{sigmod = "Proc. {ACM} {SIGMOD} International
                  Conference on Management of Data"}
@string{oopsla = "{ACM} {SIGPLAN} Conference on Object-Oriented
                  Programming, Systems, Languages and Applications"}
@string{sigcomm = "Proc. {SIGCOMM} Symposium on Communications
                  Architectures and Protocols"}
@string{ieeesp = "IEEE Symposium on Research in Security and Privacy"}
@string{rtss = "Real-Time Systems Symposium"}

%% Workshops
@string{tic = "{ACM} {SIGPLAN} Workshop on Types in Compilation"}
@string{wcsss = "{ACM} {SIGPLAN} Workshop on Compiler Support for System Software"}
@string{hotos = "Workshop on Hot Topis in Operating Systems"}
@string{lctes = "Proceedings of the {ACM} {SIGPLAN} Workshop on Languages, 
                 Compilers, and Tools for Embedded Systems"}
@string{pepm = "{ACM} {SIGPLAN} Workshop on Partial Evaluation and
                  Semantics-Based Program Manipulation"}
@string{hoots = "International Workshop on Higher Order Operational Techniques in Semantics"}

%% Journals
@string{iandc = "Information and Computation"}
@string{jacm = "Journal of the {ACM}"}
@string{jfp = "Journal of Functional Programming"}
@string{mscs = "Mathematical Structures in Computer Science"}
@string{tcs = "Theoretical Computer Science"}
@string{toplas = "{ACM} Transactions on Programming Languages and Systems"}
@string{tse = "{IEEE} Transactions on Software Engineering"}
@String{j-LISP-SYMB-COMPUT      = "Lisp and Symbolic Computation"}
@string{hosc = "Higher-Order and Symbolic Computation"}


@string{lncs = "Lecture Notes in Computer Science"}

@string{academic = "Academic Press"}
@string{addison = "Addison-Wesley"}
@string{cambridge-press = "Cambridge University Press"}
@string{chapman = "Chapman \& Hall"}
@string{elsevier = "Elsevier"}
@string{mit-press = "The MIT Press"}
@string{noholland = "North-Holland"}
@string{springer = "Springer-Verlag"}
@string{sigplan-notices = "{SIGPLAN} Notices"}
@string{cam-ma = "Cambridge, Massachusetts"}
@string{ith-ny = "Ithaca, New York"}
@string{pgh-pa = "Pittsburgh, Pennsylvania"}

@string{o1="First "}
@string{o2="Second "}
@string{o3="Third "}
@string{o4="Fourth "}
@string{o5="Fifth "}
@string{o6="Sixth "}
@string{o7="Seventh "}
@string{o8="Eighth "}
@string{o9="Ninth "}
@string{o10="Tenth "}
@string{o11="Eleventh "}
@string{o12="Twelfth "}
@string{o13="Thirteenth "}
@string{o14="Fourteenth "}
@string{o15="Fifteenth "}
@string{o16="Sixteenth "}
@string{o17="Seventeenth "}
@string{o18="Eighteenth "}
@string{o19="Nineteenth "}
@string{o20="Twentieth "}
@string{o21="Twenty-First "}
@string{o22="Twenty-Second "}
@string{o23="Twenty-Third "}
@string{o24="Twenty-Fourth "}
@string{o25="Twenty-Fifth "}
@string{o26="Twenty-Sixth "}
@string{o27="Twenty-Seventh "}
@string{o28="Twenty-Eighth "}
@string{o29="Twenty-Ninth "}
@string{o30="Thirtieth "}


%% Ack for downloaded bib entry

@String{ack-nhfb = "Nelson H. F. Beebe,
                    Center for Scientific Computing,
                    University of Utah,
                    Department of Mathematics, 322 INSCC,
                    155 S 1400 E RM 233,
                    Salt Lake City, UT 84112-0090, USA,
                    Tel: +1 801 581 5254,
                    FAX: +1 801 585 1640, +1 801 581 4148,
                    e-mail: \path|beebe@math.utah.edu|,
                            \path|beebe@acm.org|,
                            \path|beebe@ieee.org| (Internet),
                    URL: \path|http://www.math.utah.edu/~beebe/|"}






@inproceedings{deferred-type-errors,
 author = "Dimitrios Vytiniotis and Simon {Peyton Jones} and Pedro Magalhaes",
 title = "Equality proofs and deferred type errors",
 booktitle =  {Proceedings of {ACM SIGPLAN} International Conference on Functional Programming (ICFP '12)},
 pages = "341-352",
 year = 2012
}

@inproceedings{ductilej,
  author = "Michael Bayne and Richard Cook and Michael Ernst",
  title = "Always-available static and dynamic feedback",
  booktitle = "Proceedings of 33rd International Conference on Software Engineering (ICSE'11)",
  year = 2011,
  pages = "521-530",
  address = "Hawaii"
}

@INCOLLECTION{pottier:pierce-chapter,
  AUTHOR = {Fran\c{c}ois Pottier and Didier R{\'{e}}my},
  TITLE = {The Essence of {ML} Type Inference},
  BOOKTITLE = {Advanced Topics in Types and Programming Languages},
  PAGES = {389--489},
  PUBLISHER = {MIT Press},
  YEAR = {2005},
  EDITOR = {Benjamin C. Pierce},
  CHAPTER = {10},
  html = {http://cristal.inria.fr/attapl/}
}
  
@article{gill-hutton:worker-wrapper,
  author = "Andy Gill and Graham Hutton",
  title = "The worker/wrapper transformation",
  journal = {Journal of Functional Programming},
  volume = {19},
  issue = {2},
  page = {227-251},
  year = 2009
}
  
@article{pjv:modular,
  author = {Dimitrios Vytiniotis and Simon {Peyton Jones} and Tom Schrijvers and Martin Sulzmann},
  title = "OutsideIn(X): modular type inference with local assumptions",
  journal = {Journal of Functional Programming},
  volume = {21},
  issue = {4-5},
  page = {333-412},
  year = 2011
}


  
@article{rossberg08,
  author    = {Andreas Rossberg},
  title     = {Dynamic Translucency with Abstraction Kinds and Higher-Order
               Coercions},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {218},
  year      = {2008},
  pages     = {313-336},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@InProceedings{mcbride:levitation,
  author = 	 {James Chapman and Pierre-\'{E}variste Dagand and Conor McBride and Peter Morris},
  title = 	 {The Gentle Art of Levitation},
  booktitle = {Proceedings of the Fifteenth {ACM SIGPLAN} International Conference on Functional Programming (ICFP '10)},
  year = 	 2010,
  address = 	 {Baltimore, MD, USA},
  month = 	 {September},
  note = 	 {To appear.}}

#  doi = {http://dx.doi.org/10.1016/0890-5401(91)90066-B},
@article{deBruijn:telescopes,
 author = {de Bruijn, N. G.},
 title = {Telescopic mappings in typed lambda calculus},
 journal = {Inf. Comput.},
 volume = {91},
 number = {2},
 year = {1991},
 issn = {0890-5401},
 pages = {189--204},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }



@inproceedings{johann:gadt,
  author    = {Patricia Johann and
               Neil Ghani},
  title     = {Foundations for structured programming with GADTs},
  booktitle = {POPL},
  year      = {2008},
  pages     = {297-308},
  ee        = {http://doi.acm.org/10.1145/1328438.1328475},
  crossref  = {DBLP:conf/popl/2008},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2008,
  editor    = {George C. Necula and
               Philip Wadler},
  title     = {Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on
               Principles of Programming Languages, POPL 2008, San Francisco,
               California, USA, January 7-12, 2008},
  booktitle = {POPL},
  publisher = {ACM},
  year      = {2008},
  isbn      = {978-1-59593-689-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{xi:grdt,
  author    = {Hongwei Xi and
               Chiyan Chen and
               Gang Chen},
  title     = {Guarded recursive datatype constructors},
  booktitle = {POPL},
  year      = {2003},
  pages     = {224-235},
  ee        = {http://doi.acm.org/10.1145/640128.604150},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{crary:syntactic-recursive,
  author    = {Karl Crary and
               Robert Harper},
  title     = {Syntactic Logical Relations for Polymorphic and Recursive
               Types},
  journal   = {Electr. Notes Theor. Comput. Sci.},
  volume    = {172},
  year      = {2007},
  pages     = {259-299},
  note      = {Computation, Meaning, and Logic: Articles dedicated to Gordon Plotkin},
  ee        = {http://dx.doi.org/10.1016/j.entcs.2007.02.010},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{ahmed:step-indexed,
  author    = {Amal J. Ahmed},
  title     = {Step-Indexed Syntactic Logical Relations for Recursive and
               Quantified Types},
  booktitle = {ESOP},
  year      = {2006},
  pages     = {69-83},
  ee        = {http://dx.doi.org/10.1007/11693024_6},
  crossref  = {DBLP:conf/esop/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Book{kleene:mathematical-logic,
  author =	 {Stephen Cole Kleene},
  title = 	 {Mathematical Logic},
  publisher = 	 {Wiley},
  year = 	 1967
}

@inproceedings{Swamy:2009:TTC:1596550.1596598,
 author = {Swamy, Nikhil and Hicks, Michael and Bierman, Gavin M.},
 title = {A theory of typed coercions and its applications},
 booktitle = {Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
 series = {ICFP '09},
 year = {2009},
 isbn = {978-1-60558-332-7},
 location = {Edinburgh, Scotland},
 pages = {329--340},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {coercion insertion, gradual typing, nonambiguity, provenance, type-directed translation},
} 



@incollection{Remy-Yakobowski:xmlf,
  author = {R\'{e}my, Didier and Yakobowski, Boris},
  affiliation = {INRIA Paris - Rocquencourt},
  title = {A {Church}-Style Intermediate Language for {MLF}},
  booktitle = {Functional and Logic Programming},
  series = {Lecture Notes in Computer Science},
  editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, German},
  publisher = {Springer Berlin / Heidelberg},
  pages = {24-39},
  volume = {6009},
  also = {http://gallium.inria.fr/~remy/mlf/},
  abstract = {MLF is a type system that seamlessly merges ML-style implicit but
  second-class polymorphism with System-F explicit first-class
  polymorphism. We present xMLF, a Church-style version of MLF with full type
  information that can easily be maintained during reduction. All parameters
  of functions are explicitly typed and both type abstraction and type
  instantiation are explicit. However, type instantiation in xMLF is more
  general than type application in System F. We equip xMLF with a small-step
  reduction semantics that allows reduction in any context and show that this
  relation is confluent and type preserving. We also show that both subject
  reduction and progress hold for weak-reduction strategies, including
  call-by-value with the value-restriction.},
  year = {2010}
}

@InProceedings{Remy-Yakobowski:mlf-type-inference,
AUTHOR = {Didier Remy and Boris Yakobowski},
TITLE  = {{E}fficient {T}ype {I}nference for the {MLF} Language:
          a graphical and constraints-based approach},
BOOKTITLE = {The 13th ACM SIGPLAN 
             International Conference on Functional Programming (ICFP'08)}, 
YEAR = 2008,
ADDRESS = {Victoria, BC, Canada},
MONTH = Sep,
ALSO  =  {http://gallium.inria.fr/~remy/mlf/},
PDF =    {http://gallium.inria.fr/~remy/mlf/Remy-Yakobowski@icfp08:mlf-type-inference.pdf},
pages = {63--74},
doi = {http://doi.acm.org/10.1145/1411203.1411216},
ABSTRACT = {
MLF is a type system that seamlessly merges ML-style type inference with
System-F polymorphism. We propose a system of graphic (type) constraints
that can be used to perform type inference in both ML or MLF. We show
that this constraint system is a small extension of the formalism of
graphic types, originally introduced to represent MLF types. We give a
few semantic preserving transformations on constraints and propose a
strategy for applying them to solve constraints. We show that the
resulting algorithm has optimal complexity for MLF type inference, and
argue that, as for ML, this complexity is linear under reasonable
assumptions.
}
}




@inproceedings{xi:cut-elimination,
author = "Chiyan Chen and Dengping Zhu and Hongwei Xi",
title = {{Implementing Cut Elimination: A Case Study of Simulating Dependent Types in Haskell}},
booktitle = "Proceedings of the 6th International Symposium on Practical Aspects of Declarative Languages",
publisher = "Springer-Verlag LNCS vol. 3057",
year = "2004",
month = "June",
pages = "239--254",
address = "Dallas, TX",
abstract = {{
Gentzen's Hauptsatz -- cut elimination theorem -- in sequent calculi
reveals a fundamental property on logic connectives in various logics such
as classical logic and intuitionistic logic.  In this paper, we implement a
procedure in Haskell to perform cut elimination for intuitionistic sequent
calculus, where we use types to guarantee that the procedure can only
return a cut-free proof of the same sequent when given a proof of a sequent
that may contain cuts.  The contribution of the paper is two-fold.  On
the one hand, we present an interesting (and somewhat unexpected) application
of the current type system of Haskell, illustrating through a concrete
example how some typical use of dependent types can be simulated in
Haskell. On the other hand, we identify several problematic issues with
such a simulation technique and then suggest some approaches to addressing
these issues in Haskell.
}}
}



@inproceedings{HList-HW04,
 author = {Oleg Kiselyov and Ralf L\"{a}mmel and Keean Schupke},
 title = "{Strongly typed heterogeneous collections}",
 booktitle = "{Haskell '04: Proceedings of the ACM SIGPLAN workshop on Haskell}",
 year = {2004},
 isbn = {1-58113-850-4},
 pages = {96--107},
 location = {Snowbird, Utah, USA},
 doi = {http://doi.acm.org/10.1145/1017472.1017488},
 publisher = {ACM Press},
}


@Unpublished{augustsson:silly,
  author = 		  {Lennart Augustsson and Kent Petersson},
  title = 		  {Silly Type Families},
  note = 		  {Available from \url{http://www.cs.pdx.edu/~sheard/papers/silly.pdf}},
  month =		  sep,
  year =			  1994,
  annote =       {GADTs}
}

@inproceedings{sheard:omega,
  title = "Meta-programming with built-in type equality",
  author = "Tim Sheard and Emir Pasalic",
  booktitle = "Proc 4th International Workshop on Logical Frameworks and Meta-languages (LFM'04), Cork",
  month = jul,
  year = 2004,
  pages = "106--124",
  keywords = "phantom types, type indexed data types"
}



@TechReport{cheney-hinze:phantom-types,
  author = 	 {James Cheney and Ralf Hinze},
  title = 	 {First-Class Phantom Types},
  institution =  {Cornell University},
  year = 	 2003,
  type =	 {CUCIS},
  number =	 {TR2003-1901}
}


@InCollection{Remy!records,
author     = "Didier R\'{e}my",
title      = "Type Inference for Records in a Natural Extension of {ML}",
booktitle  = "Theoretical Aspects Of Object-Oriented Programming. 
              Types, Semantics and Language Design",
publisher  = "MIT Press",
year       = 1993,
editor     = "Carl A. Gunter and John C. Mitchell"
}


%% A %%

@article{abadi+:dynamic,
  author =	 "Mart\'{\i}n Abadi and Luca Cardelli and Benjamin
                  Pierce and Gordon Plotkin",
  title =	 "Dynamic typing in a statically-typed language",
  journal =	 toplas,
  year =	 1991,
  volume =	 13,
  number =	 2,
  month =	 "April",
  pages =	 "237--268",
}

@article{         Abadi92,
author =          "Mart\'{\i}n Abadi and Luca Cardelli and Benjamin Pierce
                  and Didier R\'{e}my",
title =           "Dynamic Typing in Polymorphic Languages",
journal =         "Journal of Functional Programming",
volume =          "5",
number =          "1",
pages =           "111--130",
month =           jan,
annnote =         "Summary in \bgroup \em ACM SIGPLAN Workshop on ML and its
                  Applications\egroup, June 1992",
year =            1995,
bcp =             yes
}



@article{abadi+:explicit-subs,
  author =	 "Mart\'{\i}n Abadi and Luca Cardelli and Pierre-Louis
                  Curien and Jean-Jacques L\'{e}vy",
  title =	 "Explicit Substitutions",
  journal =	 jfp,
  year =	 1991,
  volume =	 1,
  number =	 4,
  pages =	 "375--416",
}

@inproceedings{abadi+:object-interp,
  author =	 "Mart\'{\i}n Abadi and Luca Cardelli and Ramesh
                  Viswanathan",
  title =	 "An Interpretation of Objects and Object Types",
  booktitle =	 o23 # " " # popl,
  year =	 1996,
  month =	 jan,
  address =	 "St.\ Petersburg, Florida",
  pages =	 "296--409",
}

@inproceedings{abadi+:prim-objects,
  author =	 "Mart\'{\i}n Abadi and Luca Cardelli",
  title =	 "A Theory of Primitive Objects: Untyped and
                  First-Order Systems",
  booktitle =	 tacs,
  year =	 1994,
  month =	 apr,
  pages =	 "296--320",
  series =	 lncs,
  volume =	 789,
  publisher =	 springer,
}

@book{abadi+:thy-objects,
  author =	 "Mart\'{\i}n Abadi and Luca Cardelli",
  title =	 "A Theory of Objects",
  publisher =	 springer,
  year =	 1996,
}

@inproceedings{abadi:protection-in-trans,
  author =	 "Mart\'{\i}n Abadi",
  title =	 "Protection in Programming-Language Translations",
  booktitle =	 o25 # " " # icalp,
  month =	 jul,
  year =	 1998,
}

@InProceedings{abadi+:dcc,
  author = 	 {Mart\'{\i}n Abadi and Anindya Banerjee and Nevin Heintze and Jon G. Riecke},
  title = 	 {A Core Calculus of Dependency},
  booktitle = 	 o26 # " " # popl,
  pages =	 {147--160},
  year =	 1999,
  address =	 {San Antonio, Texas},
  month =	 jan
}


@inproceedings{aczel:frege-revisit,
  author =	 "Peter Aczel",
  title =	 "{F}rege Structures Revisited",
  booktitle =	 "Proceedings of the 1983 Marstrand Workshop",
  editor =	 "B. {Nordstr\"{o}m} and J. Smith",
  year =	 1983,
}


@manual{ada:manual, 
  key = {ISOA},
  edition = {6.0}, 
  month = dec, 
  organization = {International Organisation for Standardisation and 
                  International Electrotechnical Commission}, 
  title = {International Standard ISO/IEC 8652:1995 Ada Reference Manual: 
           Language and Standard Libraries }, 
  year = 1994,
  url =  "http://www.adahome.com/rm95/"
} 

@Manual{c:standard,
  title = 		  {ISO/IEC 9899:1999 Programming Languages--{C}},
  key =			  {ISOC},
  organization = {International Organisation for Standardization
                  and International Electrotechnical Commission},
  month =		  dec,
  year =			  1999
}

@Manual{c++:standard,
  title =		  {ISO/IEC 14882:1998 Information Technology--Programming Languages--{C++}},
  key =			  {ISOCP},
  organization = {International Organisation for Standardization
                  and International Electrotechnical Commission},
  month =		  sep,
  year =			  1998
}



@inproceedings{aditya+:gc,
  author =	 "Shail Aditya and Christine Flood and James Hicks",
  title =	 "Garbage Collection for Strongly-Typed Languages
                  using Run-Time Type Reconstruction",
  booktitle =	 1994 # " " # lfp,
  month =	 jun,
  pages =	 "12--23",
  year =	 1994,
  address =	 "Orlando"
}

@inproceedings{ agesen97adding,
    author = "Ole Agesen and Stephen N. Freund and John C. Mitchell",
    title = "Adding Type Parameterization to the {Java} Language",
    booktitle = "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming: {S}ystems, {L}anguages, and {A}pplications ({OOPSLA})",
    address = "Atlanta, GA",
    pages = "49--65",
    year = "1997",
    url = "citeseer.nj.nec.com/agesen97adding.html" }


@inproceedings{aiken+:type-inclusion,
  author =	 "Alexander Aiken and Edward L. Wimmers",
  title =	 "Type Inclusion Constraints and Type Inference",
  booktitle =	 "FPCA93: " # fpca,
  year =	 1993,
  pages =	 "31--41",
}

@inproceedings{allen+:reflection,
  author =	 "Stuart F. Allen and Robert L. Constable and Douglas
                  J. Howe and William E. Aitken",
  title =	 "The Semantics of Reflected Proof",
  booktitle =	 o5 # " " # lics,
  year =	 1990,
  month =	 jun,
  pages = {95--105},
  address = {Philadelphia, Pennsylvania},
  publisher = {IEEE Computer Society Press}
}

@phdthesis{allen:phd,
  author =	 "Stuart Allen",
  title =	 "A Non-Type-Theoretic Semantics for Type-Theoretic
                  Language",
  school =	 cornell-cs,
  year =	 1987,
  address =	 ith-ny,
}

@inproceedings{allen:tt-semant,
  author =	 "Stuart Allen",
  title =	 "A Non-Type-Theoretic Definition of
                  {Martin-L\"{o}f}'s Types",
  booktitle =	 o2 # " " # lics,
  year =	 1987,
  month =	 jun,
  pages =	 "215--221",
  address =	 ith-ny,
}

@article{amadio+:subtyping-rectypes,
  author =	 "Roberto Amadio and Luca Cardelli",
  title =	 "Subtyping Recursive Types",
  journal =	 toplas,
  year =	 1993,
  volume =	 15,
  number =	 4,
  pages =	 "575--631",
}

@inproceedings{appel+:cont-close,
  author =	 "Andrew W. Appel and Trevor Jim",
  title =	 "Continuation-Passing, Closure-Passing Style",
  bookTitle =	 o16 # " " # popl,
  year =	 1989,
  month =	 jan,
  pages =	 "293--302",
  address =	 "Austin",
}

@inproceedings{appel+:smlnj,
  title =	 "{S}tandard {ML} of {N}ew {J}ersey",
  author =	 "Andrew W. Appel and David B. MacQueen",
  booktitle =	 "Third International Symposium on Programming
                  Language Implementation and Logic Programming",
  publisher =	 springer,
  month =	 aug,
  year =	 "1991",
  pages =	 "1--13",
  volume =	 528,
  series =	 lncs,
}

@book{appel:cont-compiling,
  author =	 "Andrew W. Appel",
  title =	 "Compiling with Continuations",
  publisher =	 cambridge-press,
  year =	 1992,
}


@inproceedings{appel+:pcc,
 author = {Andrew W. Appel and Amy P. Felty},
 title = {A Semantic Model of Types and Machine Instructions for Proof-Carrying Code},
 booktitle = o27 # " " # popl, 
 month = jan,
 year = 2000,
 address = "Boston",
 pages = "243--253"
}

@inproceedings{ armstrong97development,
    author = "Joe Armstrong",
    title = "The development of {Erlang}",
    booktitle = "Proceedings of the {ACM} {SIGPLAN} International
                  Conference on Functional Programming ({ICFP} '97)",
    pages = "196--203",
    year = "1997",
    url = "citeseer.nj.nec.com/37831.html" }

@inproceedings{aspinall:subtype-singleton,
  author =	 "David Aspinall",
  title =	 "Subtyping with Singleton Types",
  booktitle =	 o8 # " " # csl,
  year =	 1994,
  month =	 sep,
  address =	 "Kazimierz, Poland",
  series =	 lncs,
  volume =	 933,
  publisher =	 springer,
  pages =	 "1--15",
}


@inproceedings{audebaud:partial-coq,
  title =	 "Partial Objects in the Calculus of Constructions",
  author =	 "Philippe Audebaud",
  booktitle =	 o6 # " " # lics,
  year =	 1991,
  month =	 jul,
  pages =	 "86--95",
  address =	 "Amsterdam",
}

@InProceedings{augustsson:cayenne,
  author       = {Lennart Augustsson},
  title        = {Cayenne--a language with dependent types},
  booktitle    = o3 # " " # icfp,
  pages        = {239--250},
  year         = 1998,
  month        = sep,
}

%% B %%

@Article{barendregt:impact,
  author = 	 {Henk P. Barendregt},
  title = 	 { The impact of the lambda calculus },
  journal = 	 {Bulletin of Symbolic Logic},
  year = 	 1997,
  volume =	 3,
  number =	 2
}





@InCollection{barendregt:pts,
  author =	 {Henk P. Barendregt },
  editor =	 {Samson Abramsky and Dov M. Gabbay and Thomas S. E. Maibaum},
  booktitle = 	 {Handbook of Logic in Computer Science},
  title = 	 {Lambda Calculi with Types},
  publisher = 	 {Clarendon Press},
  year = 	 1992,
  volume =	 2,
  pages = {117--309},
  address =	 {Oxford}
}

@Book{barendregt:book,
  author =	 {Hendrik P. Barendregt},
  title = 	 {The Lambda Calculus, its Syntax and Semantics},
  publisher = 	 {North Holland},
  year = 	 1984,
  edition =	 {Second}
}

@inproceedings{basin:automated-partial-fns,
  author =	 "David A. Basin",
  title =	 "An Environment for Automated Reasoning about Partial
                  Functions",
  booktitle =	 o9 # " " # cade,
  series =	 lncs,
  volume =	 310,
  publisher =	 springer,
  year =	 1988,
}

@article{bates+:proofs-as-programs,
  author =	 "Joseph L. Bates and Robert L. Constable",
  title =	 "Proofs as Programs",
  journal =	 toplas,
  year =	 1985,
  volume =	 7,
  number =	 1,
  pages =	 "113--136",
  month =	 jan,
}

@phdthesis{bates:phd,
  author =	 "Joseph L. Bates",
  title =	 "A Logic for Correct Program Development",
  year =	 1979,
  school =	 cornell-cs,
  address =	 ith-ny,
}

@article{beeson:recursive-models,
  author =	 "Michael Beeson",
  title =	 "Recursive Models for Constructive Set Theories",
  journal =	 "Annals of Mathematical Logic",
  volume =	 23,
  pages =	 "127--178",
  year =	 1982,
}


@InProceedings{berger91nbe,
  author = 	 {Ulrich Berger and Helmut Schwichtenberg},
  title = 	 {An inverse of the evaluation functional for typed $lambda$-calculus},
  booktitle = 	 { Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science},
  pages =	 {203--211},
  year =	 {1991 },
  editor =	 { R. Vemuri},
  address =	 {Los Alamitos},
  publisher =	 {IEEE Computer Society Press}
}

@inproceedings{benton+:sml-to-jvm,
  author =	 "Nick Benton and Andrew Kennedy and George Russell",
  title =	 "Compiling {Standard} {ML} to {Java} Bytecodes",
  booktitle =	 1998 # " " # icfp,
  year =	 1998,
  month =	 sep,
  address =	 "Baltimore",
  pages =	 "129--140",
}

@inproceedings{bershad+:spin,
  title =	 "Extensibility, Safety and Performance in the {SPIN}
                  Operating System",
  author =	 "Brain Bershad and Stefan Savage and Przemyslaw
                  Pardyak and Emin Sirer and Marc Fiuczynski and David
                  Becker and Craig Chambers and Susan Eggers",
  booktitle =	 o15 # " " # sosp,
  year =	 1995,
  month =	 dec,
  pages =	 "267--284",
  address =	 "{C}opper {M}ountain",
}




@Article{bird+:debruijn,
  author = 	 {Richard S. Bird and Ross Paterson},
  title = 	 {De {B}ruijn Notation as a Nested Datatype},
  journal = 	 jfp,
  year = 	 1999,
  volume =	 9,
  number = 1,
  pages = "77--91",
}

@InProceedings{bird+:nested,
  author = 	 {Richard Bird and Lambert Meertens},
  title = 	 {Nested Datatypes},
  booktitle = "Proceedings 4th Int.\ Conf.\ on 
    Mathematics of Program Construction, {MPC}'98,  
    Marstrand, Sweden, 15--17 June 1998",
  year =	 1998,
  volume =	 1422,
  series =	 lncs,
  pages = "52--67"
}

@article{ bird99generalised,
    author = "Richard Bird and Ross Paterson",
    title = "Generalised Folds for Nested Datatypes",
    journal = "Formal Aspects of Computing",
    volume = "11",
    number = "2",
    pages = "200--222",
    year = "1999",
    editor = "Johan Juering",
    url = "citeseer.nj.nec.com/bird99generalised.html"
}



@techreport{birkedal+:kit,
  title =	 "The {ML} {K}it (Version 1)",
  author =	 "Lars Birkedal and Nick Rothwell and Mads Tofte and
                  David N. Turner",
  year =	 "1993",
  institution =	 "{D}epartment of {C}omputer {S}cience, {U}niversity
                  of {C}openhagen",
  number =	 "93/14"
}

@inproceedings{birkedal+:rec-type-interp, 
  author    = "Lars Birkedal and Robert Harper", 
  title     = "Relational Interpretations of Recursive
               Types in an Operational Setting",
  pages = "458-490",
  booktitle = tacs, 
  year = 1997 
}

@inproceedings{birkedal+:regions,
  title =	 "From Region Inference to {v}on {N}eumann Machines
                  via Region Representation Inference",
  author =	 "Lars Birkedal and Mads Tofte and Magnus Vejlstrup",
  booktitle =	 o23 # " " # popl,
  year =	 "1996",
  month =	 jan,
  pages =	 "171--183",
  address =	 "St.\ Petersburg, Florida"
}

@phdthesis{blume:phd,
  author =	 "Matthias Blume",
  title =	 "Hierarchical Modularity and Intermodule
                  Optimization",
  month =	 nov,
  year =	 1997,
  school =	 "Princeton University, Department of Computer
                  Science",
  address =	 "Princeton, New Jersey",
}

@article{boehm+:gc,
  author =	 "Hans-J. Boehm and Mark Weiser",
  title =	 "Garbage Collection in an uncooperative environment",
  journal =	 "Software Practice and Experience",
  volume =	 18,
  number =	 9,
  year =	 1988,
  month =	 sep,
  pages =	 "807--820",
}

@inproceedings{boehm:infer-undecidable,
  author =	 "Hans-J. Boehm",
  title =	 "Partial Polymorphic Type Inference is Undecidable",
  booktitle =	 o26 # " Annual Symposium on Foundations of Computer
                  Science",
  year =	 1985,
  month =	 oct,
  pages =	 "339--345",
}



@Article{bohm+:algebras,
  author = 	 {Corrado B\"ohm and Allessandro Berarducci},
  title = 	 {Automatic synthesis of typed {$\Lambda$}-programs on 
                   term algebras},
  journal = 	 tcs,
  year = 	 1985,
  volume =	 39,
  pages =	 {135-154}
}

@inproceedings{ bracha98making,
    author = "Gilad Bracha and Martin Odersky and David Stoutamire and Philip Wadler",
    title = "Making the Future Safe for the Past: Adding Genericity to the {Java} Programming Language",
    booktitle = "Object Oriented Programming: Systems, Languages, and Applications ({OOPSLA})",
    address = "Vancouver, BC",
    editor = "Craig Chambers",
    pages = "183--200",
    year = "1998",
    url = "citeseer.nj.nec.com/bracha98making.html" }

@inproceedings{ bracha93strongtalk,
    author = "Gibblad Bracha and David Griswold",
    title = "{Strongtalk: Typechecking Smalltalk in a Production Environment}",
    booktitle = "Proceedings of the \mbox{OOPSLA}~'93 Conference on Object-oriented Programming Systems, Languages and Applications",
    pages = "215--230",
    year = "1993",
    url = "citeseer.nj.nec.com/bracha93strongtalk.html" }


@inproceedings{ brandt97coinductive,
    author = "Michael Brandt and Fritz Henglein",
    title = "Coinductive axiomatization of recursive type equality and subtyping",
    booktitle = "Proc.\ 3d Int'l Conf. on Typed Lambda Calculi and Applications ({TLCA}), Nancy, France, April 2-4, 1997",
    volume = "1210",
    publisher = "Springer-Verlag",
    editor = "Roger Hindley",
    pages = "63--81",
    year = "1997",
    url = "citeseer.nj.nec.com/brandt98coinductive.html" }


@inproceedings{breazu-tannen+:computing-w-coercions,
  author =	 "Val Breazu-Tannen and Carl A. Gunter and Andre
                  Scedrov",
  title =	 "Computing with Coercions",
  booktitle =	 1990 # " " # lfp,
  year =	 1990,
  pages =	 "44--60",
}

@article{breazu-tannen+:implicit-coercion,
  author =	 "Val Breazu-Tannen and Thierry Coquand and Carl
                  A. Gunter and Andre Scedrov",
  title =	 "Inheritance as Implicit Coercion",
  journal =	 iandc,
  year =	 1991,
  volume =	 93,
  pages =	 "172--221",
}

@Article{Bobrow:1988:CLOa,
  author =       "Daniel G. Bobrow and Linda G. Demichiel and Richard P.
                 Gabriel and Sonya E. Keene and Gregor Kiczales And
                 David A. Moon",
  title =        "{Common Lisp Object System} Specification 1.
                 Programmer Interface Concepts",
  journal =      j-LISP-SYMB-COMPUT,
  volume =       "1",
  number =       "2",
  pages =        "245--298",
  month =        sep,
  year =         "1988",
  CODEN =        "LSCOEX",
  ISSN =         "0892-4635",
  bibdate =      "Fri Feb 12 06:09:25 1999",
  acknowledgement = ack-nhfb,
}

@Article{Bobrow:1988:CLOb,
  author =       "Daniel G. Bobrow and Linda G. Demichiel and Richard P.
                 Gabriel and Sonya E. Keene and Gregor Kiczales And
                 David A. Moon",
  title =        "{Common Lisp Object System} Specification 2. Functions
                 in the Programmer Interface",
  journal =      j-LISP-SYMB-COMPUT,
  volume =       "1",
  number =       "2",
  pages =        "299--394",
  month =        sep,
  year =         "1988",
  CODEN =        "LSCOEX",
  ISSN =         "0892-4635",
  bibdate =      "Fri Feb 12 06:09:25 1999",
  acknowledgement = ack-nhfb,
}

@article{bruce+:binary-methods,
  author =	 "Kim B. Bruce and Luca Cardelli and Giuseppe Castagna
                  and The Hopkins Objects Group and Gary T. Leavens
                  and Benjamin C. Pierce",
  title =	 "On Binary Methods",
  journal =	 "Theory and Practice of Object Systems",
  volume =	 1,
  number =	 3,
  pages =	 "221--242",
  year =	 1996,
}

@inproceedings{bruce+:comp-obj-encodings,
  author =	 "Kim B. Bruce and Luca Cardelli and Benjamin
                  C. Pierce",
  title =	 "Comparing Object Encodings",
  booktitle =	 "Theoretical Aspects of Computer Software",
  address =	 "Sendai, Japan",
  year =	 1997,
  month =	 sep,
}

@article{bruce+:modest-model,
  author =	 "Kim B. Bruce and Giuseppe Longo",
  title =	 "A Modest Model of Records, Inheritance, and Bounded
                  Quantification",
  journal =	 iandc,
  year =	 1991,
  volume =	 87,
  pages =	 "196--240",
}


@article{bruce:paradigm-oop,
  author =	 "Kim B. Bruce",
  title =	 "A Paradigmatic Object-Oriented Programming Language:
                  Design, Static Typing and Semantics",
  journal =	 jfp,
  year =	 1994,
  month =	 apr,
  volume =	 4,
  number =	 2,
  pages =	 "127--206",
}

%% C %%



@inproceedings{canning+:f-bound-oop,
  author =	 "Peter Canning and William Cook and Walter Hill and
                  John Mitchell and Walter Olthoff",
  title =	 "F-Bounded Quantification for Object-Oriented
                  Programming",
  booktitle =	 "FPCA89: " # fpca,
  year =	 1989,
  month =	 sep,
  pages =	 "273--280",
}

@inproceedings{cardelli+:fsub,
  author =	 "Luca Cardelli and Simone Martini and John
                  C. Mitchell and Andre Scedrov",
  title =	 "An Extension of System {F} With Subtyping",
  booktitle =	 tacs # " 1991",
  address =	 "Sendai, Japan",
  year =	 1991,
  pages =	 "750--770",
  series =	 lncs,
  volume =	 526,
  publisher =	 springer,
}

@article{cardelli+:fun,
  author =	 "Luca Cardelli and Peter Wegner",
  title =	 "On Understanding Types, Data Abstraction, and
                  Polymorphism",
  journal =	 "Computing Surveys",
  volume =	 17,
  number =	 4,
  year =	 1985,
  month =	 dec,
  pages =	 "471--522",
}

@techreport{cardelli+:modula3,
  title =	 "Modula-3 Report (Revised)",
  author =	 "Luca Cardelli and James Donahue and Lucille Glassman
                  and Mick Jordan and Bill Kalsow and Greg Nelson",
  month =	 nov,
  year =	 1989,
  number =	 52,
  institution =	 dec-src,
}

@incollection{cardelli:amber,
  author =	 "Luca Cardelli",
  title =	 "Amber",
  booktitle =	 "Combinators and Functional Programming Languages",
  publisher =	 springer,
  editor =   "Guy Coisineau and Pierre-Louis Curien and Bernard Robinet",
  series =	 lncs,
  volume =	 242,
  pages = "48--70",
  year =	 1986
}

@techreport{cardelli:extensible-records,
  author =	 "Luca Cardelli",
  title =	 "Extensible Records in a Pure Calculus of Subtyping",
  institution =	 dec-src,
  year =	 1993,
  type =	 "SRC Research Report",
  number =	 "81",
  month =	 jan,
}

@unpublished{cardelli:f-omega-sub,
  author =	 "Luca Cardelli",
  title =	 "Notes about {F$^\omega_{<:}$}",
  note =	 "Unpublished manuscript",
  year =	 1990,
}

@techreport{cardelli:fsub-impl,
  author =	 "Luca Cardelli",
  title =	 "An Implementation of ${F}_{<:}$",
  institution =	 dec-src,
  year =	 1993,
  month =	 feb,
  type =	 "SRC Research Report",
  number =	 "97",
}

@article{cardelli:inherit-semantics,
  author =	 "Luca Cardelli",
  title =	 "A semantics of multiple inheritance",
  journal =	 iandc,
  volume =	 76,
  pages =	 "138--164",
  year =	 1988,
}

@unpublished{cardelli:phase,
  author =	 "Luca Cardelli",
  title =	 "Phase Distinctions in Type Theory",
  note =	 "Unpublished manuscript",
  year =	 1988,
  month =	 jan,
}

@inproceedings{cardelli:power-type,
  author =	 "Luca Cardelli",
  title =	 "Structural Subtyping and the Notion of Power Type",
  booktitle =	 o15 # " " # popl,
  year =	 1988,
  month =	 jan,
  pages =	 "70--79",
  address =	 "San Diego",
}

@incollection{cardelli:typeful,
  author =	 "Luca Cardelli",
  title =	 "Typeful Programming",
  booktitle =	 "Formal Description of Programming Concepts",
  year =	 1991,
  publisher =	 "Springer-Verlag",
}

@inproceedings{ cartwright98compatible,
    author = "Robert Cartwright and Guy L. {Steele, Jr.}",
    title = "Compatible Genericity with Run-time Types for the {Java} Programming Language",
    booktitle = "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming: {S}ystems, {L}anguages, and {A}pplications ({OOPSLA}), Vancouver, British Columbia",
    publisher = "ACM",
    editor = "Craig Chambers",
    pages = "201--215",
    year = "1998",
    url = "citeseer.nj.nec.com/cartwright98compatible.html" }


@Manual{mlton,
  title = 		  {MLton User Guide},
  author =		  {Henry Cejtin and Matthew Fluet and Suresh Jagannathan and Stephen Weeks},
  month =		  apr,
  year =			  2000,
  note =			  {\url{http://www.mlton.org/HTML/main.html}}
}

@Misc{cert:denial,
  key =		 {CERT00},
  author =	 {CERT Coordination Center and the Federal Computer
                  Incident Response Capability (FedCIRC)},
  title =	 {{CERT} Advisory CA-2000-01 Denial-of-Service
                  Developments},
  howpublished = {http://www.cert.org/advisories/CA-2000-01.html},
  month =	 jan,
  year =	 2000
}

@inproceedings{ chak-keller:more-types,
  author = 	 {Manuel M. T. Chakravarty and Gabriele Keller},
  title = 	 {More Types for Nested Data Parallel Programming},
  editor =	 {Philip Wadler},
  booktitle = 	 {Proceedings of the Fifth ACM SIGPLAN International 
		 Conference on Functional Programming (ICFP'00)},
  year =	 2000,
  publisher =	 {ACM Press},
  pages =        {94--105},
  url = {citeseer.nj.nec.com/chakravarty00more.html} }



 @InProceedings{chak:array-fusion,
  author = 		  {Manuel M. T. Chakravarty and Gabriele Keller},
  title = 		  {Functional Array Fusion},
  booktitle = 	  {Proceedings of the Sixth ACM SIGPLAN International 
                  Conference on Functional Programming},
  pages =		  {205--216},
  year =			  2002,
  address =		  {Florence, Italy},
  month =		  sep,
  publisher =	  {{ACM} Press}
}

@InProceedings{cheung+:routing,
  author =	 {Steven Cheung and Karl N. Levitt},
  title =	 {Protecting routing infrastructures from denial of
                  service using cooperative intrusion detection },
  booktitle =	 {Proceedings of the Workshop on New Paradigms},
  year =	 1998,
  address =	 {Charlottesville, VA},
  month =	 sep
}

@InProceedings{chin00sized,
  author =	 {Wei-Ngan Chin and Siau-Cheng Khoo},
  title =	 {Calculating Sized Types},
  booktitle =	 pepm,
  pages =	 "62--72",
  year =	 2000,
  address =	 {Boston,USA},
  month =	 jan
}


@Article{church:simple-types,
  author = 		  {Alonzo Church},
  title = 		  {A Formulation of the Simple Theory of Types},
  journal = 	  {Journal of Symbolic Logic},
  year = 		  1940,
  volume =		  5,
  pages =		  {56--68}
}

@InProceedings{clark90:_archit_consid,
  author =	 {D. Clark and D. Tennenhouse},
  title =	 {Architectural Considerations for a new generation of
                  protocols},
  booktitle =	 sigcomm,
  year =	 1990,
  address =	 {Philadelphia, Pennsylvania},
  month =	 sep
}



@TechReport{generic-haskell,
  author = 		  {Dave Clarke and Ralf Hinze and Johan Jeuring and Andres L\"{o}h and Jan de Wit},
  title = 		  {The {G}eneric {H}askell user's guide},
  institution =  {Utrecht University },
  year = 		  2001,
  number =		  {UU-CS-2001-26}
}


@techreport{CoFu92,
 author      = "Robin Cockett and Tom Fukushima",
 title       = "About {C}harity",
 institution = "Department of Computer Science, The University of Calgary",
 month       = jun,
 year        = 1992,
 type        = "Yellow Series Report",
 number      = "No.\ 92/480/18"
}

@InProceedings{cointe:meta-classes,
  author = 		  {Pierre Cointe},
  title = 		  {Metaclasses are first class: The {ObjVlisp} model},
  booktitle = 	  {Proceedings of the ACM Conference on Object-Oriented Programming Systems,
 Languages, and Applications (OOPSLA)},
  pages =		  {156--167},
  year =			  1987,
  address =		  { Orlando, FL}
}

@MISC{COM,
  KEY = {COM},
  TITLE = {{M}icrosoft {COM} Technologies},
  month = jan,
  year = 2002,
  NOTE = {\url{http://www.microsoft.com/com/default.asp}}
}


@article{compagnoni+:intersect-mult-inherit,
  author =	 "Adriana B. Compagnoni and Benjamin C. Pierce",
  title =	 "Higher-Order Intersection Types and Multiple
                  Inheritance",
  journal =	 mscs,
  pages =	 "469--501",
  month =	 oct,
  year =	 1996,
  volume =	 6,
  number =	 5,
}



@inproceedings{constable+:comp-founds-fn-thy,
  author =	 "Robert L. Constable and Scott Fraser Smith",
  title =	 "Computational Foundations of Basic Recursive
                  Function Theory",
  booktitle =	 o3 # " " # lics,
  year =	 1988,
  address =	 "Edinburgh, Scotland",
  pages =	 "360--371",
  month =	 jul,
}

@inproceedings{constable+:intensional-analysis,
  author =	 "Robert L. Constable and Karl Crary",
  title =	 "Computational Complexity and Induction for Partial
                  Computable Functions in Type Theory",
  booktitle =	 "Feferman Festschrift",
  year =	 1998,
  month =	 dec
}



@book{constable+:nuprl,
  title =	 "Implementing Mathematics with the {N}uprl Proof
                  Development System",
  author =	 "Robert L. Constable and Stuart F. Allen and H. Mark Bromley and
                  W. Rance Cleaveland and James F. Cremer and Robert W. Harper and
                  Douglas J. Howe and Todd B. Knoblock and Nax Paul Mendler and
                  Prakash Panangaden and James T. Sasaki and Scott F. Smith",
  publisher =	 "Prentice-Hall",
  year =	 1986,
}

@inproceedings{constable+:partial-objs,
  author =	 "Robert L. Constable and Scott F. Smith",
  title =	 "Partial Objects in Constructive Type Theory",
  booktitle =	 o2 # " " # lics,
  year =	 1987,
  month =	 jun,
  pages =	 "183--193",
  address =	 ith-ny,
}

@article{constable+:plcv3,
  author =	 "Robert L. Constable and Daniel R. Zlatin",
  title =	 "The Type Theory of {PL/CV3}",
  journal =	 toplas,
  volume =	 6,
  number =	 1,
  year =	 1984,
  month =	 jan,
  pages =	 "94--117",
}

@techreport{constable:ita,
  author =	 "Robert L. Constable",
  title =	 "Intensional Analysis of Functions and Types",
  year =	 1982,
  month =	 jun,
  number =	 "CSR-118-82",
  institution =	 edin-cs,
}

@incollection{constable:math-as-programming-logic,
  author =	 "Robert L. Constable",
  title =	 "Constructive Mathematics as a Programming Logic {I}:
                  Some Principles of Theory",
  booktitle =	 "Topics in the Theory of Computation",
  series =	 "Annals of Discrete Mathematics",
  volume =	 24,
  publisher =	 elsevier,
  year =	 1985,
  pages =	 "21--37",
  note =	 "Selected papers of the International Conference on
                  Foundations of Computation Theory 1983",
}

@inproceedings{constable:tt-found-cs,
  author =	 "Robert L. Constable",
  title =	 "Type Theory as a Foundation for Computer Science",
  booktitle =	 tacs # " 1991",
  address =	 "Sendai, Japan",
  year =	 1991,
  pages =	 "226--243",
  series =	 lncs,
  volume =	 526,
  publisher =	 springer,
}

@incollection{constable:types-logic-math-prog,
  author =	 "Robert L. Constable",
  title =	 "Types in Logic, Mathematics and Programming",
  booktitle =	 "Handbook of Proof Theory",
  editor =	 "Sam Buss",
  chapter =	 10,
  year =	 1998,
  publisher =	 "Elsevier Science",
}

@inproceedings{cook+:inherit-not-subtyping,
  author =	 "William R. Cook and Walter L. Hill and Peter
                  S. Canning",
  title =	 "Inheritance is not Subtyping",
  booktitle =	 o17 # " " # popl,
  pages =	 "125--135",
  month =	 jan,
  year =	 1990,
  address =	 "San Francisco",
}

@TechReport{coq-manual,
  title =	 "The {Coq} Proof Assistant Reference Manual: Version 6.1",
  author =	 "Bruno Barras and Samuel Boutin and Cristina Cornes
                  and {Judica\"{e}l} Courant and Jean-Christophe
                  Filli\^{a}tre and Eduardo Gim\'{e}nez and Hugo
                  Herbelin and G\'{e}rard Huet and C\'{e}sar
                  {Mu\~{n}oz} and Chetan Murthy and Catherine Parent
                  and Christine Paulin-Mohring and Amokrane
                  {Sa\"{\i}bi} and Benjamin Werner",
  institution = "{INRIA-Rocquencourt, CNRS and ENS Lyon}",
  number = "RT-0203",
  year = "1997",

}

@article{coquand+:coc,
  author =	 "Thierry Coquand and G\'{e}rard Huet",
  title =	 "The Calculus of Constructions",
  journal =	 iandc,
  year =	 1988,
  volume =	 76,
  pages =	 "95--120",
}

@inproceedings{coquand:girard-paradox,
  author =	 "Thierry Coquand",
  title =	 "An Analysis of {G}irard's Paradox",
  booktitle =	 o1 # " " # lics,
  year =	 1986,
  month =	 jun,
  pages =	 "227--236",
  address =	 cam-ma,
}

@incollection{coquand:investigate-coc,
  author =	 "Thierry Coquand",
  title =	 "Metamathematical Investigations of a Calculus of
                  Constructions",
  booktitle =	 "Logic and Computer Science",
  pages =	 "91--122",
  year =	 1990,
  series =	 "The {APIC} Series",
  volume =	 31,
  editor =	 "P. Odifreddi",
  publisher =	 academic,
}




@InProceedings{coquand+:inductively,
  author = 	 {Thierry Coquand and Christin Paulin-Mohring},
  title = 	 {Inductively Defined Types},
  booktitle = 	 {COLOG-88 International Conference on Computer Logic},
  pages =	 {50--66},
  year =	 1988,
  editor =	 {P. Martin-L\"{o}f and G. Mints},
  volume =	 417,
  series =	 lncs,
  address =	 {Tallinn, USSR},
  month =	 dec,
  publisher =	 springer
}

@Incollection{coquand:new-paradox,
  author =	 {Thierry Coquand},
  editor =	 {Dag Prawitz and Brian Skyrms and Dag Westerst\aa{}hl},
  booktitle = {Logic, Methodology and Philosophy of Science IX :
  Proceedings of the Ninth International Congress of Logic,
  Methodology, and Philosophy of Science, Uppsala, Sweden, August
  7-14, 1991},
  title = 	 {A New Paradox in Type Theory},
  publisher = 	 elsevier,
  volume = 134,
  year = 	 1994,
  pages = "555--570",
  address =	 {Amsterdam},
  url = "citeseer.nj.nec.com/coquand94new.html"
}

@InProceedings{coquand:conversion,
  author =		  {Thierry Coquand},
  editor =       {G\'{e}rard Huet and Gordon Plotkin},
  booktitle = 		  {Logical Frameworks},
  title = 	  {An Algorithm for Testing Conversion in Type Theory},
  publisher = 	  cambridge-press,
  year = 		  1991,
  pages =		  {255-277}
}

@inproceedings{crary+:capabilities,
  author =	 "Karl Crary and David Walker and Greg Morrisett",
  title =	 "Typed Memory Management in a Calculus of
                  Capabilities",
  year =	 1999,
  month =	 jan,
  booktitle =	 o26 # " " # popl,
  address =	 "San Antonio, Texas",
}

@techreport{crary+:datatypes,
  author =	 "Karl Crary and Robert Harper and Perry Cheng and
                  Leaf Petersen and Chris Stone",
  title =	 "Transparent and Opaque Interpretations of Datatypes",
  institution =	 cmu-cs,
  month =	 nov,
  year =	 1998,
  number =	 "CMU-CS-98-177",
  memo =	 "Also published as Fox Memorandum CMU-CS-FOX-98-04.",
}


@techreport{crary+:lx-tr,
  author =	 "Karl Crary and Stephanie Weirich",
  title =	 "Flexible Type Analysis (Extended version)",
  year =	 1999,
  institution =	 cornell-cs,
}

@InProceedings{crary+:popcron,
  author =	 {Karl Crary and Stephanie Weirich},
  title =	 {Resource Bound Certification},
  booktitle =	 o27 # " " # popl,
  pages =	 {184--198},
  year =	 2000,
  address =	 "Boston, MA",
  month =	 jan
}

@inproceedings{crary+:recmod,
  author =	 "Karl Crary and Robert Harper and Sidd Puri",
  title =	 "What is a Recursive Module?",
  booktitle =	 1999 # " " # pldi,
  month =	 may,
  year =	 1999,
  address =	 "Atlanta",
  memo =	 "Also published as TR CMU-CS-98-168 and Fox
                  Memorandum CMU-CS-FOX-98-03.",
}

@inproceedings{crary:admissibility,
  author =	 "Karl Crary",
  title =	 "Admissibility of Fixpoint Induction over Partial
                  Types",
  booktitle =	 o15 # " " # cade,
  year =	 1998,
  month =	 jul,
  address =	 "Lindau, Germany",
  pages =	 "270--285",
  publisher =	 springer,
  series =	 lncs,
  volume =	 1421,
  note =	 "Extended version published as CMU technical report
                  CMU-CS-98-164."
}

@techreport{crary:admissibility-tr,
  author =	 "Karl Crary",
  title =	 "Admissibility of Fixpoint Induction over Partial
                  Types",
  institution =	 cmu-cs,
  year =	 1998,
  month =	 oct,
  number =	 "CMU-CS-98-164",
}

@inproceedings{crary:ho-subtyping-impl,
  author =	 "Karl Crary",
  title =	 "Foundations for the Implementation of Higher-Order
                  Subtyping",
  booktitle =	 1997 # " " # icfp,
  year =	 1997,
  month =	 jun,
  address =	 "Amsterdam",
  pages =	 "125--135",
}

@manual{crary:kml96-manual,
  title =	 "{KML} Reference Manual",
  author =	 "Karl Crary",
  year =	 1996,
  organization = cornell-cs,
}

@techreport{crary:orei,
  author =	 "Karl Crary",
  title =	 "Simple, Efficient Object Encoding using Intersection
                  Types",
  institution =	 cmu-cs,
  year =	 1999,
  month =	 jan,
  number =	 "CMU-CS-99-100",
  memo =	 "Also published as Fox Memorandum CMU-CS-FOX-99-01",
}

@techreport{crary:orei-old,
  author =	 "Karl Crary",
  title =	 "Simple, Efficient Object Encoding using Intersection
                  Types",
  institution =	 cornell-cs,
  year =	 1998,
  month =	 apr,
  number =	 "TR98-1675",
}

@inproceedings{crary:param-sing,
  author =	 "Karl Crary",
  title =	 "A Simple Proof Technique for Certain Parametricity
                  Results",
  booktitle =	 1999 # " " # icfp,
  year =	 1999,
  month =	 sep,
  address =	 "Paris",
  pages =	 "82--89",
  memo =	 "Also published as CMU-CS-98-185 and Fox Memorandum
                  CMU-CS-FOX-98-06.",
}

@phdthesis{crary:phd,
  author =	 "Karl Crary",
  title =	 "Type-Theoretic Methodology for Practical Programming
                  Languages",
  month =	 aug,
  year =	 1998,
  school =	 cornell-cs,
  address =	 ith-ny,
}

@inproceedings{crary:tt-semant,
  author =	 "Karl Crary",
  title =	 "Programming Language Semantics in Foundational Type
                  Theory",
  booktitle =	 "International Conference on Programming Concepts and
                  Methods",
  year =	 1998,
  address =	 "Shelter Island, New York",
  publisher =	 chapman,
  note =	 "Extended version published as Cornell University
                  technical report TR98-1666.",
}

@techreport{crary:tt-semant-tr,
  author =	 "Karl Crary",
  title =	 "Programming Language Semantics in Foundational Type
                  Theory",
  institution =	 cornell-cs,
  year =	 1998,
  month =	 feb,
  number =	 "TR98-1666",
  address =	 ith-ny
}



@InProceedings{crary:subtyping,
  author = 	 {Karl Crary},
  title = 	 {Typed Compilation of Inclusive Subtyping},
  booktitle = 	 {International Conference on Functional Programming (ICFP '00)},
  year =	 2000,
  address =	 {Montreal, CA},
  month =	 sep
}

@inproceedings{curien+:coherence,
  author =	 "Pierre-Louis Curien and Giorgio Ghelli",
  title =	 "Coherence of Subsumption",
  booktitle =	 "Fifteenth Colloquium on Trees in Algebra and
                  Programming",
  publisher =	 springer,
  series =	 lncs,
  volume =	 431,
  year =	 1990,
  pages =	 "132--146",
}

@article{curien+:confluent-subs,
  author =	 "Pierre-Louis Curien and Th\'{e}r\`{e}se Hardin and
                  Jean-Jacques L\'{e}vy",
  title =	 "Confluence Properties of Weak and Strong Calculi of
                  Explicit Substitutions",
  journal =	 jacm,
  month =	 mar,
  year =	 1996,
  volume =	 43,
  number =	 2,
  pages =	 "362--397",
}

@Book{curry-feys,
  author =		  {Haskell Curry and Robert Feys},
  title = 		  { Combinatory Logic I},
  publisher = 	  { North-Holland},
  year = 		  1958
}

@inproceedings{czajkowki98:_jres,
  author =	 {Grzegorz Czajkowki and Thorsten von Eiken},
  title =	 {{JR}es: A Resource Accounting Interface for Java},
  booktitle =	 "Proceedings of the 1998 " # oopsla,
  pages =	 "21--35",
  year =	 1998,
  volume =	 33,
  number =	 10,
  series =	 {SIGPLAN Notices},
  month =	 oct
}

@inproceedings{czajkowski99database,
  author =	 {Grzegorz Czajkowski and Tobias Mayr and Praveen
                  Seshadri and Thorsten von Eicken},
  title =	 {Resource Control for Database Extensions},
  year =	 1999,
  booktitle =	 o5 # " " # "USENIX Conference on Object-Oriented
                  Technologies and Systems",
  month =	 may,
  address =	 {San Diego, California, USA}
}

%% D %%

@article{danvy+:control,
  author =	 "Olivier Danvy and Andrzej Filinski",
  title =	 "Representing control: a study of the {CPS}
                  transformation",
  journal =	 "Mathematical Structures in Computer Science",
  volume =	 2,
  number =	 4,
  month =	 dec,
  year =	 1992,
  pages =	 "361--391",
}

@inproceedings{ danvy96typedirected,
    author = "Olivier Danvy",
    title = "Type-Directed Partial Evaluation",
    booktitle = "{POPL}'96: The 23rd {ACM} {SIGPLAN}-{SIGACT}
    Symposium on Principles of Programming Languages, St. Petersburg,
    Florida, January 1996",
    pages = "242--257",
    year = "1996",
    url = "citeseer.nj.nec.com/danvy96typedirected.html"
}

@inproceedings{davies+:modal-logic-comp,
  author =	 "Rowan Davies and Frank Pfenning",
  title =	 "A Modal Analysis of Staged Computation",
  booktitle =	 o23 # " " # popl,
  year =	 1996,
  month =	 jan,
  pages =	 "258--270",
}

 
@Article{pfenning+:judgmental-reconstruct,
  author = 		  {Frank Pfenning and Rowan Davies.},
  title = 		  {A Judgmental Reconstruction of Modal Logic},
  journal = 	  {Mathematical Structures in Computer Science},
  year = 		  2001,
  volume =		  11,
  number =		  4,
  pages =		  {511--540},
  month =		  aug
}

@inproceedings{davies:temporal-logic-comp,
  author =	 "Rowan Davies",
  title =	 "A Temporal-Logic Approach to Binding-Time Analysis",
  booktitle =	 o11 # " " # lics,
  year =	 1996,
  month =	 jul,
  pages =	 "184--195",
}

@incollection{debruijn:automath-survey,
  author =	 "Nicolaas Govert de Bruijn",
  title =	 "A Survey of the Project {Automath}",
  booktitle =	 "To {H.B.} {Curry}: Essays on Combinatory Logic,
                  Lambda-Calculus and Formalism",
  editor =	 "J. Roger Seldin and Jonathan R. Hindley",
  pages =	 "579--606",
  publisher =	 "Academic Press",
  year =	 1980,
}

@article{debruijn:dummies,
  author =	 "Nicolaas Govert de Bruijn",
  title =	 "Lambda-Calculus Notation with Nameless Dummies: a
                  Tool for Automatic Formula Manipulation with
                  Application to the {Church-Rosser} Theorem",
  journal =	 "Indagationes Mathematicae",
  volume =	 34,
  number =	 5,
  year =	 1972,
  pages =	 "381--392",
}



@Book{des-rivieres:MOP,
  author =		  {Gregor Kiczales and Jim des Rivieres and Daniel Bobrow},
  title = 		  {The Art of the Meta-Object Protocol},
  publisher = 	  mit-press,
  year = 		  1991
}


@InProceedings{des-rivieres+:implementation-reflective,
  author = 		  {Jim des Rivieres and Brian Cantwell Smith},
  title = 		  {The implementation of procedurally reflective languages},
  booktitle = 	  {Conference Record of the 1984 ACM Symposium on LISP and Functional Programming},
  pages =		  {331--347},
  year =			  1984,
  address =		  {Austin, Texas},
    publisher = "ACM Press"
}

@inproceedings{demers+:reflection-survey,
  author = 		  {Francois-Nicola Demers and Jacques Malenfant},
  title = 		  {Reflection and logic, functional and object-oriented programming:
                  a Short Comparative Study},
  booktitle =    {{IJCAI '95} Workshop on Reflection and Metalevel Architectures
                 and their Applications in AI},
  pages =        {29--38},
  year =         1995,
  month =        aug,
  url = 		  {citeseer.nj.nec.com/106401.html}
 }

@Article{despeyroux+:functional,
  author = 	 {{Jo\"{e}lle} Despeyroux and Pierre Leleu },
  title = 	 {Recursion over Objects of Functional Type},
  journal = 	 {Mathematical Structures in Computer Science},
  year = 	 {2001},
  volume =      11,
  pages =        "555-572",
  publisher =    cambridge-press
}

@InProceedings{despeyroux+:functional-preprint,
  author = 	 {{Jo\"{e}lle} Despeyroux and Pierre Leleu },
  title = 	 {Recursion over Objects of Functional Type},
  booktitle = 	 {Proceedings of the Types Working Group Meeting at Kloster Irsee, 1998},
  year =	 1999,
  number =	 1657,
  series =	 lncs,
  address =	 {Berlin},
  publisher =	 springer
}


@InProceedings{despeyroux+:modal,
  author = 	 {{Jo\"{e}lle} Despeyroux and Pierre Leleu },
  title = 	 {A modal lambda-calculus with iteration and case constructs},
  booktitle = 	 {Proceedings of the Types Working Group Meeting at Kloster Irsee, 1998},
  year =	 1999,
  number =	 1657,
  series =	 lncs,
  address =	 berlin,
  publisher =	 springer
}

@inproceedings{despeyroux+:ho-recursion,
  author =	 "{Jo\"{e}lle} Despeyroux and Frank Pfenning and
                    {Carsten Sch\"{u}rmann}",
  title =	 "Primitive Recursion for Higher-Order Abstract
                  Syntax",
  booktitle =	 o3 # " " # tlca,
  year =	 1997,
  month =	 apr,
  address =	 "Nancy, France",
  pages =	 "147--163",
  series =	 lncs,
  volume =	 1210,
  publisher =	 springer,
  annote =	 "Extended version published as CMU technical report
                  CMU-CS-96-172.",
}

@inproceedings{dimock+:flow-transforms,
  title =	 "Strongly Typed Flow-Directed Representation
                  Transformations",
  author =	 "Allyn Dimock and Robert Muller and Franklyn Turbak
                  and J.~B.~Wells",
  booktitle =	 1997 # " " # icfp,
  year =	 1997,
  month =	 jun,
  address =	 "Amsterdam",
  pages =	 "11--24",
}

@InCollection{dobson91,
  author =	 {John E. Dobson},
  title =	 {Information and Denial of Service},
  booktitle =	 {Database Security V: Status and Prospects},
  series =	 {IFIP Transactions},
  volume =	 {A-6},
  pages =	 {21--46},
  year =	 1991
}

@inproceedings{dubois+:extensional-poly,
  author =	 "Catherine Dubois and Fran\c{c}ois Rouaix and Pierre
                  Weis",
  title =	 "Extensional Polymorphism",
  booktitle =	 o22 # " " # popl,
  address =	 "San Francisco",
  month =	 jan,
  year =	 1995,
  pages =	 "118--129",
}

@inproceedings{duggan:marshalling,
  author =	 "Dominic Duggan",
  title =	 "A Type-Based Semantics for User-Defined Marshalling
                  in Polymorphic Languages",
  booktitle =	 o2 # " " # tic,
  year =	 1998,
  month =	 mar,
}

@InProceedings{duggan:tmal,
  author = 	 {Dominic Duggan},
  title = 	 {Sharing in Typed Module Assembly Language},
  booktitle = 	 {Types in Compilation : Third International Workshop, {TIC} 2000 Montreal;
 Canada, September 21, 2000; Revised Selected Papers},
  year =	 2001,
  editor =	 {R. Harper},
  pages =        {85--116},
  volume =	 2071,
  series =	 lncs,
  address =	 {Berlin},
  publisher =	 {Springer}
}

@book{dummett:intuitionism,
  author =	 "Michael Dummett",
  title =	 "Elements of Intuitionism",
  publisher =	 "Clarendon Press",
  year =	 1977,
  series =	 "Oxford Logic Guides",
}


@InCollection{dybjer:inductive,
  author = 	 {Peter Dybjer},
  title = 	 {Inductive sets and families in {M}artin-{L}\"of's 
                  type theory and their set-theoretic semantics},
  booktitle = 	 {Logical Frameworks},
  pages =	 {280--306},
  year =	 1991,
  editor =	 {Gerard Huet and Gordon
     Plotkin},
  publisher =	 {Prentice Hall}
}

%% E %%

@incollection{eifrig+:constrained-types,
  author =	 "J. Eifrig and S. Smith and V. Trifonov",
  title =	 "Type Inference for Recursively Constrained Types and
                  its Application to {OOP}",
  booktitle =	 mfps,
  publisher =	 elsevier,
  series =	 "Electronic Notes in Theoretical Computer Science",
  volume =	 1,
  year =	 1995,
}

@BOOKLET{ELF,
  AUTHOR = {{T}ool {I}nterface {S}tandards {C}ommittee},
  TITLE = {{E}xecutable and {L}inking {F}ormat ({ELF}) Specification},
  MONTH = {May},
  YEAR = {1995},
  HOWPUBLISHED = {\url{http://x86.ddj.com/ftp/manuals/tools/elf.pdf}}
}


@InProceedings{engblom98optimize,
  author =	 {Jakob Engblom and Andreas Ermedahl and Peter
                  Altenbernd},
  title =	 {Facilitating worst-case execution time analysis of
                  optimized code},
  booktitle =	 {Proceedings of the 10th EuroMicro Workshop on
                  Real-Time Systems},
  year =	 1998,
  address =	 {Berlin, Germany},
  month =	 jun
}

@INPROCEEDINGS{EnglerKO95,
  TITLE = {{E}xokernel: an operating system architecture for application-level
           resource management},
  AUTHOR = {Dawson R. Engler and M. Frans Kaashoek and James {O'Toole Jr.}},
  BOOKTITLE = {Proceedings of the 15th {ACM} {S}ymposium on {O}perating
               {S}ystems {P}rinciples},
  YEAR = {1995},
  MONTH = {December},
  ADDRESS = {Copper Mountain Resort, Colorado},
  PAGES = {251--266},
  URL = {http://www.pdos.lcs.mit.edu/papers/exokernel-sosp95.ps}
}



@InProceedings{erlingsson99sasi,
  author =	 {\'{U}lfar Erlingsson and Fred B. Schneider},
  title =	 {{SASI} Enforcement of Security Policies: A
                  Retrospective},
  booktitle =	 {Proceedings of the 1999 New Security Paradigms
                  Workshop},
  year =	 1999,
  address =	 {Caledon Hills, Ontario, Canada},
  month =	 sep
}

%% F %%

@Article{feferman62,
  author = 		  {Solomon Feferman},
  title = 		  { Transfinite Recursive Progressions of Axiomatic Theories.},
  journal = 	  { Journal of Symbolic Logic},
  year = 		  1962,
  volume =		  27,
  number =		  3,
  pages =		  {259--316},
  month =		  sep
}

@inproceedings{ fegaras+:outer-space,
    author = "Leonidas Fegaras and Tim Sheard",
    title = "Revisiting Catamorphisms over Datatypes with Embedded Functions (or, Programs from Outer Space)",
booktitle = o23 # popl,
 address = {St.~Petersburg Beach, {FL},{USA}},
   pages = "284--294",
    year = 1996,
    annote =	 {Also: OGI Technical Report 95/014},
    url = "citeseer.nj.nec.com/article/fegaras96revisiting.html" }

%    publisher = "ACM Press",
%    address = "New York",
%    booktitle = "Conf.\ Record 23rd {ACM} {SIGPLAN}/{SIGACT} Symp.\ 
%         on Principles of Programming Languages, {POPL}'96, 
%         St.~Petersburg Beach, {FL}, {USA}, 21--24 Jan.\ 1996",


@InCollection{ferdinand98cache,
  author =	 {Christian Ferdinand and Reinhard Wilhelm},
  title =	 {On predicting Data Cache Behavior for Real-Time
                  systems},
  booktitle =	 lctes,
  pages =	 "16--30",
  publisher =	 springer,
  year =	 1998,
  editor =	 {Frank Muller and Azer Bestarvros},
  volume =	 1474,
  series =	 lncs,
  month =	 jun
}

@phdthesis{filinski:phd,
  author =	 "Andrzej Filinski",
  title =	 "Controlling Effects",
  year =	 1996,
  month =	 may,
  school =	 cmu-cs,
  address =	 pgh-pa,
}

@inproceedings{fischer:cps,
  author =	 "M.J. Fischer",
  title =	 "Lambda calculus schemata",
  booktitle =	 "ACM Conference on Proving Assertions About Programs,
                  SIGPLAN Notices 7(1)",
  year =	 1972,
  pages =	 "104--109",
}


@inproceedings{flatt+:units,
  author =	 "Matthew Flatt and Matthias Felleisen",
  title =	 "Units: Cool Modules for {HOT} Languages",
  booktitle =	 1998 # " " # pldi,
  pages =	 "236--248",
  year =	 1998,
  month =	 jun,
  address =	 "Montreal, Canada",
}



@InProceedings{freeman91refinement,
  author = 	 {Tim Freeman and Frank Pfenning},
  title = 	 {Refinement Types for {ML}},
  booktitle = 	 1991 # " " # pldi,
  pages =	 {268--277},
  year =	 1991,
  address =	 {Toronto, Canada},
  month =	 jun
}

@InBook{friedman:equality,
  author =		  {H. Friedman},
  editor =		  {R. Parikh},
  chapter = 		  {Equality between functionals},
  title = 	  {Logic Colloquium},
  publisher = 	  {Springer-Verlag},
  year = 		  1975,
  address =		  {Berlin},
  pages =		  {22--37}
}

%% G %%

@Article{PittsAM:newaas-jv,
  author =	 {M. J. Gabbay and A. M. Pitts},
  title =	 {A New Approach to Abstract Syntax with Variable
                  Binding},
  journal =	 {Formal Aspects of Computing},
  year =	 2001,
  volume =	 13,
  pages =	 {341--363}
}


@incollection{gallier:candidates-of-reducibility,
  author =	 "Jean H. Gallier",
  title =	 "On {Girard's} ``{Candidats} de {Reductibilit{\'{e}}}''",
  booktitle =	 "Logic and Computer Science",
  pages =	 "123--203",
  year =	 1990,
  series =	 "The {APIC} Series",
  volume =	 31,
  editor =	 "P. Odifreddi",
  publisher =	 academic,
}

@InProceedings{gapayev+:regular-object-types,
  author = 	 {Vladimir Gapeyev and Benjamin Pierce},
  title = 	 {Regular Object Types},
  booktitle = 	 {Proc. 10th International Workshops on Foundations of Object-Oriented Languages, FOOL '03},
  year =	 2003,
  address =	 {New Orleans, LA, USA},
  month =	 jan
}

@InCollection{gandy:turing-proof,
  author =		  {Robin O. Gandy},
  editor =	 "J. Roger Seldin and Jonathan R. Hindley",
  title = 		  { An Early Proof of Normalization by {A.M. Turing}},
  booktitle = 	  {  Introduction to Combinators and $\lambda$-Calculus },
  publisher = 	  cambridge-press,
  year = 		  1986,
  series =		  {London Mathematical Society Student Texts},
  address =		  {Cambridge},
  pages =		  {453--455 }
}

@InProceedings{garrigue:poly-variants,
  author = 	 {J. Garrigue},
  title = 	 {Programming with polymorphic variants},
  booktitle = 	 {ML Workshop},
  url = "citeseer.nj.nec.com/garrigue98programming.html",
  year =	 1998,
  month =	 sep
}


@inproceedings{gifford+:effects,
title = "Integrating functional and imperative programming",
author = "D. K. Gifford and J. M. Lucassen",
booktitle = "{ACM} Conference on {Lisp} and Functional Programming",
address = "Cambridge, Massachusetts",
month = aug,
year = 1986
}


@article{ghelli:fsub-divergence,
  author =	 "Giorgio Ghelli",
  title =	 "Divergence of {$F_{\leq}$} type checking",
  journal =	 "Theoretical Computer Science",
  volume =	 139,
  number =	 "1,2",
  pages =	 "131--162",
  year =	 1995,
}

@phdthesis{ghelli:phd,
  author =	 "Giorgio Ghelli",
  title =	 "Proof Theoretic Studies about a Minimal Type System
                  Integrating Inclusion and Parametric Polymorphism",
  school =	 "Dipartimento di Informatica, Universit\`{a} di Pisa",
  year =	 1990,
  month =	 mar,
}

@book{girard+:proofs-and-types,
  author =	 "Jean-Yves Girard and Yves Lafont and Paul Taylor",
  title =	 "Proofs and Types",
  publisher =	 cambridge-press,
  year =	 1988,
}

@inproceedings{girard:cut-elimination,
  author =	 "Jean-Yves Girard",
  title =	 "Une extension de l'interpr\'{e}tation de {G\"{o}del}
                  \`{a} l'analyse, et son application \`{a}
                  l'\'{e}limination de coupures dans l'analyse et la
                  th\'{e}orie des types",
  editor =	 "J. E. Fenstad",
  booktitle =	 "Proceedings of the Second Scandinavian Logic
                  Symposium",
  pages =	 "63--92",
  year =	 1971,
  publisher =	 "North-Holland Publishing Co.",
}

@article{girard:linear,
  title =	 "Linear Logic",
  author =	 "Jean-Yves Girard",
  journal =	 "Theoretical Computer Science",
  year =	 1987,
  volume =	 50,
  pages =	 "1--102",
}

@phdthesis{girard:phd,
  author =	 "Jean-Yves Girard",
  title =	 "Interpr\'{e}tation fonctionelle et \'{e}limination
                  des coupures de l'arithm\'{e}tique d'ordre
                  sup\'{e}rieur",
  school =	 "Universit\'{e} Paris VII",
  year =	 1972,
}



@InProceedings{glew:branded,
  author = 		  {Neal Glew},
  title = 		  {Type Dispatch for Named Hierarchical Types},
  booktitle =	  1999 # " " # icfp,
  pages =		  {172--182},
  year =			  1999,
  address =		  {Paris, France},
  month =		  sep
}

@inproceedings{glew+:linking,
  author =	 "Neal Glew and Greg Morrisett",
  title =	 "Type-Safe Linking and Modular Assembly Language",
  year =	 1999,
  booktitle =	 o26 # " " # popl,
  month =	 jan,
  address =	 {San Antonio, TX},
  pages =	 {250--261}
}

@Article{gligor84:os,
  author =	 {Virgil D. Gligor},
  title =	 {A Note on Denial-of-Service in Operating Systems},
  journal =	 {IEEE Transactions on Software Engineering},
  year =	 1984,
  volume =	 10,
  number =	 3,
  pages =	 {320--324}
}

@inproceedings{gligor86:_denial_servic_comput_networ,
  author =	 {Virgil D. Gligor},
  title =	 {On Denial-of-Service in Computer Networks},
  booktitle =	 {Proceedings of the Second International Conference
                  on Data Engineering, February 5-7, 1986, Los
                  Angeles, California, USA},
  publisher =	 {IEEE Computer Society},
  year =	 1986,
  isbn =	 {0-8186-0655-X},
  pages =	 {608-617},
  crossref =	 {DBLP:conf/icde/86},
  bibsource =	 {DBLP, http://dblp.uni-trier.de}
}

@Article{godel:incompleteness,
  author = 		  {Kurt Godel},
  title = 		  {\"{U}ber formal unentschiedbare S\"atze der 
                     Principia Mathematica und verwandter Systeme, {I}},
  journal = 	  {Monatshefte f\"ur Mathematik und Physik},
  year = 		  1931,
  volume =		  38,
  pages =		  {173--98}
}

@InProceedings{godfrey98:_secur_portab_datab_exten,
  author =	 {M. Godfrey and T. Mayr and P. Seshadri and T. von
                  Eiken},
  title =	 {Secure and Portable Database Extensibility},
  booktitle =	 sigmod,
  year =	 1998,
  volume =	 27,
  number =	 2,
  series =	 {SIGMOD Record},
  month =	 jun
}

@book{gordon+:hol,
  author =	 "Michael J. C. Gordon and Tom F. Melham",
  title =	 "Introduction to {HOL}: A Theorem Proving Environment
                  for Higher-Order Logic",
  publisher =	 cambridge-press,
  year =	 1993,
}

@inproceedings{gordon+:imperative-objs,
  author =	 "Andrew D. Gordon and Paul D. Hankin and {S\o ren}
                  B. Lassen",
  title =	 "Compilation and Equivalence of Imperative Objects",
  booktitle =	 "Foundations of Software Technology and Theoretical
                  Computer Science",
  year =	 1997,
  month =	 dec,
  series =	 lncs,
  volume =	 1346,
  publisher =	 springer,
}

@book{gordon+:lcf,
  author =	 "Michael J. Gordon and Arthur J. Milner and
                  Christopher P. Wadsworth",
  title =	 "Edinburgh {LCF}: A Mechanised Logic of Computation",
  publisher =	 springer,
  series =	 lncs,
  year =	 1979,
  volume =	 78,
}

@book{gosling+:java,
  author =	 "James Gosling and Bill Joy and Guy Steele",
  title =	 "The {Java} Language Specification",
  publisher =	 addison,
  year =	 1996,
}

@inproceedings{gougen+:datatypes,
   author = "J. A. Goguen and J. W. Thatcher and E. G. Wagner",
   title = "An initial algebra approach to the specification, 
             correctness and implementation of abstract data types.",
   editor = "R. T. Yeh",
   booktitle = "Current Trends in Programming Methodology IV: 
              Data Structuring",
   pages = "80--144",
   publisher = "Prentice Hall",
   year = 1978
} 




@InProceedings{green:java-reflection,
  author =		  {Dale Green},
  editor =		  {Mary Campione and Kathy Walrath and  Alison Huml and Tutorial Team},
  booktitle = 		  {The Java Tutorial Continued: The Rest of the JDK(TM) },
  title = 	  {Trail: The Reflection {API}},
  publisher = 	  {Addison-Wesley Pub Co},
  year = 		  1998,
  note =			  {\url{http://java.sun.com/docs/books/tutorial/reflect/index.html}}
}

@Article{grossman:sta,
  author = 		  {Dan Grossman and Greg Morrisett and Steve Zdancewic},
  title = 		  {Syntactic Type Abstraction},
  journal = 	  toplas,
  year = 		  2000,
  volume =		  22,
  number =		  6,
  pages =		  {1037--1080},
  month =		  nov
}

@InProceedings{grossman+:tic,
  author =	 {Dan Grossman and Greg Morrisett},
  title =	 {Scalable Certification of Native Code: Experience
                  from Compiling to TALx86},
  booktitle = 	 "Preliminary Proceedings of the Third " # tic,
  year =	 2000,
  address =	 {Montreal, CA},
  month =	 sep,
  note =	 {Extended version published as Cornell University Computer Science technical 
report TR2000-1783}
}

@TechReport{grossman00,
  author =	 {Dan Grossman and Greg Morrisett},
  title =	 {Scalable Certification of Native Code: Experience
                  from Compiling to TALx86},
  institution =	 cornell-cs,
  year =	 2000,
  number =	 {TR2000-1783},
  month =	 feb
}


@book{gunter+:theoretical-oop,
  editor =	 "Carl A. Gunter and John C. Mitchell",
  title =	 "Theoretical Aspects of Object-Oriented Programming",
  publisher =	 mit-press,
  year =	 1994,
  address =	 cam-ma
}

%% H %%

@article{ hall96type,
    author = "Cordelia V. Hall and Kevin Hammond and Simon L. {Peyton Jones} and Philip L. Wadler",
    title = "Type Classes in {H}askell",
    journal = "ACM Transactions on Programming Languages and Systems",
    volume = "18",
    number = "2",
    month = mar,
    publisher = "ACM Press",
    pages = "109--138",
    year = "1996"
}
#    url = "citeseer.nj.nec.com/article/hall96type.html" 



@TechReport{harrison:survey,
  author =		  {John Harrison},
  title =		  {Metatheory and Reflection in Theorem Proving: A Survey and 
                  Critique},
  institution =  {SRI},
  number =		  {CRC-053},
  month =		  feb,
  year =			  1995
}

@inproceedings{harper+:cps,
  author =	 "Robert Harper and Mark Lillibridge",
  title =	 "Explicit Polymorphism and {CPS} Conversion",
  booktitle =	 o20 # " " # popl,
  month =	 jan,
  year =	 1993,
  pages =	 "206--219",
}

@inproceedings{harper+:ita,
  author =	 "Robert Harper and Greg Morrisett",
  title =	 "Compiling Polymorphism Using Intensional Type
                  Analysis",
  pages =	 "130--141",
  booktitle =	 o22 # " " # popl,
  address =	 "San Francisco",
  month =	 jan,
  year =	 1995,
}

@article{harper+:lf,
  author =	 "Robert Harper and Furio Honsell and Gordon Plotkin",
  title =	 "A Framework for Defining Logics",
  journal =	 jacm,
  volume =	 40,
  number =	 1,
  month =	 jan,
  year =	 93,
  pages =	 "143--184",
}

@inproceedings{harper+:phase,
  author =	 "Robert Harper and John C. Mitchell and Eugenio
                  Moggi",
  title =	 "Higher-Order Modules and the Phase Distinction",
  booktitle =	 o17 # " " # popl,
  address =	 "San Francisco",
  month =	 jan,
  year =	 1990,
  pages =	 "341--354"
}

@inproceedings{harper+:translucent,
  author =	 "Robert Harper and Mark Lillibridge",
  title =	 "A Type-Theoretic Approach to Higher-Order Modules
                  with Sharing",
  booktitle =	 o21 # " " # popl,
  month =	 jan,
  year =	 1994,
  address =	 "Portland, Oregon",
  pages =	 "123--137",
}

@incollection{harper+:tt-interp-sml,
  author =	 "Robert Harper and Chris Stone",
  title =	 "A Type-Theoretic Interpretation of {Standard} {ML}",
  booktitle =	 "Proof, Language and Interaction: Essays in Honour of
                  Robin Milner",
  year =	 1998,
  publisher =	 mit-press,
  note =	 "Extended version published as CMU technical report
                  CMU-CS-97-147.",
}

@techreport{harper+:tt-interp-sml-tr,
  author =	 "Robert Harper and Chris Stone",
  title =	 "An Interpretation of {Standard} {ML} in Type Theory",
  institution =	 cmu-cs,
  year =	 1997,
  month =	 jun,
  number =	 "CMU-CS-97-147",
}

@article{harper+:type-structure-sml,
  author =	 "Robert Harper and John C. Mitchell",
  title =	 "On the Type Structure of {Standard ML}",
  journal =	 toplas,
  year =	 1993,
  volume =	 15,
  number =	 2,
  pages =	 "211--252",
  month =	 apr,
}

@article{harper+:typecheck-univ,
  author =	 "Robert Harper and Robert Pollack",
  title =	 "Type Checking with Universes",
  journal =	 tcs,
  volume =	 89,
  year =	 1991,
  pages =	 "107--136",
}

@inproceedings{harper+:typical-ambiguity,
  author =	 "Robert Harper and Robert Pollack",
  title =	 "Type Checking, Universe Polymorphism, and Typical
                  Ambiguity in the Calculus of Constructions",
  booktitle =	 "Proceedings of the International Joint Conference on
                  Theory and Practice of Software Development",
  address =	 "Barcelona",
  year =	 1989,
  month =	 mar,
  series =	 lncs,
  volume =	 352,
  publisher =	 springer,
}

@article{harper:types-over-op-semant,
  author =	 "Robert Harper",
  title =	 "Constructing Type Systems over an Operational
                  Semantics",
  journal =	 "Journal of Symbolic Computation",
  year =	 1992,
  volume =	 14,
  pages =	 "71--84",
}



@inproceedings{harper:tdtt,
  author = "Daniel R. Licata and Robert Harper",
  title  = "2-Dimensional {Directed} {Type} {Theory}",
  year   = 2011, 
  booktitle = "MFPS XXVII: Mathematical Foundations of Programming Semantics"
}


@Unpublished{harper:notes,
  author = 	 {Robert Harper},
  title = 	 {Programming Languages: Theory and Practice},
  note = 	 {Unpublished, draft available at \url{http://www.cs.cmu.edu/~rwh/plbook/}},
  year =	 2001
}



@Article{hosoya+:xduce,
  author = 	 {Haruo Hosoya and Benjamin C. Pierce},
  title = 	 {Regular expression pattern matching for {XML}},
  journal = 	 jfp,
  year = 	 2002,
  volume =	 13,
  number =	 4
}

@TechReport{peterson+:tilt,
  author = 		  {Leaf Petersen and Perry Cheng and Robert Harper and Chris Stone},
  title = 		  {Implementing the {TILT} Internal Language},
  institution =  { Carnegie Mellon University Computer Science},
  year = 		  2000,
  number =		  {CMU-CS-00-180},
  month =		  dec
}

@unpublished{hickey:tt-obj-semant,
  author =	 "Jason J. Hickey",
  title =	 "A Semantics of Objects in Type Theory",
  note =	 "Unpublished manuscript",
  year =	 1997,
}

@inproceedings{hickey:very-dependent-type,
  author =	 "Jason J. Hickey",
  title =	 "Formal Objects in Type Theory Using Very Dependent
                  Types",
  booktitle =	 "Foundations of Object Oriented Languages 3",
  year =	 1996,
}



@Article{hinze:polytypic-journal,
  author = 		  {Ralf Hinze},
  title = 		  {Polytypic values possess polykinded types},
  journal = 	  {Science of Computer Programming},
  year = 		  2002,
  volume =		  43,
  number =       {2--3},
  pages =		  {129--159},
  note =			  {MPC Special Issue}
}

@InProceedings{hinze:polytypic,
  author = 	 {Ralf Hinze},
  title = 	 {Polytypic values possess polykinded types},
  booktitle = 	 {Proceedings of the Fifth
     International Conference on Mathematics of Program Construction (MPC 2000)},
  year =	 2000,
  editor =	 {Roland Backhouse and J.N. Oliveira},
  address =	 {Ponte de Lima, Portugal},
  month =	 jul,
  pages = "2--27"
}

@Incollection{hinze+:derivable,
  author = 	 {Ralf Hinze and Simon {Peyton Jones}},
  title = 	 {Derivable Type Classes},
  booktitle = 	 { Proceedings of the Fourth {H}askell Workshop, Montreal,
     Canada, September 17, 2000},
  year =	 2000,
  editor =	 {Graham Hutton},
  series = { Electronic Notes in Theoretical Computer Science},
  publisher = { Elsevier Science},
  volume = {41.1},
  month = aug,
  annotation = {no page number.}
}


@InProceedings{hinze+:type-indexed-datatypes,
  author = 		  {Ralf Hinze and Johan Jeuring and Andres L\"oh},
  title = 		  {Type-indexed data types},
  booktitle = 	  {Proceedings of the Sixth International Conference on Mathematics 
                  of Program Construction (MPC 2002)},
  year =			  2002,
  editor =		  {Eerke Boiten, Bernhard M\"oller},
  address =		  { Dagstuhl, Germany },
  month =		  jul,
  pages =        {148--174}
}


@article{luo:coercions,
  author    = {Zhaohui Luo},
  title     = {Coercions in a polymorphic type system},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {18},
  number    = {4},
  year      = {2008},
  pages     = {729-751},
  ee        = {http://dx.doi.org/10.1017/S0960129508006804},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{chakravarty+:accelerate,
 author = {Chakravarty, Manuel M.T. and Keller, Gabriele and Lee, Sean and McDonell, Trevor L. and Grover, Vinod},
 title = {Accelerating {Haskell} array codes with multicore {GPU}s},
 booktitle = {Proceedings of the sixth workshop on {Declarative} {Aspects} of {Multicore} {Programming}},
 series = {DAMP '11},
 year = {2011},
 isbn = {978-1-4503-0486-3},
 location = {Austin, Texas, USA},
 pages = {3--14},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {arrays, data parallelism, dynamic compilation, gpgpu, haskell, skeletons},
} 



@article{henglein:coercions,
 author = {Henglein, Fritz},
 title = {Dynamic typing: syntax and proof theory},
 journal = {Sci. Comput. Program.},
 volume = {22},
 issue = {3},
 month = {June},
 year = {1994},
 issn = {0167-6423},
 pages = {197--230},
 numpages = {34},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
} 


@INPROCEEDINGS{HicksMN01a,
  AUTHOR = {Michael Hicks and Jonathan T. Moore and Scott Nettles},
  BOOKTITLE = {Proceedings of the {ACM SIGPLAN} Conference on Programming 
Language Design and Implementation},
  TITLE = {Dynamic Software Updating},
  MONTH = {June},
  YEAR = 2001,
  PAGES = {13--23},
  PUBLISHER = {{ACM}},
  ABSTRACT = {
Many important applications must run continuously and without interruption,
yet must be changed to fix bugs or upgrade functionality.  No
prior general-purpose methodology for dynamic updating achieves a practical
balance between flexibility, robustness, low overhead, and ease of use.

We present a new approach for C-like languages that provides type-safe
dynamic updating of native code in an extremely flexible manner (code, data,
and types may be updated, at programmer-determined times) and permits the
use of automated tools to aid the programmer in the updating process.  Our
system is based on \emph{dynamic patches} that both contain the updated code
and the code needed to transition from the old version to the new.  A novel
aspect of our patches is that they consist of \emph{verifiable native code}
(\emph{e.g.} Proof-Carrying Code~\cite{necula:pcc} or Typed Assembly
Language~\cite{morrisett+:tal}), which is native code accompanied by
annotations that allow on-line verification of the code's safety.  We
discuss how patches are generated mostly automatically, how they are applied
using dynamic-linking technology, and how code is compiled to make it
updateable.

To concretely illustrate our system, we have implemented a
dynamically-updateable web server, FlashEd.  We discuss our experience
building and maintaining FlashEd.  Performance experiments show that for
FlashEd, the overhead due to updating is typically less than 1 percent.
},
  URL = {http://www.cis.upenn.edu/~mwh/papers/dyn_update.ps}
}


@PHDTHESIS{Hicks01,
  AUTHOR = {Michael Hicks},
  TITLE = {Dynamic Software Updating},
  YEAR = 2001,
  MONTH = {August},
  SCHOOL = {Department of Computer and Information Science, University of Pennsylvania},
  URL = {http://www.cis.upenn.edu/~mwh/papers/thesis.pdf}
}


@InProceedings{hicks98:_plan,
  author =	 {M. Hicks and P. Kakkar and J. Moore and C. Gunter
                  and S. Nettles},
  title =	 {{PLAN:} A Programming Language for Active Networks},
  booktitle =	 o3 # " " # icfp,
  pages =	 "86--93",
  year =	 1998
}

@article{hoffman+:unifying-objects,
  author =	 "Martin Hofmann and Benjamin Pierce",
  title =	 "A Unifying Type-Theoretic Framework for Objects",
  journal =	 jfp,
  year =	 1995,
  month =	 oct,
  volume =	 5,
  number =	 4,
  pages =	 "593--635"
}

@InProceedings{hofmann00esop,
  author =	 {Martin Hofmann},
  title =	 {A Type System for Bounded Space and Functional
                  in-place update},
  booktitle =	 esop,
  year =	 2000
}

@InProceedings{hofmann99lics,
  author =	 {Martin Hofmann},
  title =	 {Linear Types and non-size increasing polynomial
                  computation},
  booktitle =	 lics,
  year =	 1999,
  address =	 {Trento, Italy},
  month =	 jul
}

@MISC{HotJava,
  KEY = {hotjava},
  TITLE = {HotJava Browser},
  NOTE = {\url{http://java.sun.com/products/hotjava/index.html}}
}


@techreport{hook+:impred-strong-sum,
  author =	 "James G. Hook and Douglas J. Howe",
  title =	 "Impredicative Strong Existential Equivalent to
                  Type:Type",
  institution =	 cornell-cs,
  year =	 1986,
  month =	 jun,
  number =	 "TR 86-760",
}

@incollection{hook:understanding-russell,
  author =	 "James G. Hook",
  title =	 "Understanding {Russell}---A First Attempt",
  booktitle =	 "Semantics of Data Types",
  series =	 lncs,
  volume =	 173,
  publisher =	 springer,
  year =	 1984,
}

@InProceedings{hornof99rtcg,
  author = 	 {Luc Hornof and Trevor Jim},
  title = 	 {Certifying compilation and run-time code generation},
  booktitle = 	 pepm,
  year =	 1999,
  month =	 jan
}

@incollection{howard:formulas-as-types,
  author =	 "W. Howard",
  title =	 "The Formulas-as-Types Notion of Construction",
  booktitle =	 "To {H.B.} {Curry}: Essays on Combinatory Logic,
                  Lambda-Calculus and Formalism",
  editor =	 "J. P. Seldin and J. R. Hindley",
  pages =	 "479--490",
  publisher =	 "Academic Press",
  year =	 1980,
}

@InBook{howard73logical,
  author = 		  {W. Howard},
  chapter = 		  {Hereditarily majorizable functionals},
  title = 	  {Mathematical Investigation of Intuistionistic Arithmetic and Analysis},
  year = 		  1973,
  number =		  {LNM},
  pages =		  {454--461},
 address =		  {Berlin},
  publisher =   {Springer}
}

@techreport{howe:embedding-hol-in-nuprl,
  author =	 "Douglas J. Howe",
  title =	 "Semantic Foundations for Embedding {HOL} in {Nuprl}",
  institution =	 "Bell Labs",
  year =	 1996,
}

@inproceedings{howe:girard-paradox,
  author =	 "Douglas J. Howe",
  title =	 "The Computational Behaviour of {G}irard's Paradox",
  booktitle =	 o2 # " " # lics,
  year =	 1987,
  month =	 jun,
  pages =	 "205--214",
  address =	 ith-ny,
}

@inproceedings{howe:squiggle-eq,
  author =	 "Douglas J. Howe",
  title =	 "Equality in Lazy Computation Systems",
  booktitle =	 o4 # " " # lics,
  year =	 1989,
}


@article{hudak+:haskell,
  author =	 "Paul Hudak and Simon {Peyton Jones} and Philip
                  Wadler",
  title =	 "Report on the Programming Language {Haskell},
                  version 1.2",
  journal =	 "SIGPLAN Notices",
  volume =	 27,
  number =	 5,
  year =	 1992,
  month =	 may,
}


@InProceedings{hughes96:_provin_correc_react_system_using_sized_types,
  author =	 {John Hughes and Lars Pareto and Amr Sabry},
  title =	 {Proving the Correctness of Reactive Systems Using
                  Sized Types},
  booktitle =	 o23 # " " # popl,
  year =	 1996,
  pages =	 "410--423",
  month =	 jan
}

@Manual{hugs,
  title = 		  {Hugs 98 : A functional programming system based on {H}askell 98 : User Manual},
  author =		  {Mark P Jones and Alastair Reid},
  organization = {Yale Haskell Group and Oregon Graduate Institute of Science and Technology},
  note =			  {Available at \url{http://cvs.haskell.org/Hugs/downloads/hugs.pdf}},
  month = sep,
  year = 1999
}

@InProceedings{hurkens:paradox,
  author =       {Antonious J. C. Hurkens },
  title = 	 {A simplification of {Girard's} Paradox},
  year = 	 1995,
  booktitle =    "Second International Conference on Typed Lambda Calculi and Applications, TLCA '95",
  editor =	 {Mariangiola Dezani-Ciancaglini and Gordon Plotkin},
  volume =	 902,
  series =	 lncs,
  address =	 {Edinburgh, United Kingdom},
  month =	 apr,
  publisher =	 springer,
  pages = {266--278}
}

%% I %%
@techreport{igarashi:admissibility,
  author =	 "Shigeru Igarashi",
  title =	 "Admissibility of Fixed-Point Induction in
                  First-Order Logic of Typed Theories",
  institution =	 "Computer Science Department, Stanford University",
  year =	 1972,
  month =	 may,
  number =	 "AIM-168",
}
%% J %%
@manual{jackson:nuprl-manual,
  title =	 "The {N}uprl Proof Development System, Version 4.1",
  author =	 "Paul Jackson",
  organization = cornell-cs,
  webnote =	 "Available at
                  http://www.cs.cornell.edu/Info/Projects/NuPrl/html/nuprldocs.html",
  year =	 1994,
}

@phdthesis{jackson:phd,
  author =	 "Paul Bernard Jackson",
  title =	 "Enhancing the Nuprl Proof Development System and
                  Applying it to Computational Abstract Algebra",
  school =	 cornell-cs,
  month =	 jan,
  year =	 1995,
  address =	 ith-ny,
}


@PhdThesis{jansson:phd,
  author = 	 {Patrik Jansson},
  title = 	 {Functional Polytypic Programming},
  school = 	 {Chalmers University of Technology and Goteborg University},
  year = 	 2000
}

@InProceedings{jansson97polyp,
  author = 	 {Patrick Jansson and Johan Jeuring},
  title = 	 {{PolyP}---{A} Polytypic Programming Language Extension},
  booktitle = 	 o24 # " " # popl,
  pages =	 {470--482},
  year =	 1997,
  address =	 {Paris, France}
}

@InProceedings{janssonjeuringWGP00:rewriting,
  author =   {Jansson, Patrik and Jeuring, Johan},
  title =    {A Framework for Polytypic Programming on Terms, with
                  an Application to Rewriting},
  booktitle =    "Workshop on Generic Programming (WGP2000), 
                   Ponte de Lima, Portugal",
  publisher =    "Utrecht University",
  note =     "Technical Report UU-CS-2000-19",
  year =     2000
}


@InProceedings{jansson+:polytypic-compression,
  author = 		  {Patrik Jansson and Johan Jeuring},
  title = 		  {Polytypic Compact Printing and Parsing},
  booktitle = 	  esop,
  pages =		  {273-287},
  year =			  1999,
  volume =		  1576,
  series =		  lncs
}

@Article{jansson+:polytypic-unification,
  author = 		  {Patrik Jansson and Johan Jeuring},
  title = 		  {Functional Pearl: Polytypic Unification},
  journal = 	  jfp,
  year = 		  1998,
  volume =		  8,
  number =		  5,
  month =		  sep,
  pages = {527--536}
}

@article{jategaonkar+:ext-pattern-subtypes,
  author =	 "Lalita A. Jategaonkar and John C. Mitchell",
  title =	 "Type Inference with Extended Pattern Matching and
                  Subtypes",
  journal =	 "Fundamenta Informaticae",
  year =	 1993,
  volume =	 19,
  pages =	 "127--166",
  note =	 "{\it Preliminary version appeared in 1988 {ACM}
                  Conference on Lisp and Functional Programming}",
}



@Misc{JavaBeans,
  key =			  {JavaBeans},
  title =		  {{JavaBeans}: The Only Component for {Java} Technology},
  month =		  may,
  year =			  2002,
  note =			  {\url{http://java.sun.com/products/javabeans/}}
}

@MISC{JavaClassloading96,
  KEY = {javaclass},
  TITLE = {Basics of Java class loaders},
  YEAR = {1996},
  NOTE = {\url{http://www.javaworld.com/javaworld/jw-10-1996/jw-10-indepth.html}}
}


@Article{jay+:fml,
  author = 	 {C. Barry Jay and Gianna Bell\`{e} and Eugenio Moggi},
  title = 	 {Functorial {ML} },
  journal = 	 jfp,
  year = 	 1998,
  volume =	 8,
  number =	 6,
  pages =	 {573--619},
  month =	 nov
}

@article{ jay95semantics,
    author = "C. Barry Jay",
    title = "A Semantics for Shape",
    journal = "Science of Computer Programming",
    volume = "25",
    number = "2--3",
    pages = "251--283",
    year = "1995",
    url = "citeseer.nj.nec.com/71598.html" }

@Article{jay:fish,
  author = 		  {C.B. Jay},
  title = 		  {Programming in {FISh} },
  journal = 	  {International Journal on Software Tools for Technology Transfer},
  year = 		  1999,
  volume =		  2,
  pages =		  {307--315}
}

@unpublished{ jim99type,
    author = "Trevor Jim and Jens Palsberg",
    title = "Type inference in systems of recursive types with subtyping",
    year = "1999",
    note   = { Available at \url{citeseer.nj.nec.com/jim97type.html}}
}




@Article{johann:short-cut,
  author = 		  {Patricia Johann},
  title = 		  {A Generalization of Short-Cut Fution and its Correctness Proof},
  journal = 	  hosc,
  year = 		  2002,
  volume =		  15,
  pages =		  {273--300}
}

@techreport{jones:gofer-impl,
  author =	 "Mark P. Jones",
  title =	 "The Implementation of the {G}ofer Functional
                  Programming System",
  institution =	 yale-cs,
  year =	 1994,
  month =	 may,
  type =	 "Research Report",
  number =	 "YALEU/DCS/RR-1030",
}


@phdthesis{jones:phd,
  author =	 "Mark P. Jones",
  title =	 "Qualified Types: Theory and Practice",
  school =	 "Oxford University Computing Laboratory",
  year =	 1992,
  month =	 jul,
}


@techreport{jones:qualified-type-coherence,
  author =	 "Mark P. Jones",
  title =	 "Coherence for Qualified Types",
  institution =	 yale-cs,
  year =	 1993,
  month =	 sep,
  type =	 "Research Report",
  number =	 "YALEU/DCS/RR-989",
}

@incollection{ jones:qualified-types,
    author = "Mark P. Jones",
    title = "A Theory of Qualified Types",
    booktitle = "{ESOP} '92, 4th European Symposium on Programming, Rennes, France, February 1992, Proceedings",
    volume = 582,
    publisher = "Springer-Verlag",
    address = "New York, N.Y.",
    editor = "Bernd Krieg-Bruckner",
    pages = "287--306",
    year = 1992,
    url = "citeseer.nj.nec.com/jones92theory.html" }


@Article{jones:ho-poly,
  author = 	 {Mark P. Jones},
  title = 	 {A system of constructor classes: overloading 
                  and implicit higher-order polymorphism },
  journal = 	 jfp,
  year = 	 1995,
  volume =	 5,
  number =	 1,
  month =	 jan
}


@InProceedings{jones:fundeps,
  author = 		  {Mark P. Jones},
  title = 		  {Type Classes with Functional Dependencies},
  booktitle =	  {Proceedings of the 9th European Symposium on Programming, ESOP 2000, Berlin, Germany},
  year =			  2000,
  number =		  1782,
  series =		  {LNCS},
  publisher =	  {Springer-Verlag}
}

@inproceedings{ jones97firstclass,
    author = "Mark P. Jones",
    title = "First-class Polymorphism with Type Inference",
    booktitle = "Conference Record of {POPL}~'97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages",
    month = "15--17",
    address = "Paris, France",
    pages = "483--496",
    year = "1997",
    url = "citeseer.nj.nec.com/451312.html" }


@inproceedings{jouvelot+:effects,
  author = "Pierre Jouvelot and D. K. Gifford",
  title = "Algebraic reconstruction of types and effects",
  booktitle = eighteenth # popl,
  year = 1991,
  month = jan,
  pages = "303--310"
}



@InProceedings{juering:polytypic-pattern,
  author = 		  {J. Jeuring},
  title = 		  { Polytypic pattern matching},
  booktitle = 	  "FPCA95: " # fpca,
  pages =		  {238--248},
  year =			  1995
}

%% K %%

@inproceedings{kamin:smalltalk-semantics,
  author =	 "Samuel Kamin",
  title =	 "Inheritance in {S}malltalk-80: A Denotational
                  Definition",
  booktitle =	 o15 # " " # popl,
  year =	 1988,
  month =	 jan,
  pages =	 "80--87",
  address =	 "San Diego",
}

@Article{r5rs,
  author = 		  {Richard Kelsey and William Clinger and Jonathan Rees, editors},
  title = 		  { {Revised$^5$} Report on the Algorithmic Language {S}cheme },
  journal = 	  {Higher-Order and Symbolic Computation},
  year = 		  1998,
  volume =		  11,
  number =		  1,
  month =		  sep,
  pages =        {7--105}
}

@inproceedings{kennedy:dimensions,
  author =	 "Andrew J. Kennedy",
  title =	 "Relational Parametricity and Units of Measure",
  booktitle =	 o24 # " " # popl,
  year =	 1997,
  month =	 jan,
  address =	 "Paris",
  pages =	 "442--455",
}

@InProceedings{kennedy+:c-sharp-generics,
  author = 		  {Andrew Kennedy and Don Syme},
  title = 		  {Design and Implementation of Generics for 
                   the {.NET} Common Language Runtime },
  booktitle =	  proc # 2001 # pldi,
  pages =		  {1--12},
  year =			  2001,
  address =		  {Snowbird, Utah, USA},
  month =		  jun
}



@Book{k&r,
  author =		  {Brian W. Kernighan and Dennis M. Ritchie},
  title = 		  {The C Programming Language, Second Edition},
  publisher = 	  {Prentice Hall, Inc.},
  year = 		  1988
}

@inproceedings{kieburtz:taming-effects,
  author =	 "Richard B. Kieburtz",
  title =	 "Taming Effects with Monadic Typing",
  booktitle =	 1998 # " " # icfp,
  year =	 1998,
  month =	 sep,
  address =	 "Baltimore",
  pages =	 "51--62",
}


@Incollection{kiczales:aop,
  author = 		  {Gregor Kiczales and John Lamping and Anurag Mendhekar and  
  Chris Maeda and
  Cristina Videira Lopes and Jean-Marc Loingtier and John Irwin},
  title = 		  {Aspect-Oriented Programming},
  booktitle = 	  { Proceedings of the European Conference on Object-Oriented
  Programming (ECOOP)},
  year =			  1997,
  volume =		  1241,
  series =		  lncs,
  month =		  jun,
  editor = "Mehmet Ak\c{s}it and Satoshi Matsuoka",
  pages = "220--242",
  publisher =	  {Springer-Verlag}
}

@InProceedings{kim99impacts,
  author =	 {Sung-Kwan Kim and Rhan Ha and Sang Lyul Min},
  title =	 {Analysis of the Impacts of Overestimation Sources on
                  the Accuracy of Worst Case Timing Analysis},
  booktitle =	 {IEEE Real-Time Systems Symposium},
  pages =	 {22--31},
  year =	 1999,
  address =	 {Phoeniz, AZ},
  month =	 {December},
  organization = {IEEE Computer Society}
}

@inproceedings{kranz+:orbit,
  author =	 "David Kranz and R. Kelsey and J. Rees and
                  P. R. Hudak and J. Philbin and N. Adams",
  title =	 "{ORBIT}: An Optimizing Compiler for {S}cheme",
  booktitle =	 "Proceedings of the {ACM SIGPLAN} '86 Symposium on
                  Compiler Construction",
  year =	 1986,
  month =	 jun,
  pages =	 "219--233",
}

@techreport{kreitz:embedding,
  author =	 "Christoph Kreitz",
  title =	 "Formal Reasoning about Communications Systems {I}",
  institution =	 cornell-cs,
  year =	 1997,
}

@inproceedings{ krishnamurthi+:extensible-visitor,
    author = "Shriram Krishnamurthi and Matthias Felleisen and Daniel P. Friedman",
    title = "Synthesizing Object-Oriented and Functional Design to Promote Re-use",
    booktitle = "European Conference on Object Oriented Programming",
    pages = "91--113",
    year = "1998",
    url = "citeseer.nj.nec.com/krishnamurthi98synthesizing.html" }

@TechReport{Kozen98,
  author = 	 {Dexter Kozen},
  title = 	 {Efficient Code Certification},
  institution =  {Department of Computer Science, Cornell University},
  year = 	 1998,
  number =	 {98-1661},
  address =	 {Ithaca, NY 12853-7501},
  month =	 {January}
}

@inproceedings{ kozen93efficient,
    author = "Dexter Kozen and Jens Palsberg and Michael I. Schwartzbach",
    title = "Efficient Recursive Subtyping",
    booktitle = "Conference Record of the Twentieth Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages",
    address = "Charleston, South Carolina",
    pages = "419--428",
    year = "1993",
    url = "citeseer.nj.nec.com/article/kozen95efficient.html" }


%% L %%



@TechReport{lampson:cedar,
  author = 		  {Butler Lampson},
  title = 		  {A description of the {C}edar language},
  institution =  {Xerox Palo Alto Research Center},
  year = 		  1983,
  number =		  {CSL-83-15}
}

@article{landin:closure,
  author =	 "P. J. Landin",
  title =	 "The mechanical evaluation of expressions",
  journal =	 "Computer J.",
  volume =	 6,
  number =	 4,
  pages =	 "308--320",
  year =	 1964,
}

@article{launchbury+:haskell-state,
  author =	 "John Launchbury and Simon {Peyton Jones}",
  title =	 "State in {Haskell}",
  journal =	 "Lisp and Symbolic Computation",
  volume =	 8,
  number =	 4,
  month =	 dec,
  year =	 1995,
  pages =	 "293--341",
}

@inproceedings{launchbury+:param-unbox,
  author =	 "John Launchbury and Ross Paterson",
  title =	 "Parametricity and Unboxing with Unpointed Types",
  booktitle =	 o6 # " " # esop,
  year =	 1996,
  month =	 apr,
  address =	 "{Link\"{o}ping}, Sweden",
  pages =	 "204--218",
  series =	 lncs,
  volume =	 1058,
  publisher =	 springer,
}


@inproceedings{ lebotlan-remy:mlf-icfp,
  author = {Le Botlan, Didier  and Remy, Didier}, 
  title = "{MLF}: Raising {ML} to the Power of {S}ystem-{F}",
  booktitle = {Proceedings of the International Conference on Functional Programming ({ICFP} 2003), Uppsala, Sweden}, 
  year = {2003},
  publisher = {ACM Press},
  pages = {27--38},
  month = {aug},
  pdf= {http://pauillac.inria.fr/~remy/work/mlf/icfp.pdf},
  html= {http://pauillac.inria.fr/~remy/work/mlf/},
  url = {citeseer.nj.nec.com/564799.html} 
}

@inproceedings{leroy:applicative-functors,
  author =	 "Xavier Leroy",
  title =	 "Applicative Functors and Fully Transparent
                  Higher-Order Modules",
  booktitle =	 o22 # " " # popl,
  year =	 1995,
  month =	 jan,
  address =	 "San Francisco",
}

@inproceedings{leroy:manifest,
  author =	 "Xavier Leroy",
  title =	 "Manifest Types, Modules and Separate Compilation",
  booktitle =	 o21 # " " # popl,
  year =	 1994,
  month =	 jan,
  address =	 "Portland, Oregon",
  pages =	 "109--122",
}

@manual{leroy:ocaml-manual,
  title =	 "The {O}bjective {C}aml System, Release 1.00",
  author =	 "Xavier Leroy",
  year =	 1996,
  organization = inria,
  webnote =	 "Available at http://pauillac.inria.fr/ocaml",
}

@inproceedings{leroy:unbox,
  author =	 "Xavier Leroy",
  title =	 "Unboxed objects and polymorphic typing",
  booktitle =	 o19 # " " # popl,
  year =	 1992,
  pages =	 "177-188",
}

@inproceedings{leroy:unbox-effectiveness,
  author =	 "Xavier Leroy",
  title =	 "The Effectiveness of Type-Based Unboxing",
  booktitle =	 tic,
  year =	 1997,
  month =	 jun,
  address =	 "Amsterdam",
  organization = "{ACM SIGPLAN}",
  note =	 "Published as {B}oston {C}ollege Computer Science
                  Department Technical Report BCCS-97-03",
}



@Article{leroy+:exceptions,
  author = 	 {Xavier Leroy and F. Pessaux},
  title = 	 {Type-based analysis of uncaught exceptions},
  journal = 	 toplas,
  year = 	 2000,
  volume =	 22,
  number =	 2,
  pages =	 {340--377}
}

@incollection{ leroy91dynamics,
    author = "Xavier Leroy and Michel Mauny",
    title = "Dynamics in {ML}",
    booktitle = "Functional Programming Languages and Computer Architecture, 5th {ACM} Conference",
    volume = "523",
    publisher = "Springer-Verlag",
    address = "Berlin, Heidelberg, New York",
    editor = "J. Hughes",
    pages = "406--426",
    year = "1991",
    url = "citeseer.nj.nec.com/313297.html" }


@InProceedings{leroy+:dynamics,
  author = 		  {Xavier Leroy and Michel Mauny},
  title = 		  {Dynamics in {ML}},
  booktitle = 	   {Functional Programming Languages and Computer Architecture},
  pages =		  {406-426},
  year =			  1991,
  editor =	 {J. Hughes},
  number =	 523,
  series =	 {Lecture Notes in Computer Science},
  month =	 aug,
  publisher =	 {Springer-Verlag}

}

@string{popl00="Proceedings of the 27th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, Boston, Massachusetts"}

@inproceedings{lewis+:implicit-params
,author="Jeffrey Lewis and Mark Shields and Erik Meijer and John Launchbury"
,title="Implicit Parameters: Dynamic Scoping with Static Types"
,booktitle=popl00
,year="2000"
,month="Jan"
,pages="108--118"
}

@InProceedings{liedke+97:webos,
  author =	 {Jochen Liedtke and Nyeem Islam and Trent Jaeger},
  title =	 {Preventing Denial-of-Service Attacks on a
                  $\mu$-Kernel for web {OS}es},
  booktitle =	 o6 # " " # hotos,
  year =	 1997
}

@article{liedtke95:cheap_time,
  author =	 {Jochen Liedtke},
  title =	 {A Short Note on Cheap Fine-grained Time Measurement},
  journal =	 {ACM Operating Systems Review},
  pages =	 {31--34},
  year =	 95,
  volume =	 29,
  number =	 3,
  month =	 {July}
}

@phdthesis{lillibridge:phd,
  author =	 "Mark Lillibridge",
  title =	 "Translucent Sums: A Foundation for Higher-Order
                  Module Systems",
  year =	 1997,
  month =	 may,
  address =	 pgh-pa,
  school =	 cmu-cs,
}



@InProceedings{lim94risc,
  author = 	 {Sung-Soo Lim and Young Hyun Bae and Gyu Tae Jang and Byung-Do Rhee
 and Sang Lyul Min and Chang Yun Park and Heonshik Shin and Kunsoo Park and Chong Sang Kim},
  title = 	 {An Accurate Worts Case Timing Analysis Technique for {RISC} Processors},
  booktitle = 	 o15 # " " # rtss,
  pages =	 {97--108},
  year =	 1994
}

@book{lindholm+:jvm,
  title =	 "The {Java} Virtual Machine Specification",
  author =	 "Tim Lindholm and Frank Yellin",
  publisher =	 addison,
  year =	 1996,
}


@MISC{LinuxDynlink95,
  KEY = {DLOPEN},
  TITLE = {{DLOPEN}(3)},
  howpublished = {{L}inux {P}rogrammer's {M}anual},
  MONTH = {December},
  YEAR = {1995}
}



@inproceedings{ liu98automatic,
  author =	 "Yanhong Liu and Gustavo Gomez",
  title =	 "Automatic accurate time-bound analysis for
                  high-level languages",
  booktitle =	 lctes,
  publisher =	 springer,
  month =	 jun,
  series =	 lncs,
  volume =	 1474,
  year =	 1998
}

@techreport{lucassen+:fx,
  author =	 "J. M. Lucassen and D. K. Gifford and P. Jouvelot and
                  M. A. Sheldon",
  title =	 "{FX-87} Reference Manual",
  institution =	 "MIT Laboratory for Computer Science",
  number =	 "MIT/LCS/TR-407",
  month =	 sep,
  year =	 1987,
}

@InCollection{lundqvist98integrating,
  author =	 {T. Lundqvist and P. Stenstrom},
  title =	 {Integrating path and timing analysis using
                  instruction-level simulation techniques},
  booktitle =	 lctes,
  pages =	 {1--15},
  publisher =	 springer,
  year =	 1998,
  editor =	 {Frank Mueller and Azer Bestavros},
  number =	 1474,
  series =	 lncs
}

%% M %%

@inproceedings{ma+:parametric-poly2,
  author =	 "QingMing Ma and John C. Reynolds",
  title =	 "Types, Abstraction, and Parametric Polymorphism,
                  Part 2",
  booktitle =	 o7 # " " # mfps,
  year =	 1991,
  month =	 mar,
  address =	 "Pittsburgh, Pennsylvania",
  series =	 lncs,
  volume =	 598,
  publisher =	 springer,
  pages =	 "1--40",
}

@inproceedings{ma:parametricity,
  author =	 "QingMing Ma",
  title =	 "Parametricity as Subtyping",
  booktitle =	 o19 # " " # popl,
  year =	 1992,
  month =	 jan,
  address =	 "Albuquerque, New Mexico",
  pages =	 "281--292",
}

@inproceedings{macqueen+:semantics-ho-functors,
  author =	 "David B. MacQueen and Mads Tofte",
  title =	 "A Semantics for Higher-order Functors",
  booktitle =	 o5 # " " # esop,
  year =	 1994,
  series =	 lncs,
  volume =	 788,
  publisher =	 springer,
  pages =	 "409--423",
}

@inproceedings{macqueen:modular-struct,
  author =	 "David MacQueen",
  title =	 "Using Dependent Types to Express Modular Structure",
  booktitle =	 o13 # " " # popl,
  year =	 1986,
  month =	 jan,
  pages =	 "277--286",
  address =	 "St.\ Petersburg Beach, Florida",
}

@inproceedings{maqueen:modules,
  author =	 "David MacQueen",
  title =	 "Modules for {Standard} {ML}",
  booktitle =	 1984 # " " # lfp,
  year =	 1984,
  month =	 aug,
  address =	 "Austin, Texas",
  pages =	 "198--207",
}

@InProceedings{maes:reflection,
  author = 		  {Pattie Maes},
  title = 		  {Concepts and experiments in computational reflection},
  booktitle = 	  {Proceedings of the 2nd Annual Conference on Object-Oriented Programming
Systems, Languages and Applications (OOPSLA '87), (Orlando,
FL)},
  pages =		  {147--155},
  year =			  1987,
  month =		  oct
}

@inproceedings{martin-lof:constructive-math-and-programming,
  author =	 "Per Martin-L{\"{o}}f",
  title =	 "Constructive Mathematics and Computer Programming",
  booktitle =	 "Sixth International Congress of Logic, Methodology
                  and Philosophy of Science",
  pages =	 "153--175",
  publisher =	 noholland,
  year =	 1982,
  series =	 "Studies in Logic and the Foundations of Mathematics",
  volume =	 104,
}

@inproceedings{martin-lof:intuitionistic-types-pred,
  author =	 "Per Martin-L{\"{o}f}",
  title =	 "An Intuitionistic Theory of Types: Predicative Part",
  booktitle =	 "Proceedings of the Logic Colloquium, 1973",
  pages =	 "73--118",
  publisher =	 noholland,
  year =	 1975,
  series =	 "Studies in Logic and the Foundations of Mathematics",
  volume =	 80,
}



@article{meertens:paramorphisms,
  author = 	 {Lambert G. L. T. Meertens},
  title = 	 {Paramorphisms},
  journal = 	 {Formal Aspects of Computing},
  pages =	 {413--424},
  year =	 1992,
  volume =	 4,
  number =	 5,
  publisher =	 springer
}

@inproceedings{mmf91m
,author="Erik Meijer and Fokkinga, Maarten M. and Ross Paterson"
,title="Functional Programming with Bananas, Lenses, Envelopes and
  Barbed Wire"
,booktitle="FPCA91: " # fpca
,pages="124--144"
,year=1991

}
% ,volume=523
% ,series=lncs
% ,publisher=springer

@inproceedings{ meijer95bananas,
    author = "Erik Meijer and Graham Hutton",
    title = "Bananas in Space: Extending Fold and Unfold to Exponential Types",
    booktitle = "FPCA95: " # fpca,
    month = jun,
    address = "La Jolla, CA",
    pages = "324--333",
    year = 1995,
    url = "citeseer.nj.nec.com/293490.html"
}

@article{mendler:inductive-types,
  author =	 "Nax Paul Mendler",
  title =	 "Inductive Types and Type Constraints in the
                  Second-Order Lambda Calculus",
  journal =	 "Annals of Pure and Applied Logic",
  year =	 1991,
  volume =	 51,
  number =	 "1--2",
  pages =	 "159--172",
}

@phdthesis{mendler:phd,
  author =	 "Paul Francis Mendler",
  title =	 "Inductive Definition in Type Theory",
  school =	 cornell-cs,
  month =	 sep,
  year =	 1987,
  address =	 ith-ny,
}

@inproceedings{meyer+:type-not-type,
  author =	 "Albert R. Meyer and Mark B. Reinhold",
  title =	 "`{T}ype' is Not a Type",
  booktitle =	 o13 # " " # popl,
  year =	 1986,
  month =	 jan,
  pages =	 "287--295",
  address =	 "St. Petersburg Beach, Florida",
}

@InProceedings{millen92,
  author =	 {J. K. Millen},
  title =	 {A Resource Allocation Model for Denial of Service},
  booktitle =	 ieeesp,
  pages =	 {137--147},
  year =	 1992,
  address =	 {Oakland, CA},
  month =	 {May},
  publisher =	 {IEEE Computer Society Press}
}

@InCollection{millen95,
  author =	 {Jonathan K. Millen},
  title =	 {Denial of Service: A Perspective},
  booktitle =	 {Dependable Computing for Critical Applications 4},
  publisher =	 springer,
  year =	 1995,
  editor =	 {F. Cristian and G. {Le Lann} and T. Lunt},
  volume =	 9,
  series =	 {Dependable Computing and Fault Tolerant Systems},
  address =	 {Wien, Austria}
}

@book{milner+:sml,
  title =	 "The Definition of {S}tandard {ML}",
  author =	 "Robin Milner and Mads Tofte and Robert Harper",
  publisher =	 mit-press,
  address =	 cam-ma,
  year =	 1990,
}

@book{milner+:sml-comment,
  title =	 "Commentary on {S}tandard {ML}",
  author =	 "Robin Milner and Mads Tofte",
  publisher =	 mit-press,
  address =	 cam-ma,
  year =	 1991,
}

@book{milner+:sml97,
  title =	 "The Definition of {Standard} {ML} (Revised)",
  author =	 "Robin Milner and Mads Tofte and Robert Harper and
                  David MacQueen",
  publisher =	 mit-press,
  address =	 cam-ma,
  year =	 1997,
}


@Article{milner:alg-w,
  author = 		  {Robin Milner},
  title = 		  {A Theory of Type Polymorphism in Programming},
  journal = 	  {Journal of Computer and System Sciences },
  year = 		  1978,
  volume =		  17,
  number =		  3,
  pages =		  {348--375}
}
 

@InProceedings{millstein+:eml,
  author = 	 {Todd Millstein and Colin Bleckner and Craig Chambers},
  title = 	 {Modular Typechecking for Hierarchically Extensible Datatypes and 
                  Functions},
  booktitle = 	 icfp,
  year =	 2002,
  address =	 {Pittsburgh, PA, USA},
  month =	 oct
}

@inproceedings{minamide+:typed-closure-conversion,
  author =	 "Yasuhiko Minamide and Greg Morrisett and Robert
                  Harper",
  title =	 "Typed Closure Conversion",
  pages =	 "271--283",
  booktitle =	 o23 # " " # popl,
  address =	 "St. Petersburg, Florida",
  month =	 jan,
  year =	 1996,
}

@unpublished{minamide:full-lift,
  author =	 "Yasuhiko Minamide",
  title =	 "Full Lifting of Type Parameters",
  note =	 "Submitted for publication. Earlier version published
                  as ``Compilation Based on a Calculus for Explicit
                  Type-Passing'' in the {\em Second Fuji International
                  Workshop on Functional and Logic Programming,\/}
                  1996.",
}


@InProceedings{minimide99space,
  author = 	 {Yasuhiko Minamide},
  title = 	 {Space-Profiling Semantics of the Call-by-Value Lambda Calculus 
 and the CPS transformation},
  booktitle = 	 o3 # " " # hoots,
  pages =	 {103--118},
  year =	 1999,
  volume =	 26,
  series =	 {Electronic Notes in Theoretical Computer Science},
  address =	 {http://www.elsevier.nl/locate/entcs},
  publisher =	 {Elsevier}
}

@book{mips,
  title =	 "{MIPS} {RISC} Architecture",
  author =	 "Gerry Kane and Joe Heinrich",
  publisher =	 "Prentice-Hall",
  year =	 1991,
}

@article{mitchell+:existential,
  author =	 "John C. Mitchell and Gordon D. Plotkin",
  title =	 "Abstract Types Have Existential Type",
  journal =	 toplas,
  year =	 1988,
  volume =	 10,
  number =	 3,
  month =	 jul,
  pages =	 "470--502",
}



@Book{mitchell:book,
  author =	 {John C. Mitchell},
  title = 	 {Foundations for Programming Languages},
  publisher = 	 mit-press,
  year = 	 1996
}

@article{moggi:computation-monad,
  author =	 "Eugenio Moggi",
  title =	 "Notions of Computation and Monads",
  journal =	 iandc,
  volume =	 93,
  year =	 1991,
  pages =	 "55-92",
}


@INPROCEEDINGS{moreau-Queinnec:DSL97,
  AUTHOR =	 {Luc Moreau and Christian Queinnec},
  TITLE =	 {{Design and Semantics of Quantum: a Language to
                  Control Resource Consumption in Distributed
                  Computing}},
  BOOKTITLE =	 {Usenix Conference on Domain-Specific Languages
                  (DSL'97)},
  ADDRESS =	 {Santa-Barbara, California},
  YEAR =	 1997,
  PAGES =	 {183--197},
  MONTH =	 OCT,
  PS =		 {http://www.ecs.soton.ac.uk/~lavm/papers/dsl97.ps.gz},
  EXPORT =	 {yes},
  PIND =	 {EZ~02~01~04},
  ABSTRACT =	 {This paper describes the semantics of Quantum, a
                  language that was specifically designed to control
                  resource consumption of distributed computations,
                  such as mobile agent style applications. In Quantum,
                  computations can be driven by mastering their
                  resource consumption. Resources can be understood as
                  processors cycles, geographical expansion, bandwidth
                  or duration of communications, etc. We adopt a
                  generic view by saying that computations need energy
                  to be performed. Quantum relies on three new
                  primitives that deal with energy. The first
                  primitive creates a tank of energy associated with a
                  computation. Asynchronous notifications inform the
                  user of energy exhaustion and computation
                  termination. The other two primitives allow us to
                  implement suspension and resumption of computations
                  by emptying a tank and by supplying more energy to a
                  tank. The semantics takes the form of an abstract
                  machine with explicit parallelism and energy-related
                  primitives.}
}

@inproceedings{morrisett+:abstract-memory-management,
  author =	 "Greg Morrisett and Matthias Felleisen and Robert
                  Harper",
  title =	 "Abstract Models of Memory Management",
  booktitle =	 "FPCA95: " # fpca,
  pages =	 "66--77",
  year =	     1995,
  month =	 jun,
  address =	 "La Jolla, CA",
}

@incollection{ morrisett97semantics,
    author = "Greg Morrisett and Robert Harper",
    title = "Semantics of Memory Management for Polymorphic Languages",
    booktitle = "Higher Order Operational Techniques in Semantics",
    publisher = "Newton Institute, Cambridge University Press",
    editor = "Andrew Gordon and Andrew M. Pitts",
    year = "1997",
    pages = {175--226},
    url = "citeseer.nj.nec.com/147455.html" }


@inproceedings{morrisett+:poly-memory-management,
  author =	 "Greg Morrisett and Robert Harper",
  title =	 "Semantics of Memory Management for Polymorphic
                  Languages",
  editor =	 "A. D. Gordon and A. M. Pitts",
  booktitle =	 "Higher Order Operational Techniques in Semantics",
  publisher =	 cambridge-press,
  year =	 1997,
}

@inproceedings{morrisett+:stal,
  author =	 "Greg Morrisett and Karl Crary and Neal Glew and
                  David Walker",
  title =	 "Stack-Based Typed Assembly Language",
  booktitle =	 o2 # " " # tic,
  year =	 1998,
  month =	 mar,
  series =	 lncs,
  volume =	 1473,
  publisher =	 springer,
  note =	 "Extended version published as CMU technical report
                  CMU-CS-98-178.",
  memo =	 "Extended version also published as Fox Memorandum
                  CMU-CS-FOX-98-05.",
}

@article{morrisett+:tal,
  author =	 "Greg Morrisett and David Walker and Karl Crary and
                  Neal Glew",
  title =	 "From {System} {F} to Typed Assembly Language",
  journal =	 toplas,
  year =	 1999,
  month =	 may,
  volume =	 21,
  number =	 3,
  pages =	 {528--569},
  note =	 "An earlier version appeared in the 1998 Symposium on
                  Principles of Programming Languages.",
}

@inproceedings{morrisett+:tal-popl,
  author =	 "Greg Morrisett and David Walker and Karl Crary and
                  Neal Glew",
  title =	 "From {System} {F} to Typed Assembly Language",
  booktitle =	 o25 # " " # popl,
  month =	 jan,
  year =	 1998,
  address =	 "San Diego",
  pages =	 "85--97",
  note =	 "Extended version published as Cornell University
                  technical report TR97-1651.",
}

@techreport{morrisett+:tal-tr,
  author =	 "Greg Morrisett and David Walker and Karl Crary and
                  Neal Glew",
  title =	 "From {System} {F} to Typed Assembly Language
                  (Extended Version)",
  institution =	 cornell-cs,
  year =	 1997,
  month =	 nov,
  number =	 "TR97-1651",
}

@inproceedings{morrisett+:til-safety,
  author =	 "Greg Morrisett and David Tarditi and Perry Cheng and
                  Chris Stone and Robert Harper and Peter Lee",
  title =	 "The {TIL/ML} Compiler: Performance and Safety
                  Through Types",
  booktitle =	 "Workshop on Compiler Support for Systems Software",
  year =	 1996,
  month =	 feb,
  address =	 "Tucson"
}

@phdthesis{morrisett:phd,
  author =	 "Greg Morrisett",
  title =	 "Compiling with Types",
  school =	 cmu-cs,
  year =	 1995,
  month =	 dec,
  address =	 pgh-pa,
}

@inproceedings{mycroft:poly-type-schemes,
  author =	 "Alan Mycroft",
  title =	 "Polymorphic Type Schemes and Recursive Definitions",
  booktitle =	 o6 # " " # "International Symposium on Programming",
  series =	 lncs,
  number =	 167,
  pages =	 "217--228",
  publisher =	 springer,
  month =	 apr,
  year =	 1984,
}

@inproceedings{ myers97parameterized,
    author = "Andrew C. Myers and Joseph A. Bank and Barbara Liskov",
    title = "Parameterized Types for {Java}",
    booktitle = "Conference Record of {POPL} '97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages",
    address = "New York, NY",
    pages = "132--145",
    year = "1997",
    url = "citeseer.nj.nec.com/myers97parameterized.html" }

%% O %%


%% N %%

@inproceedings{necula+:safe-extensions,
  title =	 "Safe Kernel Extensions Without Run-Time Checking",
  author =	 "George Necula and Peter Lee",
  booktitle =	 o2 # " " # osdi,
  year =	 1996,
  month =	 oct,
  pages =	 "229--243",
  address =	 "Seattle",
}

@inproceedings{necula+:touchstone,
  title =	 "The Design and Implementation of a Certifying
                  Compiler",
  author =	 "George Necula and Peter Lee",
  booktitle =	 1998 # " " # pldi,
  year =	 1998,
  month =	 jun,
  pages =	 "333--344",
  address =	 "Montreal",
}

@incollection{necula+:untrusted-agents,
  author =	 "George Necula and Peter Lee",
  title =	 "Safe, Untrusted Agents using Proof-Carrying Code",
  booktitle =	 "Special Issue on Mobile Agent Security",
  publisher =	 springer,
  series =	 lncs,
  volume =	 1419,
  month =	 oct,
  year =	 1997,
}

@inproceedings{necula:pcc,
  title =	 "Proof-Carrying Code",
  author =	 "George Necula",
  booktitle =	 o24 # " " # popl,
  year =	 1997,
  month =	 jan,
  address =	 "Paris",
  pages =	 "106--119",
}

@PhdThesis{necula:phd,
  author =	 {George Necula},
  title =	 {Compiling with Proofs},
  school =	 {Carnegie Mellon University},
  year =	 1998,
  address =	 pittsburgh-pa,
  month =	 sep,
  note =	 {Technical Report CMU-CS-98-154}
}





@inproceedings{neubauer01functional_notation,
  author = 	 {Matthias Neubauer and  Peter Thiemann and Martin Gasbichler and Michael Sperber },
  title = 	 {A Functional Notation for Functional Dependencies},
  booktitle = 	 {Preliminary Proceedings of the 2001 {ACM SIGPLAN}
Haskell Workshop
({HW}'2001)
Firenze, Italy
2nd September 2001},
  year =	 2001,
  editor =	 {Ralf Hinze},
  number =	 {UU-CS-2001-23},
  institution = {Institute of Information and Computing Sciences
Utrecht University}
}

@Book{nielson+:two-level,
  author =		  { Flemming Nielson and Hanne Riis Nielson},
  title = 		  {Two-Level Functional Languages},
  publisher = 	  cambridge-press,
  year = 		  1992,
  volume =		  34,
  series =		  {Cambridge Tracts in Theoretical Computer Science}
}

@inproceedings{ocallahan:jvm-types,
  author =	 "Robert O'Callahan",
  title =	 "A Simple, Comprehensive Type System for {Java}
                  Bytecode Subroutines",
  booktitle =	 o26 # " " # popl,
  year =	 1999,
  month =	 jan,
  address =	 "San Antonio, Texas",
  pages =	 {70--78},
}

@inproceedings{ odersky96putting,
    author = "Martin Odersky and Konstantin {L\"aufer}",
    title = "Putting Type Annotations to Work",
    booktitle = "Conference Record of {POPL} '96: The 23rd {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages, St. Petersberg Beach, Florida",
    address = "New York, N.Y.",
    pages = "54-67",
    year = "1996",
    url = "citeseer.nj.nec.com/odersky96putting.html" }


@article{ohearn+:param-local-vars,
  author =	 "Peter W. O'Hearn and Robert D. Tennent",
  title =	 "Parametricity and Local Variables",
  journal =	 jacm,
  volume =	 42,
  number =	 3,
  pages =	 "658--709",
  year =	 1995,
  month =	 may,
}
@inproceedings{okasaki:catenable-dequeues,
  author =	 "Chris Okasaki",
  title =	 "Catenable Double-Ended Queues",
  booktitle =	 1997 # " " # icfp,
  year =	 1997,
  month =	 jun,
  address =	 "Amsterdam",
  pages =	 "66--74",
}

@Book{okasaki:phd,
  author =		  {Chris Okasaki},
  title = 		  {Purely Functional Data Structures},
  publisher = 	  cambridge-press,
  year = 		  1998
}

@InProceedings{okasaki99fast,
  author = 	 {Chris Okasaki},
  title = 	 {From fast exponentiation to square matrices: An adventure in types},
  booktitle = 	 1999 # " " # icfp,
  pages =	 {28--35},
  year =	 1999,
  month =	sep,
  address = {Paris, France}
}


%% P %%

@techreport{palmgren+:domain-interp-itt,
  author =	 "Erik Palmgren and Viggo Stoltenberg-Hansen",
  title =	 "Domain Interpretations of Intuitionistic Type
                  Theory",
  institution =	 "Uppsala University, Department of Mathematics",
  year =	 1989,
  month =	 jan,
  type =	 "{U.U.D.M.} Report",
  number =	 "1989:1",
}

@article{palmgren:infosys-interp-mltt,
  author =	 "Erik Palmgren",
  title =	 "An Information System Interpretation of
                  {Martin-L\"{o}f}'s Partial Type Theory with
                  Universes",
  journal =	 iandc,
  year =	 1993,
  volume =	 106,
  pages =	 "26--60",
}

@inproceedings{palsberg:object-inference,
  author =	 "Jens Palsberg",
  title =	 "Efficient Inference of Object Types",
  booktitle =	 o9 # " " # lics,
  year =	 1994,
  month =	 jul,
  pages =	 "186--195",
  address =	 "Paris",
}

@article{park:fixpoint,
  author =	 "David Park",
  title =	 "Fixpoint Induction and Proofs of Program Properties",
  journal =	 "Machine Intelligence",
  volume =	 5,
  year =	 1969,
  pages =	 "59--78",
}



@Article{parigot:recursive,
  author = 	 {Michel Parigot},
  title = 	 {Recursive Programming with Proofs},
  journal = 	 tcs,
  year = 	 1992,
  volume =	 94,
  number =	 2,
  pages =	 {335-356},
  month =	 mar
}

@INPROCEEDINGS{Moh93,
  author = {Christin  Paulin-Mohring},
  booktitle = {Proceedings of the conference Typed Lambda Calculi and Applications},
  editor = {Marc Bezem and Jan Friso Groote},
  institution = {LIP-ENS Lyon},
  note = {LIP research report 92-49},
  number = {664},
  pages  ={328--345},
  series = {Lecture Notes in Computer Science},
  title = {Inductive Definitions in the System {Coq} - Rules and Properties},
  type = {research report},
  year = {1993},
}

@book{paulson:lcf,
  author =	 "Lawrence C. Paulson",
  title =	 "Logic and Computation: Interactive Proof with
                  {Cambridge} {LCF}",
  year =	 1987,
  publisher =	 cambridge-press,
}



@InProceedings{persson99lctes,
  author =	 {Patrik Persson},
  title =	 {Live Memory Analysis for Garbage Collection in
                  Embedded Systems},
  booktitle =	 1999 # " " # lctes,
  pages =	 {45--54},
  year =	 1999,
  volume =	 34,
  number =	 7,
  series =	 {SIGPLAN Notices},
  address =	 {Atlanta, GA},
  month =	 {may}
}


@TECHREPORT{PetersonHL97,
  AUTHOR = {Peterson, John and Hudak, Paul and Ling, Gary Shu},
  TITLE = {Principled Dynamic Code Improvement},
  INSTITUTION = {Department of Computer Science, Yale University},
  NUMBER = {YALEU/DCS/RR-1135},
  MONTH = {July},
  YEAR = {1997},
  URL = {http://www.cis.upenn.edu/~mwh/papers_DB/yale-tr.ps}
}

@Unpublished{peyton-jones:boilerplate,
  author = 		  {Simon {Peyton Jones} and Ralf Laemmel},
  title = 		  {Scrap your Boilerplate: a practical design pattern for generic programming},
  note = 		  {Available at http://research.microsoft.com/Users/simonpj/papers/hmap/},
  year =			  2002
}

@InProceedings{peyton-jones+:unboxed,
  author = 		  {Simon {Peyton Jones} and John Launchbury},
  title = 		  {Unboxed values as first class citizens in a 
non-strict functional programming language},
  booktitle = 	  "FPCA91:" # " " # fpca,
  pages =		  {636-666},
  year =			  1991,
  address =		  {New York, NY},
  month =		  aug,
  publisher =	  {ACM Press}
}

@inproceedings{peyton-jones+:ghc,
  author =	 "Simon L. {Peyton Jones} and Cordelia V. Hall and
                  Kevin Hammond and Will Partain and Philip Wadler",
  title =	 "The {G}lasgow {H}askell compiler: a technical
                  overview",
  year =	 1993,
  month =	 jul,
  booktitle =	 "Proc. UK Joint Framework for Information Technology
                  (JFIT) Technical Conference",
}

@inproceedings{peyton-jones+:imperative-fnal-prog,
  author =	 "Peyton Jones, Simon L. and Philip Wadler",
  title =	 "Imperative Functional Programming",
  booktitle =	 o20 # " " # popl,
  address =	 "Charleston, South Carolina",
  year =	 1993,
  month =	 jan,
}

@TechReport{peyton-jones99:haskell,
  author =	 {Simon {Peyton Jones} and John Hughes},
  title =	 {Report on the Programming Language {H}askell 98, A
                  Non-strict Purely Functional Language},
  institution =	 {Yale University, Department of Computer Science},
  year =	 1999,
  number =	 {YALEU/DCS/RR-1106},
  month =	 feb,
  note =	 {Available from \url{http://www.haskell.org/definition/}}
}

@Book{peyton-jones03:haskell,
  editor =		  {Simon {Peyton Jones}},
  title = 		  {Haskell 98 Language and Libraries: The Revised Report},
  publisher = 	  {Cambridge University Press},
  year = 		  2003
}




@InProceedings{pfenning+:twelf,
  author = 		  {Frank Pfenning and Carsten Sch\"urmann},
  title = 		  {System description: Twelf---a meta-logical framework for deductive systems},
  booktitle =	  {Proceedings of the 16th International Conference on Automated Deduction (CADE-16)},
  pages =		  {202--206},
  year =			  1999,
  editor =		  {H. Ganzinger},
  address =		  {Trento, Italy},
  month =		  jul
}

@InProceedings{pfenning+:hoas,
  author = 	 {Frank Pfenning and Conal Elliott},
  title = 	 {Higher-order Abstract Syntax},
  booktitle = 	 1988 # " " # pldi,
  pages =	 {199-208},
  year =	 1988,
  address =	 {Atlanta, GA, USA},
  month =	 jun
}

@inproceedings{pfenning+:leap,
  author =	 "Frank Pfenning and Peter Lee",
  title =	 "{LEAP}: A language with eval and polymorphism",
  booktitle =	 "Proceedings of the International Joint Conference on
                  Theory and Practice in Software Development",
  address =	 "Barcelona",
  year =	 1989,
  series =	 lncs,
  volume =	 352,
  publisher =	 springer,
  pages =	 "345--359",
}

@techreport{pfenning:inductive-types-coq,
  author =	 "Frank Pfenning",
  title =	 "Inductively Defined Types in the Calculus of Constructions",
  institution =	 cmu-cs,
  month =	 nov,
  year =	 1988,
  type =	 "Ergo Report",
  number =	 "88-069",
}


@INPROCEEDINGS{PfPa89,
  author = {Frank Pfenning and Christin Paulin-Mohring},
  booktitle = {Proceedings of Mathematical Foundations of Programming Semantics},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 442,
  title = {Inductively defined types in the {Calculus of Constructions}},
  year = 1990,
  pages = {209--228}
}

@inproceedings{pfenning:partial-inference,
  author =	 "Frank Pfenning",
  title =	 "Partial Polymorphic Type Inference and Higher-Order
                  Unification",
  booktitle =	 1998 # " " # lfp,
  year =	 1988,
  month =	 jul,
  pages =	 "153--163",
  address =	 "Snowbird, Utah",
}

@article{pfenning:recon-undecidable,
  author =	 "Frank Pfenning",
  title =	 "On the Undecidability of Partial Polymorphic Type
                  Reconstruction",
  journal =	 "Fundamenta Informaticae",
  year =	 1993,
  volume =	 19,
  number =	 "1,2",
  pages =	 "185--199",
}

@inproceedings{pfenning:unification,
  author =	 "Frank Pfenning",
  title =	 "Unification and Anti-Unification in the Calculus of
                  Constructions",
  booktitle =	 o6 # " " # lics,
  year =	 1991,
  month =	 jul,
  pages =	 "74--85",
  address =	 "Amsterdam",
}

@article{pierce+:ho-subtyping,
  author =	 "Benjamin Pierce and Martin Steffen",
  title =	 "Higher-Order Subtyping",
  year =	 1997,
  journal =	 "Theoretical Computer Science",
  volume =	 176,
  number =	 "1--2",
  pages =	 "235--282",
}

@article{pierce+:oop-tt-foundations,
  author =	 "Benjamin C. Pierce and David N. Turner",
  title =	 "Simple Type-Theoretic Foundations For
                  Object-Oriented Programming",
  journal =	 jfp,
  year =	 1994,
  month =	 apr,
  volume =	 4,
  number =	 2,
  pages =	 "207--247",
}

@inproceedings{pierce+:oop-wo-rectype,
  author =	 "Benjamin C. Pierce and David N. Turner",
  title =	 "Object-Oriented Programming Without Recursive Types",
  booktitle =	 o20 # " " # popl,
  year =	 1993,
  month =	 jan,
  pages =	 "299--312",
}

@techreport{pierce+:programming-in-ho-lambda,
  author =	 "Benjamin Pierce and Scott Dietzen and Spiro
                  Michaylov",
  title =	 "Programming in Higher-Order Typed Lambda-Calculi",
  year =	 1989,
  institution =	 cmu-cs,
  number =	 "CMU-CS-89-111",
}

@incollection{pierce:bq-undecidable,
  author =	 "Benjamin C. Pierce",
  title =	 "Bounded Quantification is Undecidable",
  booktitle =	 "Theoretical Aspects of Object-Oriented Programming",
  year =	 1994,
  publisher =	 "The {MIT} Press",
  pages =	 "427--459",
}

@article{pierce:intersection-and-bq,
  author =	 "Benjamin C. Pierce",
  title =	 "Intersection Types and Bounded Polymorphism",
  pages =	 "129--193",
  journal =	 mscs,
  month =	 apr,
  year =	 1997,
  volume =	 7,
  number =	 2,
}

@phdthesis{pierce:phd,
  author =	 "Benjamin C. Pierce",
  title =	 "Programming with Intersection Types and Bounded
                  Polymorphism",
  school =	 cmu-cs,
  year =	 1991,
  month =	 dec,
  address =	 pgh-pa,
}

@manual{pierce:pict,
  author =	 "Benjamin C. Pierce",
  title =	 "Programming in the Pi-Calculus: An Experiment in
                  Concurrent Language Design",
  year =	 1995,
  month =	 dec,
  webnote =	 "Available at
                  http://www.cs.indiana.edu/hyplan/pierce/ftp/pict/Html/Pict.html",
}



@inproceedings{ pierce98local,
    author = "Benjamin C. Pierce and David N. Turner",
    title = "Local Type Inference",
    booktitle = "Conference Record of {POPL} 98: The 25TH {ACM} {SIGPLAN}-{SIGACT} 
              Symposium on Principles of Programming Languages, San Diego, California",
    address = "New York, NY",
    pages = "252--265",
    year = "1998",
    url = "citeseer.nj.nec.com/pierce98local.html" }


@Book{pierce:book,
  author =	 {Benjamin C. Pierce},
  title = 	 {Types and Programming Languages},
  publisher = 	 mit-press,
  year = 	 2002
}

@InProceedings{pierce+:recursive-types-dummies,
  author = "Vladimir Gapeyev and Michael Y. Levin and Benjamin C. Pierce",
  title = "Recursive Subtyping Revealed",
  booktitle = 2000 # " " # icfp,
  address = "Montreal",
  month = sep, 
  year = 2000,
  pages = {221--232},
  url = "citeseer.nj.nec.com/470426.html" }
}

@inproceedings{ pitts00metalanguage,
    author = "Andrew M. Pitts and Murdoch Gabbay",
    title = "A Metalanguage for Programming with Bound Names Modulo Renaming",
    booktitle = "Mathematics of Program Construction",
    pages = "230--255",
    year = "2000",
    url = "citeseer.nj.nec.com/pitts00metalanguage.html" }

@TechReport{plotkin:logical-relations,
  author = 		  {G.D. Plotkin},
  title = 		  {Lambda-definablility and logical relations},
  institution =  {University of Edinburgh, School of Artificial Intelligence},
  year = 		  1973,
  number =		  {SAI-RM-4}
}
@article{plotkin:name-value,
  author =	 "Gordon D. Plotkin",
  title =	 "Call-by-name, call-by-value, and the lambda
                  calculus",
  journal =	 tcs,
  volume =	 1,
  year =	 1975,
  pages =	 "125--159",
}



@inbook{plotkin:lambda-definability,
  author = 		  {G.D. Plotkin},
  chapter = 		  {Lambda definability in the full type hierarchy},
  book = 	  {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
  year = 		  1980,
  pages =		  {363--373},
  publisher =    {Academic Press}
}

@inproceedings{plotkin+:param-logic,
  author =	 "Gordon Plotkin and Mart\'{\i}n Abadi",
  title =	 "A Logic for Parametric Polymorphism",
  booktitle =	 tlca,
  year =	 1993,
  pages =	 "361--375",
}

@inproceedings{plotkin+:subtype-parametricity,
  author =	 "Gordon Plotkin and Mart\'{\i}n Abadi and Luca
                  Cardelli",
  title =	 "Subtyping and Parametricity",
  booktitle =	 o9 # " " # lics,
  year =	 1994,
  month =	 jul,
  pages =	 "310--319",
}

@MastersThesis{poulsen:masters,
  author =  {Eigil Rosager Poulsen},
  title  = {Representation analysis for efficient implementation
            of polymorphism},
  school = {DIKU, University of Copenhagen},
  year   = 1993,
  month  = apr
}

%% Q %%

%% R %%
@inproceedings{pottier:simp-subtyping,
  author =	 "Fran\c{c}ois Pottier",
  title =	 "Simplifying Subtyping Constraints",
  booktitle =	 1996 # " " # icfp,
  year =	 1996,
  month =	 may,
  address =	 "Philadelphia",
  pages =	 "122--133",
}

@inproceedings{reed99:xenoservers,
  author =	 "D. Reed and I. Pratt and S. Early and P. Menage and
                  N. Stratford",
  title =	 "Xenoservers: Accountable execution of untrusted
                  programs",
  booktitle =	 o7 # " " # hotos,
  month =	 1999,
  year =	 "1999"
}

@InProceedings{reistad94,
  author =	 {Brian Reistad and David K. Gifford},
  title =	 {Static Dependent Costs for Estimating Execution
                  Time},
  booktitle =	 lfp,
  pages =	 {65--78},
  year =	 1994,
  address =	 {Orlando, FL},
  month =	 jul
}

@inproceedings{remy+:objective-ml,
  title =	 "Objective {ML}: A Simple Object-Oriented Extension
                  of {ML}",
  author =	 "Didier R\'{e}my and J\'{e}r\^{o}me Vouillon",
  booktitle =	 o24 # " " # popl,
  year =	 1997,
  month =	 jan,
  address =	 "Paris",
  pages =	 "40--53",
}

@inproceedings{remy:ml-art,
  author =	 "Didier R\'{e}my",
  title =	 "Programming Objects with {ML-ART}: An Extension to
                  {ML} with Abstract and Record Types",
  booktitle =	 tacs # " 1994",
  address =	 "Sendai, Japan",
  year =	 1994,
  pages =	 "321--346",
  series =	 lncs,
  volume =	 789,
  publisher =	 springer,
}

@incollection{remy:record-ext,
  author =	 "Didier R\'{e}my",
  title =	 "Type Inference for Records in a Natural Extension of
                  {ML}",
  booktitle =	 "Theoretical Aspects of Object-Oriented Programming",
  editor =	 "Carl A. Gunter and John C. Mitchell",
  chapter =	 3,
  pages =	 "67--95",
  year =	 1994,
  publisher =	 mit-press,
  address =	 cam-ma,
}

@inproceedings{remy:type-rec-var,
  author =	 "Didier R\'{e}my",
  title =	 "Typechecking Records and Variants in a Natural
                  Extension of {ML}",
  booktitle =	 o16 # " " # popl,
  pages =	 "77--87",
  year =	 1989,
  month =	 jan,
}



@inproceedings{reppy+:simple-objects,
  author =	 "John Reppy and Jon Riecke",
  title =	 "Simple Objects for {S}tandard {ML}",
  booktitle =	 1996 # " " # pldi,
  year =	 1996,
  month =	 may,
  pages =	 "171--180",
  address =	 "Philadelphia",
}

@inproceedings{reynolds:definitional-interp,
  author =	 "John C. Reynolds",
  title =	 "Definitional Interpreters for Higher-Order
                  Programming Languages",
  booktitle =	 "Conference Record of the 25th National ACM
                  Conference",
  pages =	 "717--740",
  address =	 "Boston",
  month =	 aug,
  year =	 "1972",
}

@inproceedings{reynolds:essence-of-algol,
  author =	 "John C. Reynolds",
  title =	 "The Essence of {Algol}",
  booktitle =	 "Proceedings of the International Symposium on
                  Algorithmic Languages",
  editor =	 "J. W. de Bakker and J. C. van Vliet",
  address =	 "Amsterdam",
  year =	 1981,
  month =	 oct,
  pages =	 "345--372",
  publisher =	 noholland,
}

@techreport{reynolds:forsythe,
  author =	 "John C. Reynolds",
  title =	 "Design of the Programming Language {F}orsythe",
  year =	 1996,
  month =	 jun,
  institution =	 cmu-cs,
  number =	 "CMU-CS-94-146",
}

@incollection{reynolds:implicit-conversions,
  author =	 "John C. Reynolds",
  title =	 "Using Category Theory to Design Implicit Conversions
                  and Generic Operators",
  booktitle =	 "Semantics-Directed Compiler Generation",
  publisher =	 springer,
  series =	 lncs,
  volume =	 94,
  year =	 1980,
  pages =	 "211--258",
}

@inproceedings{reynolds:intersection-coherence,
  author =	 "John C. Reynolds",
  title =	 "The Coherence of Languages with Intersection Types",
  booktitle =	 tacs # " 1991",
  address =	 "Sendai, Japan",
  year =	 1991,
  pages =	 "675--700",
  series =	 lncs,
  volume =	 526,
  publisher =	 springer,
}

@inproceedings{REYNOLDS83,
  author =	 "John C. Reynolds",
  title =	 "Types, Abstraction and Parametric Polymorphism",
  booktitle =	 "Information Processing '83",
  year =	 1983,
  pages =	 "513--523",
  publisher =	 noholland,
  note =	 "Proceedings of the IFIP 9th World Computer Congress",
}

@inproceedings{reynolds:polymorphism-not-set-theoretic,
  author =	 "John C. Reynolds",
  title =	 "Polymorphism is not Set-Theoretic",
  booktitle =	 "Proceedings of the International Symposium on
                  Semantics of Data Types",
  year =	 1984,
  series =	 lncs,
  volume =	 173,
  publisher =	 springer,
  pages = {145--156}
}

@inproceedings{reynolds:syntactic-control-interfere,
  author =	 "John C. Reynolds",
  title =	 "Syntactic Control of Interference",
  booktitle =	 o5 # " " # popl,
  year =	 1978,
  pages =	 "39--46",
  address =	 "Tucson, Arizona",
}

@inproceedings{reynolds:syntactic-control-interfere2,
  author =	 "John C. Reynolds",
  title =	 "Syntactic Control of Interference, Part 2",
  booktitle =	 o16 # " " # icalp,
  month =	 jul,
  year =	 1989,
}

@inproceedings{reynolds:type-structure,
  author =	 "John C. Reynolds",
  title =	 "Towards a theory of type structure",
  booktitle =	 "Programming Symposium",
  pages =	 "408--425",
  series =	 lncs,
  volume =	 19,
  year =	 1974,
}

@Article{reynolds+:funept,
  author =	 {John C.~Reynolds and Gordon D.~Plotkin},
  title =	 {On Functors Expressible in the Polymorphic Typed
                  Lambda Calculus},
  journal =	 {Information and Computation},
  year =	 1993,
  volume =	 105,
  pages =	 {1--29}
}

@techreport{rezus:semant-ctt,
  author =	 "Adrian Rezus",
  title =	 "Semantics of Constructive Type Theory",
  institution =	 "Informatics Department, Faculty of Science,
                  Nijmegen, University, The Netherlands",
  year =	 1985,
  month =	 sep,
  number =	 70,
}

@inproceedings{ roe97lightweight,
    author = "Paul Roe and Clemens Szyperski",
    title = "Lightweight Parametric Polymorphism for Oberon",
    booktitle = "Proc. of Joint Modular Languages Conference ({JMLC})",
    address = "Linz, Austria",
    year = "1997",
    url = "citeseer.nj.nec.com/roe97lightweight.html" }


@INPROCEEDINGS{Rouaix96,
  AUTHOR = {Fran\c{c}ois Rouaix},
  TITLE = {A {Web} navigator with applets in {Caml}},
  BOOKTITLE = {Proceedings of the 5th International {World} {Wide} {Web}
                  Conference, in {Computer} {Networks} and
                  {Telecommunications} {Networking}},
  VOLUME = {28},
  YEAR = {1996},
  PUBLISHER = {Elsevier},
  MONTH = {May},
  PAGES = {1365--1371},
  URL = {http://pauillac.inria.fr/~rouaix/mmm/papers/mmm.ps.gz}
}



@InProceedings{ ruehr98structural,
    author = "Fritz Ruehr",
    title = "Structural polymorphism",
    booktitle = "Informal Proceedings Workshop on Generic Programming, WGP'98, Marstrand,
      Sweden, 18 June 1998.",
    editor = "Roland Backhouse and Tim Sheard",
    year = 1998,
    url = "citeseer.nj.nec.com/ruehr98structural.html"
}



@PhdThesis{ruehr:phd,
  author = 	 {Fritz Ruehr},
  title = 	 {Analytical and Structural Polymorphism Expressed Using Patterns Over Types},
  school = 	 {University of Michigan},
  year = 	 1992
}

@inproceedings{ruf:df,
  title =	 "Partitioning Dataflow Analyses Using Types",
  author =	 "Erik Ruf",
  booktitle =	 o24 # " " # popl,
  year =	 "1997",
  month =	 jan,
  pages =	 "15--26",
  address =	 "Paris",
}

@article{russell:types,
  author =	 "Bertrand Russell",
  title =	 "Mathematical logic as based on a theory of type",
  journal =	 "Am. J. Math.",
  volume =	 30,
  pages =	 "222--262",
  year =	 1908,
}

%% S %%

@inproceedings{saha+:type-lift,
  author =	 "Bratin Saha and Zhong Shao",
  title =	 "Optimal Type Lifting",
  booktitle =	 o2 # " " # tic,
  year =	 1998,
  month =	 mar,
}

@InProceedings{saha+:fully,
  author = 	 {Valery Trifonov and  Bratin Saha and Zhong Shao},
  title = 	 {Fully Reflexive Intensional Type Analysis},
  booktitle = 	 o5 # " " # icfp,
  year =	 2000,
  address =	 "Montreal",
  month =	 sep,
  pages =        "82--93",
  annote =	 {Extended version is YALEU/DCS/TR-1194}
}

@InProceedings{saha+:fully-erasure,
  author = 	 {Bratin Saha and Valery Trifonov and Zhong Shao},
  title = 	 {Fully Reflexive Intensional Type Analysis in Type Erasure Semantics},
  booktitle = 	 o3 # " " # tic,
  year =	 2000,
  address =	 "Montreal",
  month =	 sep
}


@inproceedings{DBLP:conf/types/BradyMM03,
  author    = {Edwin Brady and
               Conor McBride and
               James McKinna},
  title     = {Inductive Families Need Not Store Their Indices},
  booktitle = {TYPES},
  year      = {2003},
  pages     = {115-129},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3085{\&}spage=115},
  crossref  = {DBLP:conf/types/2003},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/types/2003,
  editor    = {Stefano Berardi and
               Mario Coppo and
               Ferruccio Damiani},
  title     = {Types for Proofs and Programs, International Workshop, TYPES
               2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected
               Papers},
  booktitle = {TYPES},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3085},
  year      = {2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@STRING{fossacs11="Foundations of Software Science and Computational
		  Structures, 14th International Conference, FOSSACS 2011,
                  Saarbrucken, Germany"}

@InProceedings{abel:fossacs11,
  author	= {Andreas Abel},
  title		= {Irrelevance in Type Theory with a Heterogeneous Equality
		  Judgement},
  optcrossref	= {},
  optkey	= {},
  booktitle	= fossacs11,
  optpages	= {},
  year		= {2011},
  opteditor	= {},
  optvolume	= {},
  optnumber	= {},
  optseries	= {},
  optaddress	= {},
  optmonth	= {},
  optorganization={},
  optpublisher	= {},
  note		= {To appear.},
  opturl	= {},
  optpostscript	= {},
  optpdf	= {},
  optdvi	= {},
  optabstract	= {}
}

@inproceedings{bengtson+:f7,
 author = {Bengtson, Jesper and Bhargavan, Karthikeyan and Fournet, C\'{e}dric and Gordon, Andrew D. and Maffeis, Sergio},
 title = {Refinement Types for Secure Implementations},
 booktitle = {Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium},
 year = {2008},
 isbn = {978-0-7695-3182-3},
 pages = {17--32},
 numpages = {16},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
} 


@inproceedings{Borgstrom:2011:VSP:1929529.1929532,
 author = {Borgstrom, Johannes and Chen, Juan and Swamy, Nikhil},
 title = {Verifying stateful programs with substructural state and hoare types},
 booktitle = {Proceedings of the 5th ACM workshop on Programming languages meets program verification},
 series = {PLPV '11},
 year = {2011},
 isbn = {978-1-4503-0487-0},
 location = {Austin, Texas, USA},
 pages = {15--26},
 numpages = {12},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {affine types, dependent types, security type systems}}





@incollection {mishra:erasure,
   author = {Mishra-Linger, Nathan and Sheard, Tim},
   affiliation = {Portland State University},
   title = {Erasure and Polymorphism in Pure Type Systems},
   booktitle = {Foundations of Software Science and Computational Structures},
   series = {Lecture Notes in Computer Science},
   editor = {Amadio, Roberto},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {},
   pages = {350-364},
   volume = {4962},
   year = {2008}
}
@Article{saltzer75protection,
  author =	 "J.H. Saltzer and M.D. Schroeder",
  title =	 "The Protection of Information in Computer Systems",
  journal =	 {Proceedings of the IEEE},
  year =	 1975,
  volume =	 63,
  number =	 9,
  pages =	 {1278--1308},
  month =	 sep
}

@article{ schneider00enforceable,
    author = "Fred B. Schneider",
    title = "Enforceable security policies",
    journal = "Information and System Security",
    volume = "3",
    number = "1",
    pages = "30-50",
    year = "2000",
    url = "citeseer.nj.nec.com/article/schneider98enforceable.html" }


@Article{schurmann:hoas,
  author = 	 {Carsten Sch\"{u}rmann and Jo\"{e}lle Despeyroux and Frank Pfenning},
  title = 	 {Primitive recursion for higher-order abstract syntax},
  journal = 	 {Theoretical Computer Science},
  year = 	 2001,
  volume =	 266,
  number =	 {1--2},
  pages =	 {1--58},
  month =	 sep
}

@Unpublished{schuermann:delphin,
  author = 		  {Carsten Sch\"{u}rmann and Richard Fontana and Yu Liao},
  title = 		  {Delphin: Functional Programming with deductive systems},
  note = 		  {Available at \url{http://cs-www.cs.yale.edu/homes/carsten/}},
  year =			  2002
}

@inproceedings{scott:advice-modal,
  author =		  {Dana Scott},
  editor =		  {K. Lambert},
  booktitle = 		  {Philosophical Problems in Logic},
  title = 	  {Advice on Modal Logic},
  publisher = 	  {D. Riedel Publishing Company},
  year = 		  1973,
  pages =		  {143--173}
}

@inproceedings{scott+:semantics,
  author =	 "Dana Scott and Christopher Strachey",
  title =	 "Toward a Mathematical Semantics for Computer
                  Languages",
  booktitle =	 "Proceedings of the Symposium on Computers and
                  Automata",
  series =	 "Microwave Research Institute Symposia Series",
  volume =	 21,
  publisher =	 "Polytechnic Institute of Brooklyn",
  year =	 1971,
}

@inproceedings{scott:lattice-models,
  author =	 "Dana Scott",
  title =	 "Lattice Theoretic Models for Various Type-Free
                  Calculi",
  booktitle =	 "Fourth International Congress of Logic, Methodology
                  and Philosophy of Science",
  publisher =	 noholland,
  year =	 1972,
}

@inproceedings{scott:math-thy-comp,
  author =	 "Dana Scott",
  title =	 "Outline of a Mathematical Theory of Computation",
  booktitle =	 "Fourth Princeton Conference on Information Sciences
                  and Systems",
  year =	 1970,
  pages =	 "169--176",
}

@InProceedings{seltzer96vino,
  author =	 {Margo Seltzer and Yasuhiro Endo and Chris Small and
                  Keith Smith},
  title =	 {Dealing with Disaster: Surviving Misbehaved Kernel
                  Extensions},
  booktitle =	 o2 # " " # osdi,
  pages =	 {213--227},
  year =	 1996,
  address =	 {Seattle, WA},
  month =	 oct
}

@inproceedings{senizergues:dpda,
  author =	 "G\'{e}raud S\'{e}nizergues",
  title =	 "The Equivalence Problem for Deterministic Pushdown
                  Automata is Decidable",
  booktitle =	 o24 # " " # icalp,
  year =	 1997,
  month =	 jul,
  address =	 "Bologna, Italy",
  pages =	 "671--681",
  series =	 lncs,
  volume =	 1256,
  publisher =	 springer,
}

@Book{dylan:manual,
  author =		  {Andrew Shalit and  David Moon and Orca Starbuck},
  title = 		  {The Dylan Reference Manual : The Definitive Guide to the New Object-Oriented Dynamic Language
},
  publisher = 	  {Apple Press},
  year = 		  1996
}

@InProceedings{shao98implementing,
  author =	 {Zhong Shao and Christopher League and Stefan
                  Monnier},
  title =	 {Implementing Typed Intermediate Languages},
  booktitle =	 1998 # " " # icfp,
  pages =	 {313--323},
  year =	 1998,
   volume =	 34,
  number =	 1,
  series =	 {{ACM} {SIGPLAN} Notices},
  address =	 {Baltimore, Maryland},
  month =	 {sep}
}

@inproceedings{shao:flint,
  author =	 "Zhong Shao",
  title =	 "An Overview of the {FLINT/ML} Compiler",
  booktitle =	 1997 # " " # tic,
  month =	 jun,
  year =	 1997,
  address =	 "Amsterdam",
  note =	 "Published as {B}oston {C}ollege Computer Science
                  Department Technical Report BCCS-97-03",
}

@inproceedings{shao:rep-analysis,
  author =	 "Zhong Shao",
  title =	 "Flexible Representation Analysis",
  booktitle =	 1997 # " " # icfp,
  year =	 1997,
  month =	 jun,
  address =	 "Amsterdam",
  pages =	 "85--98",
}

@inproceedings{shao:typed-module-comp,
  author =	 "Zhong Shao",
  title =	 "Typed Cross-Module Compilation",
  booktitle =	 1998 # " " # icfp,
  year =	 1998,
  month =	 sep,
  address =	 "Baltimore, Maryland",
  pages =	 "141--152",
}



@Article{shaw89time,
  author = 	 {Alan C. Shaw},
  title = 	 {Reasoning about Time in Higher-Level Language Software},
  journal = 	 tse,
  year = 	 1989,
  volume =	 15,
  number =	 7,
  pages =	 {875--889},
  month =	 jul
}


@TechReport{ sheard93type,
  author = "Tim Sheard",
  title = "Type parametric programming",
  number = "CSE 93-018",
  institution =  {Oregon Graduate Institute},
  year = 1993,
  url = "citeseer.nj.nec.com/sheard93type.html" }



@inproceedings{shields01object-oriented,
    author = {Mark Shields and Simon {Peyton Jones}},
    title = {Object-Oriented Style Overloading for Haskell},
    booktitle = {Electronic Notes in Theoretical Computer Science},
    volume = {59},
    issue = {1},
    publisher = {Elsevier Science Publishers},
    editor = {Nick Benton
 and Andrew Kennedy},
    year = {2001},
    url = "http://www.elsevier.com/gej-ng/31/29/23/89/27/show/Products/notes/index.htt#008"
}

@Article{shostak:residue,
  author =	 {R. Shostak},
  title =	 {Deciding linear inequalities by computing loop
                  residues},
  journal =	 jacm,
  year =	 1981,
  volume =	 28,
  number =	 4,
  pages =	 {748--752},
  month =	 oct
}



@inproceedings{sirer+:spinlink,
 author = "Emin Gun Sirer and Marc E. Fiuczynski and Przemyslaw Pardyak and Brian N. Bershad",
 title = "Safe Dynamic Linking in an Extensible Operating System",
 booktitle = o1 # " " # wcsss,
 year = 1996,
 month = "February",
 address = "Tucson",
}


@InProceedings{smith00alias,
  author =	 {Frederick Smith and David Walker and Greg Morrisett},
  title =	 {Alias Types},
  booktitle =	 {European Symposium on Programming},
  year =	 2000,
  address =	 {Berlin, Germany},
  month =	 mar
}

@phdthesis{smithg:phd,
  author =	 "Geoffrey Seward Smith",
  title =	 "Polymorphic Type Inference For Languages with
                  Overloading and Subtyping",
  school =	 cornell-cs,
  year =	 1991,
  month =	 aug,
  address =	 ith-ny,
}

@Article{smith+:active,
  author = 		  {Jonathan M. Smith and
 Kenneth L. Calvert and Sandra L. Murphy and Hilarie K. Orman and Larry L. Peterson},
  title = 		  {Activating networks: A progress report},
  journal = 	  {IEEE Computer},
  year = 		  {1999},
  OPTkey = 		  {},
  OPTvolume = 	  {32},
  OPTnumber = 	  {4},
  OPTpages = 	  {32--41},
  OPTmonth = 	  apr,
  OPTnote = 	  {},
  OPTannote = 	  {}
}

@article{smith:partial-total,
  author =	 "Scott F. Smith",
  title =	 "Hybrid Partial-Total Type Theory",
  journal =	 "International Journal of Foundations of Computer
                  Science",
  volume =	 6,
  pages =	 "235--263",
  year =	 1995,
}

@phdthesis{smith:phd,
  author =	 "Scott Fraser Smith",
  title =	 "Partial Objects in Type Theory",
  school =	 cornell-cs,
  month =	 jan,
  year =	 1989,
  address =	 ith-ny,
}



@InProceedings{smith:reflection,
  author = 		  {Brian Cantwell Smith},
  title = 		  {Reflection and Semantics in {LISP}},
  booktitle = 	  o14 # " " # popl,
  pages =		  {23--35},
  year =			  1984
}

@inproceedings{solomon:type-defs-param,
  author =	 "Marvin Solomon",
  title =	 "Type Definitions with Parameters (Extended
                  Abstract)",
  booktitle =	 o5 # " " # popl,
  year =	 1978,
  month =	 jan,
  address =	 "Tucson, Arizona",
  pages =	 "31--38",
}

@InProceedings{spatscheck99:_defen_scout,
  author =	 {Oliver Spatscheck and Larry L.Peterson },
  title =	 {Defending against denial of service attacks in
                  Scout},
  booktitle =	 o3 # " " # sosp,
  pages =	 {59-72},
  year =	 1999
}

@InProceedings{splawski+:type-fixpoints,
  author = 	 {Zdzis\l{}aw Sp\l{}awski and Pawe\l{} Urzyczyn},
  title = 	 {Type Fixpoints: Iteration vs. Recursion},
  booktitle = 	 o4 # " " # icfp,
  pages =	 {102--113},
  year =	 1999,
  address =	 {Paris, France},
  month =	 sep
}

@TechReport{spoonhower98telephony,
  author =	 {Daniel Spoonhower and Grzegorz Czajkowski and Chris
                  Hawblitzel and Chi-Chao Chang and Deyu Hu and
                  Thorsten von Eicken},
  title =	 {Design and Evaluation of an Extensible Web &
                  Telephony Server based on the J-Kernel},
  institution =	 cornell-cs,
  year =	 1998,
  number =	 {TR98-1715},
  address =	 {ithaca-ny}
}

@inproceedings{stansifer:subtype-inf,
  title =	 "Type Inference with Subtypes",
  author =	 "Ryan Stansifer",
  booktitle =	 o15 # " " # popl,
  address =	 "San Diego",
  year =	 1988,
  month =	 jan,
  pages =	 "88--97",
}



@Article{statman:logical-relations,
  author = 		  {R. Statman},
  title = 		  {Logical Relations and Typed Lambda Calculus},
  journal = 	  {Information and Control},
  year = 		  1985,
  volume =		  65,
  pages =		  {85--97}
}

@mastersthesis{steele:rabbit,
  author =	 "Guy L. {Steele Jr.}",
  title =	 "{R}abbit: A Compiler for {S}cheme",
  school =	 "MIT",
  year =	 1978,
}



@Book{steele:cltl2,
  author =		  {Guy L. {Steele Jr.}},
  title = 		  {Common Lisp the Language, 2nd Edition},
  publisher = 	  {Digital Press},
  year = 		  1990
}

@techreport{stone+:sml96,
  title =	 "A Type-Theoretic Account of {S}tandard {ML} 1996",
  author =	 "Chris Stone and Robert Harper",
  institution =	 cmu-cs,
  year =	 1996,
  number =	 "CMU-CS-96-136",
}

@InProceedings{stone+:singleton-kinds,
  author = 		  {Chris Stone and Robert Harper},
  title = 		  {Deciding Type Equivalence in a Language with Singleton Kinds},
  booktitle = 	  o27 # " " # popl,
  pages =		  {214--225},
  year =			  2000,
  address =		  {Boston, MA, USA},
  month =		  jan
}

@Article{strachey:param,
  author = 	 {Christopher Strachey},
  title = 	 {Fundamental Concepts in Programming Languages},
  journal = 	 {Higher-Order and Symbolic Computation},
  year = 	 2000,
  volume =	 13,
  pages =	 {11--49},
  note =	 {This paper forms the substance of a course of lectures given at the International Summer School in
                      Computer Programming at Copenhagen in August, 1967.}
}



@Book{stroustrup:c++,
  author =		  {Bjarne Stroustrup},
  title = 		  {The C++ Programming Language (Third Edition) },
  publisher = 	  {Addison Wesley Longman},
  year = 		  1997,
  address =		  {Reading, MA}
}

@Article{sumii01:hybrid-pe,
  author = 		  {Eijiro Sumii and Naoki Kobayashi},
  title = 		  {A Hybrid Approach to Online and Offline Partial Evaluation},
  journal = 	  {Higher-Order and Symbolic Computation},
  year = 		  2001,
  volume =		  14,
  number =		  {2/3},
  pages =		  {101--142}
}

%% T %%


@Article{tait:intensional,
  author = 		  {William W. Tait},
  title = 		  {Intensional interpretation of functionals of finite type},
  journal = 	  {Journal of Symbolic Logic},
  year = 		  1967,
  volume =		  32,
  pages =		  {198--212}
}

@inproceedings{tarditi+:til,
  author =	 "David Tarditi and Greg Morrisett and Perry Cheng and
                  Chris Stone and Robert Harper and Peter Lee",
  title =	 "{TIL}: A Type-Directed Optimizing Compiler for {ML}",
  booktitle =	 1996 # " " # pldi,
  year =	 1996,
  month =	 may,
  pages =	 "181--192",
}


@PhdThesis{tarditi:phd,
  author = 	 {David Tarditi},
  title = 	 {Design and Implementation of Code Optimizations for a Type-Directed
Compiler for Standard ML},
  school = 	 {Carnegie Mellon School of Computer Science},
  year = 	 1996,
  note =	 {Available as CMU-CS-97-108}
}

@Article{talpin+:type-effect,
  author = 	 {J.-P. Talpin and P. Jouvelot},
  title = 	 {The Type and Effect Discipline},
  journal = 	 {Information and Computation},
  year = 	 1994,
  volume =	 111,
  number =	 2,
  pages =	 {245--296}
}

@Article{tennenhouse97survey,
  author =	 "D. Tennenhouse and J. Smith and W. Sincoskie and
                  D. Wetherall and G. Minden",
  title =	 "A Survey of Active Network Research",
  booktitle =	 {IEEE Communications Magazine},
  pages =	 {80--86},
  month =	 jan,
  volume =	 35,
  number =	 1,
  year =	 1997
}


@article{ tennenhouse96towards,
    author = "David L. Tennenhouse and David J. Wetherall",
    title = "Towards an Active Network Architecture",
    journal = "Computer Communication Review",
    volume = "26",
    number = "2",
    year = "1996",
    pages = "5--18",
    url = "citeseer.nj.nec.com/tennenhouse96towards.html" 
}


@InProceedings{thiemann01,
  author = 		  { Peter Thiemann},
  title = 		  { Enforcing Security Properties by Type Specialization },
  booktitle = 	  {  European Symposium on Programming (ESOP'01) },
  year =			  2001,
  volume =		  2028,
  series =		  lncs,
  address =		  {Genova, Italy },
  month =		  apr,
  publisher =	  {Springer-Verlag}
}


@InProceedings{tuiryn:subtyping-undecidable,
  author = 		  {Jerzy Tiuryn and Pawel Urzyczyn},
  title = 		  { The subtyping problem for second-order types is undecidable.},
  booktitle = 	  {Proceedings of the IEEE Symposion on Logic in Computer Science (LICS 96)},
  pages =		  {74--85},
  year =			  1996,
  address =		  {New Brunswick, New Jersey},
  publisher =	  {IEEE Computer Society Press}
}

@inproceedings{tofte:higher-order-modules,
  author =	 "Mads Tofte",
  title =	 "Principal Signatures for Higher-Order Program
                  Modules",
  booktitle =	 o19 # " " # popl,
  year =	 1992,
  month =	 jan,
  pages =	 "189--199",
}

@article{tofte:polymorphic-refs,
  author =	 "Mads Tofte",
  title =	 "Type Inference for Polymorphic References",
  journal =	 iandc,
  volume =	 89,
  pages =	 "1--34",
  year =	 1990,
  month =	 nov,
}

@inproceedings{tolmach:tagless-gc,
  author =	 "Andrew Tolmach",
  title =	 "Tag-Free Garbage Collection Using Explicit Type
                  Parameters",
  booktitle =	 1994 # " " # lfp,
  month =	 jun,
  pages =	 "1--11",
  year =	 1994,
  address =	 "Orlando"
}

@InProceedings{vanderwaart+:datatypes,
  author = 	 {Joseph C. Vanderwaart and Derek Dreyer and Leaf Petersen and Karl Crary and Robert Harper and Perry Cheng},
  title = 	 {Typed Compilation of Recursive Datatypes},
  booktitle = 	 {{ACM} {SIGPLAN} Workshop on Types in Language Design and Implementation},
  year =	 2003,
  address =	 {New Orleans, USA},
  month =	 jan
}

%% U %%

%% V %%


@techreport{van-renesse+:horus,
  author =	 "Robbert van Renesse and Takako M. Hickey and Kenneth
                  P. Birman",
  title =	 "Design and Performance of {H}orus: A Lightweight
                  Group Communications System",
  institution =	 cornell-cs,
  year =	 1994,
  month =	 aug,
  number =	 "TR 94-1442",
}


@MastersThesis{vestin:polytypic-ga,
  author = 		  {M\o{a}ns Vestin},
  title = 		  {Genetic algorithms in {H}askell with polytypic programming},
  school = 		  {G\"{o}teborg University},
  year = 		  1997
}

@inproceedings{viswanathan:fully-abstract-objs,
  author =	 "Ramesh Viswanathan",
  title =	 "Full Abstraction for First-Order Objects with
                  Recursive Types and Subtyping",
  booktitle =	 o13 # " " # lics,
  year =	 1998,
  month =	 jun,
  address =	 "Indianapolis",
}

%% W %%

@InProceedings{wadler+:type-classes,
  author =	 {Philip Wadler and Stephen Blott},
  title =	 {How to make Ad-hoc Polymorphism less ad-hoc},
  booktitle =	 o16 # " " # popl,
  pages =	 {60--76},
  year =	 1989,
  publisher =	 {ACM Press}
}

@inproceedings{wadler:comprehending-monads,
  author =	 "Philip Wadler",
  title =	 "Comprehending Monads",
  year =	 1992,
  booktitle =	 "Mathematical Structures in Computer Science",
  volume =	 2,
  pages =	 "461--493",
  publisher =	 cambridge-press,
}

@inproceedings{wadler:effects-to-monads,
  author =	 "Philip Wadler",
  title =	 "The Marriage of Effects and Monads",
  booktitle =	 1998 # " " # icfp,
  year =	 1998,
  month =	 sep,
  address =	 "Baltimore",
  pages =	 "63--74"
}

@inproceedings{wadler:fnal-essence,
  author =	 "Philip Wadler",
  title =	 "The Essence of Functional Programming",
  booktitle =	 o19 # " " # popl,
  year =	 1992,
  month =	 jan,
  address =	 "Albuquerque, New Mexico",
}

@inproceedings{Wadler89,
  author =	 "Philip Wadler",
  title =	 "Theorems for Free!",
  booktitle =	 "FPCA89:" # " " # fpca,
  year =	 1989,
  month =	 sep,
    pages = "347--359",
  address =	 "London",
}

@inproceedings{wadler:linear-taste,
  author =	 "Philip Wadler",
  title =	 "A taste of linear logic",
  booktitle =	 "Mathematical Foundations of Computer Science",
  year =	 1993,
  publisher =	 springer,
  volume =	 711,
  series =	 lncs,
}

@inproceedings{wadler:linear-world,
  author =	 "Philip Wadler",
  title =	 "Linear types can change the world!",
  booktitle =	 "IFIP Working Conference on Programming Concepts and
                  Methods",
  address =	 "Sea of Galilee, Israel",
  month =	 apr,
  year =	 1990,
  publisher =	 noholland,
}

@inproceedings{wahbe+:sfi,
  title =	 "Efficient Software-Based Fault Isolation",
  author =	 "Robert Wahbe and Steven Lucco and Thomas Anderson
                  and Susan Graham",
  booktitle =	 o14 # " " # sosp,
  year =	 1993,
  month =	 dec,
  pages =	 "203--216",
  address =	 "Asheville",
}

@TechReport{walker00recursive-alias,
  author =	 {David Walker and Greg Morrisett},
  title =	 {Alias Types for Recursive Data Structures},
  institution =	 cornell-cs,
  year =	 2000,
  number =	 {TR2000-1787},
  address =	 ith-ny,
  month =	 mar,
  note =	 {submitted for publication}
}


@InProceedings{walker00,
  author = 	 {David Walker},
  title = 	 {A Type System for Expressive Security Policies},
  booktitle = 	 {Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages 
January 19 - 21, 2000, Boston, MA USA},
  pages =	 {254--267},
  year =	 2000,
  publisher =	 {ACM Press}
}

@InProceedings{watanabe+:reflection-oo,
  author = 		  {Takuo Watanabe and Akinori Yonezawa},
  title = 		  {Reflection in an Object-Oriented Concurrent Language},
  booktitle = 	  oopsla,
  pages =		  {306--315},
  year =			  1988
}

@inproceedings{wand:hoal,
  author =	 "Mitchell Wand",
  title =	 "Correctness of Procedure Representations in
                  Higher-Order Assembly Language",
  booktitle =	 mfps,
  year =	 1991,
  volume =	 598,
  publisher =	 springer,
  series =	 1992,
  pages =	 "294--311",
}



@TechReport{washburn+:itaname-tr,
  author = 		  {Geoffrey Washburn and Stephanie Weirich},
  title = 		  {Unifying nominal and structural ad-hoc polymorphism (Extended version)},
  institution =  {University of Pennsylvania},
  year = 		  2004, 
  note =         { Available at \url{http://www.cis.upenn.edu/~sweirich/} }
}

@Article{wells:typability,
  author = 		  {Joe B. Wells},
  title = 		  {Typability and type checking in System {F} are equivalent and undecidable},
  journal = 	  {Ann. Pure Appl. Logic},
  year = 		  1999,
  volume =		  98,
  number =		  {1--3},
  pages =		  {111--156}
}

@book{whitehead+:principia,
  author =	 "Alfred North Whitehead and Bertrand Russell",
  title =	 "Principia Mathematica",
  publisher =	 cambridge-press,
  year =	 "1910",
  edition =	 "2nd",
}

@InProceedings{wickline98rtcg,
  author = 	 {Philip Wickline and Peter Lee and Frank Pfenning},
  title = 	 {Run-time Code Generation and Modal-{ML}},
  booktitle = 	 1998 # " " # pldi,
  pages =	 {224--235},
  year =	 1998,
  month =	 jun,
  organization = {ACM SIGPLAN}
}

@article{wright+:syntactic-soundness,
  author =	 "Andrew K. Wright and Matthias Felleisen",
  title =	 "A Syntactic Approach to Type Soundness",
  journal =	 iandc,
  volume =	 115,
  pages =	 "38--94",
  year =	 1994,
}

@article{wright:value-restriction,
  author =	 "Andrew K. Wright",
  title =	 "Simple Imperative Polymorphism",
  journal =	 "Lisp and Symbolic Computation",
  volume =	 8,
  number =	 4,
  month =	 dec,
  year =	 1995,
  pages =	 "343--356",
}


%% X %%
@inproceedings{xi+:dependent-types-practical,
  author =	 "Hongwei Xi and Frank Pfenning",
  title =	 "Dependent Types in Practical Programming",
  booktitle =	 o26 # " " # popl,
  address =	 "San Antonio, Texas",
  month =	 jan,
  year =	 1999,
  pages =	 "214--227",
}

@PhdThesis{xi:phd,
  author =	 {Hongwei Xi},
  title =	 {Dependent Types in Practical Programming},
  school =	 {Carnegie Mellon University},
  year =	 1998,
  address =	 {Pittsburgh, PA},
  month =	 sep
}



@InProceedings{xi+:guarded-datatype,
  author = 		  {Hongwei Xi and Chiyan Chen and Gang Chen},
  title = 		  {Guarded Recursive Datatype Constructors},
  booktitle =	  o30 # " " # popl,
  pages =		  {224--235},
  year =			  2003,
  address =		  {New Orleans, LA, USA},
  month =		  jan
}

%% Y %%

@InProceedings{yang:encoding_types,
  author = 	 {Zhe Yang},
  title = 	 {Encoding Types in {ML}-like languages},
  booktitle = 	 1998 # " " # icfp,
  year =	 1998,
  volume =	 34,
  series =	 {{ACM} {SIGPLAN} Notices}, 
  address =	 {Baltimore, MD},
  month =	 sep,
  pages = { 289--300 }
}

@inproceedings{ zenger01extensible,
    author = {Matthias Zenger and Martin Odersky},
    title = {Extensible Algebraic Datatypes with Defaults},
    year = 2001,
    month = "September",
    booktitle = "Proceedings of the International Conference on Functional Programming",
    address = {Firenze, Italy},
    url = {citeseer.nj.nec.com/zenger01extensible.html} }

%% Z %%



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@inproceedings{nanevski:namenec,
 author = {Aleksandar Nanevski},
 title = {Meta-programming with names and necessity},
 booktitle = {Proceedings of the seventh ACM SIGPLAN international conference on Functional programming},
 year = {2002},
 isbn = {1-58113-487-8},
 pages = {206--217},
 location = {Pittsburgh, PA, USA},
 doi = {http://doi.acm.org/10.1145/581478.581498},
 publisher = {ACM Press},
 }

@inproceedings{loh+:dependgen,
 author = {Andres L\"oh and Dave Clarke and Johan Jeuring},
 title = {Dependency-style Generic Haskell},
 booktitle = proc # o8 # icfp,
 year = 2003,
 pages = {141-152},
 location = {Uppsala, Sweden},
 }

@inproceedings{nanevsk:dynamic,
 author = {Aleksandar Nanevski},
 title = {From dynamic binding to state via modal possibility},
 booktitle = {Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming},
 year = {2003},
 isbn = {1-58113-705-2},
 pages = {207--218},
 location = {Uppsala, Sweden},
 doi = {http://doi.acm.org/10.1145/888251.888271},
 publisher = {ACM Press},
 }



@inproceedings{ambler+:hybrid,
  author = {Simon Ambler and Roy L. Crole and Alberto Momigliano},
  title     = {Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction},
  booktitle     = {Theorem Proving in Higher Order Logics, 15th International Conference,
               TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = 2410,
  year      = 2002,
  isbn      = {3-540-44039-9},
}

@Unpublished{washburn:modal-spec,
author = {Geoffrey Washburn},
title = {Modal Typing for Specifying Run-time Code Generation},
note = {Available from \url{http://www.cis.upenn.edu/~geoffw/research/}},
year = {2001}
}

@inproceedings{acar+:selective-mem,
  author =	 "Umut Acar and Guy Blelloch and Robert Harper",
  title =	 "Selective Memoization",
  booktitle =	 o30 # " " # popl,
  year =	 2002,
  month =	 jan,
  address =	 "New Orleans, LA",
}

@InProceedings{miller:mllam,
  author = 	 {Dale Miller},
  title = 	 {An Extension to {ML} to Handle Bound Variables in Data Structures: Preliminary Report},
  booktitle = 	 {Proceedings of the Logical Frameworks BRA Workshop},
  year =	 1990,
  month =	 may
}

@article{dp:modal-logic-comp,
  author =	 "Rowan Davies and Frank Pfenning",
  title =	 "A Modal Analysis of Staged Computation",
  journal =	 jacm,
  year =	 2001,
  volume =	 48,
  number =	 3,
  month =	 "May",
  pages =	 "555--604",
}

@inproceedings{pitts:fresh,
 author = {Andrew M. Pitts},
 title = {A fresh approach to representing syntax with static binders in functional programming},
 booktitle = {Proceedings of the sixth ACM SIGPLAN international conference on Functional programming},
 year = {2001},
 isbn = {1-58113-415-0},
 pages = {1--1},
 location = {Florence, Italy},
 doi = {http://doi.acm.org/10.1145/507635.507637},
 publisher = {ACM Press},
 }


@Unpublished{weirich:type-erasure,
  author = 		  {Stephanie Weirich},
  title = 		  {Higher-Order Intensional Type Analysis in Type-Erasure Semantics},
  note = 		  {Available from \url{http://www.cis.upenn.edu/~sweirich/}},
  year =			  2003
}


@inproceedings{lammel:boilerplate,
 author    = {Ralf L\"ammel and Simon {Peyton Jones}},
 title     = "Scrap your boilerplate:
              a practical design pattern for generic programming",
 year      = "2003",
 booktitle = "Proc.\ of the ACM SIGPLAN Workshop
              on Types in Language Design and Implementation (TLDI~2003)"
}


@inproceedings{dreyer+:modules,
 author = {Derek Dreyer and Karl Crary and Robert Harper},
 title = {A type system for higher-order modules},
 booktitle = proc # o30 # popl,
 year = {2003},
 isbn = {1-58113-628-5},
 pages = {236--249},
 location = {New Orleans, Louisiana, USA},
 doi = {http://doi.acm.org/10.1145/604131.604151},
 publisher = {ACM Press},
 }

@InProceedings{Leifer:2003:GAS,
  author =       "James J. Leifer and Gilles Peskine and Peter Sewell
                 and Keith Wansbrough",
  title =        "Global abstraction-safe marshalling with hash types",
  booktitle =    proc # o8 # icfp,
  year =         "2003",
  pages =        "87--98",
  address =      "Uppsala, Sweden"
} 

@TechReport{washburn+:mtr,
  author = 		  {Geoff Washburn and Stephanie Weirich},
  title = 		  {Unifying nominal and structural ad-hoc polymorphism},
  institution =  {University of Pennsylvania},
  year = 		  2003,
  note =			  {Available from \url{http://www.cis.upenn.edu/\~\ washburn/research/}}
}

@inproceedings{Remy:popl89,
  author       = "Didier Remy",
  title        = "Records and Variants as a natural Extension of {ML}",
  booktitle    = "Sixteenth Annual Symposium on
                  Principles Of Programming Languages",
  year         = 1989,
  note          = "Available from \url{http://doi.acm.org/10.1145/75277.75284}",
}


@TechReport{vytiniotis+:mtr,
  author = 	 {Dimitrios Vytiniotis and Geoffrey Washburn and Stephanie Weirich},
  title = 	 {An Open and Shut Typecase},
  institution =  {University of Pennsylvania},
  year = 	 {2004},
  number = 	 {MS-CIS-04-26},
  note = 	 {Available from \url{http://www.cis.upenn.edu/~dimitriv/itaname}}
}

@TechReport{zenger+:expression,
  author =       {Matthias Zenger and Martin Odersky.},
  title =        {Independently Extensible Solutions to the Expression Problem},
  institution =  {EPFL Lausanne, Switzerland},
  year =         2004,
  number =       {IC/2004/33}
}

@Book{Nipkow-Paulson-Wenzel:2002,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {LNCS},
  volume	= 2283,
  year		= 2002}


@inproceedings{mellies:rectypes,
 author = {Paul-Andr\'{e} Melli\`{e}s and J\'{e}r\^{o}me Vouillon},
 title = {Recursive Polymorphic Types and Parametricity in an Operational Framework},
 booktitle = {LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05)},
 year = {2005},
 isbn = {0-7695-2266-1},
 pages = {82--91},
 doi = {http://dx.doi.org/10.1109/LICS.2005.42},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
 }

@inproceedings{DBLP:conf/esop/Ahmed06,
  author    = {Amal J. Ahmed},
  title     = {Step-Indexed Syntactic Logical Relations for Recursive and
               Quantified Types.},
  booktitle = {ESOP},
  year      = {2006},
  pages     = {69-83},
  ee        = {http://dx.doi.org/10.1007/11693024_6},
  crossref  = {DBLP:conf/esop/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/esop/2006,
  editor    = {Peter Sestoft},
  title     = {Programming Languages and Systems, 15th European Symposium
               on Programming, ESOP 2006, Held as Part of the Joint European
               Conferences on Theory and Practice of Software, ETAPS 2006,
               Vienna, Austria, March 27-28, 2006, Proceedings},
  booktitle = {ESOP},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3924},
  year      = {2006},
  isbn      = {3-540-33095-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{appel01:indexed,
 author = {Andrew W. Appel and David McAllester},
 title = {An indexed model of recursive types for foundational proof-carrying code},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {23},
 number = {5},
 year = {2001},
 issn = {0164-0925},
 pages = {657--683},
 doi = {http://doi.acm.org/10.1145/504709.504712},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@Article{johann:higher-order-poly,
  author = 		  {Patricia Johann},
  title = 		  {On Proving the Correctness of Program Transformations based
on Free Theorems for Higher-Order Polymorphic Lambda
Calculi},
  journal = 	  {Math. Struct. Comp. Sci.},
  year = 		  2005,
  number =		  15,
  pages =		  {201--229}
}


@inproceedings{johann04:seq,
 author = {Johann, Patricia and Voigtl\"{a}nder, Janis},
 title = {Free theorems in the presence of seq},
 booktitle = {POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2004},
 isbn = {1-58113-729-X},
 pages = {99--110},
 location = {Venice, Italy},
 doi = {http://doi.acm.org/10.1145/964001.964010},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@InCollection{PittsAM:typor,
  author =	 {A. M. Pitts},
  title =	 {Typed Operational Reasoning},
  booktitle =	 {Advanced Topics in Types and Programming Languages},
  pages =	 {245--289},
  publisher =	 {The MIT Press},
  year =	 2005,
  editor =	 {B. C. Pierce},
  chapter =	 7,
  isbn =	 {0-262-16228-8}
}

@techreport{simonet-pottier:gadt-inference,
  AUTHOR = {Vincent Simonet and Fran\c{c}ois Pottier},
  TITLE = {Constraint-Based Type Inference with Guarded Algebraic Data Types},
  URL = {http://pauillac.inria.fr/~fpottier/publis/simonet-pottier-hmg.ps.gz},
  institution = {INRIA},
  MONTH = JUL,
  YEAR = {2003} }

@ARTICLE{simonet-pottier-hmg-toplas,
  AUTHOR = {Vincent Simonet and Francois Pottier},
  TITLE = {A Constraint-Based Approach to Guarded Algebraic Data
                 Types},
  MONTH = JAN,
  YEAR = {2007},
  JOURNAL = {ACM Transactions on Programming Languages and
                 Systems},
  VOLUME = {29},
  NUMBER = {1},
}




@article{         Pitts00,
author =          "Andrew M. Pitts",
title =           "Parametric polymorphism and operational equivalence",
journal =         "Mathematical Structures in Computer Science",
volume =          10,
pages =           "321--359",
year =            "2000"
}

@techreport{sulzmann+:eadts,
  author = "Martin Sulzmann and Jeremy Wazny and Peter Stuckey",
  title = "A framework for extended algebraic data types",
  year = 2005, 
  institution = "National University of Singapore",
  keywords = "GADT, type classes"
}


@inproceedings{spj+:gadt,
 author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
 title = {Simple unification-based type inference for {GADTs}},
 booktitle = {ICFP '06: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming},
 year = {2006},
 isbn = {1-59593-309-3},
 pages = {50--61},
 location = {Portland, Oregon, USA},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@inproceedings{sulzman+:eadts,
  author    = {Martin Sulzmann and
               Jeremy Wazny and
               Peter J. Stuckey},
  title     = {A Framework for Extended Algebraic Data Types.},
  booktitle = {FLOPS},
  year      = {2006},
  pages     = {47-64},
  ee        = {http://dx.doi.org/10.1007/11737414_5},
  crossref  = {DBLP:conf/flops/2006},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/flops/2006,
  editor    = {Masami Hagiya and
               Philip Wadler},
  title     = {Functional and Logic Programming, 8th International Symposium,
               FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings},
  booktitle = {FLOPS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3945},
  year      = {2006},
  isbn      = {3-540-33438-6},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{crary+:polyrecrelns,
 author = {Crary, Karl and Harper, Robert},
 title = {Syntactic Logical Relations for Polymorphic and Recursive Types},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {172},
 year = {2007},
 issn = {1571-0661},
 pages = {259--299},
 doi = {http://dx.doi.org/10.1016/j.entcs.2007.02.010},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 }


@INPROCEEDINGS{Was+Wei:2005,
  AUTHOR = {Geoffrey Washburn and Stephanie Weirich},
  TITLE = {Generalizing Parametricity Using Information Flow},
  BOOKTITLE = {The Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},  
  YEAR = 2005,
  MONTH = {June},
  PAGES = {62--71},
  ADDRESS = {Chicago, IL},
  ORGANIZATION = {{IEEE} Computer Society},  
  PUBLISHER= {{IEEE} Computer Society Press},	
  PDF = {http://www.cis.upenn.edu/~geoffw/research/papers/lics2005.pdf},
  PLCLUB = "yes",
  ABSTRACT = {
Run-time type analysis allows programmers to easily and concisely define
operations based upon type structure, such as serialization, iterators,
and structural equality.  However, when types can be inspected at run
time, nothing is secret.  A module writer cannot use type abstraction
to hide implementation details from clients: clients can determine the
structure of these supposedly ``abstract'' data types.  Furthermore,
access control mechanisms do not help isolate the implementation of
abstract datatypes from their clients.  Buggy or malicious authorized
modules may leak type information to unauthorized clients, so module
implementors cannot reliably tell which parts of a program rely on their
type definitions.

Currently, module implementors rely on parametric polymorphism to provide
integrity and confidentiality guarantees about their abstract datatypes.
However, standard parametricity does not hold for languages with run-time
type analysis; this paper shows how to generalize parametricity so
that it does.   The key is to augment the type system with annotations
about information-flow.  Implementors can then easily see which parts
of a program depend on the chosen implementation by tracking the flow
of dynamic type information.
  }
}

@incollection{cardelli91extension,
    author = "Luca Cardelli and John C. Mitchell and Simone Martini and Andre Scedrov",
    title = "An Extension of System {F} with Subtyping",
    booktitle = "Proc.\ of 1st Int.\ Symp.\ on Theor.\ Aspects of Computer Software, {TACS}'91, Sendai, Japan, 24--27 Sept 1991",
    volume = "526",
    publisher = "Springer-Verlag",
    address = "Berlin",
    editor = "Takayasu Ito and Albert R. Meyer",
    pages = "750--770",
    year = "1991",
    url = "citeseer.ist.psu.edu/cardelli91extension.html" }



@inproceedings{donnelly-xi:normalization,
  author    = {Kevin Donnelly and Hongwei Xi},
  title     = "A Formalization of Strong normalization for Simply Typed Lambda-Calculus and {System F}", 
  booktitle = {International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), Seattle, WA},
  year      = {2006},
  pages     = "98--113",
  month     = {Aug},
}


@techreport{sarnat-schuermann:lr,
  author = "Jeffrey Sarnat and Carsten Schurmann",
  title = "On the representation of logical relations in {Twelf}", 
  institution = "Yale University", 
  year = "2006",
  number = "YaleU/DCS/TR-1362"}



@article{harper-mitchell:joperator,
 author = {Robert Harper and John C. Mitchell},
 title = {Parametricity and variants of {Girard's} {J} operator},
 journal = {Inf. Process. Lett.},
 volume = {70},
 number = {1},
 year = {1999},
 issn = {0020-0190},
 pages = {1--5},
 doi = {http://dx.doi.org/10.1016/S0020-0190(99)00036-8},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 }


@PhDThesis{KucanThesis,
author =          "Jacov Ku\v{c}an ",
title =           "Metatheorems about Convertibility in Typed Lambda Calculi: Applications to CPS Transform and Free Theorems",
school =          "Massachusetts Institute of Technology",
month =           "February",
year =            "1997"
}



@TechReport{takeuti:lambda-cube,
  year =     {2001},
  month =    jun,
  author = 	 {Izumi Takeuti},
  title = 	 {The Theory of Parametricity in Lambda Cube (Towards new interaction between category theory and proof theory)},
  uri = {\url{http://hdl.handle.net/2433/41237}},
  institution = {Kyoto University Research Information Repository}
}


@article{vytiniotis:rtheorems,
 author = {Dimitrios Vytiniotis and Stephanie Weirich},
 title = {Free Theorems and Runtime Type Representations},
 journal = {Electron. Notes Theor. Comput. Sci.},
 volume = {173},
 year = {2007},
 issn = {1571-0661},
 pages = {357--373},
 doi = {http://dx.doi.org/10.1016/j.entcs.2007.02.043},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
}

@inproceedings{achten+:compositional-model-views,
  author    = {Peter Achten and
               Marko C. J. D. van Eekelen and
               Marinus J. Plasmeijer},
  title     = {Compositional Model-Views with Generic Graphical User Interfaces.},
  booktitle = {Practical Aspects of Declarative Languages, 6th International
               Symposium, PADL 2004, Dallas, TX, USA, June 18-19, 2004, Proceedings},
  pages     = {39-55},
  year      = {2004}, 
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3057{\&}spage=39},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{cheney:nameplate,
 author = {James Cheney},
 title = {Scrap your nameplate: (functional pearl)},
 booktitle = {ICFP '05: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming},
 year = {2005},
 isbn = {1-59593-064-7},
 pages = {180--191},
 location = {Tallinn, Estonia},
 doi = {http://doi.acm.org/10.1145/1086365.1086389},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }

@article{pfenning:logical-frameworks,
 author = {Frank Pfenning},
 title = {Logical frameworks},
 journal = {Handbook of automated reasoning},
 year = {2001},
 isbn = {0-444-50812-0},
 pages = {1063--1147},
 publisher = {Elsevier Science Publishers B. V.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 }


@inproceedings{baars+:tdt,
 author = {Arthur I. Baars and S. Doaitse Swierstra},
 title = {Typing dynamic typing},
 booktitle = {ICFP '02: Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming},
 year = {2002},
 isbn = {1-58113-487-8},
 pages = {157--166},
 location = {Pittsburgh, PA, USA},
 doi = {http://doi.acm.org/10.1145/581478.581494},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@inproceedings{cheney-hinze:lightweight-generics,
 author = {James Cheney and Ralf Hinze},
 title = {A lightweight implementation of generics and dynamics},
 booktitle = {Haskell '02: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell},
 year = {2002},
 isbn = {1-58113-605-6},
 pages = {90--104},
 location = {Pittsburgh, Pennsylvania},
 doi = {http://doi.acm.org/10.1145/581690.581698},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@inproceedings{lammel:syb-xpath,
 author = {Ralf L\"{a}mmel},
 title = {Scrap your boilerplate with {XPath}-like combinators},
 booktitle = {POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages},
 year = {2007},
 isbn = {1-59593-575-4},
 pages = {137--142},
 location = {Nice, France},
 doi = {http://doi.acm.org/10.1145/1190216.1190240},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@article{weirich:runtime,
 author = {Stephanie Weirich},
 title = {Type-safe run-time polytypic programming},
 journal = {Journal of Functional Programming},
 volume = {16},
 number = {6},
 year = {2006},
 issn = {0956-7968},
 pages = {681--710},
 doi = {http://dx.doi.org/10.1017/S0956796806005879},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@inproceedings{syb3,
 author = {Ralf L\"{a}mmel and Simon {Peyton Jones}},
 title = "{Scrap your boilerplate with class: extensible generic functions}",
 booktitle = "{Proceedings of the ACM SIGPLAN International Conference
               on Functional Programming (ICFP 2005)}",
 year      = {2005},
 pages     = {204--215},
 location  = {Tallinn, Estonia},
 publisher = {ACM Press},
 month = sep,
}

@inproceedings{generic-views,
  author = {Stefan Holdermans and Johan Jeuring and Andres L\"{o}h and Alexey Rodriguez}, 
  title  = {Generic Views on Data Types},
  booktitle     = {Mathematics of Program Construction, 
                   8th International Conference, MPC 2006, Kuressaare, Estonia, July 3-5, 2006, Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = 4014,
  year      = 2006,
  isbn      = {978-3-540-35631-8},
}


@article{harper-pfening:canforms,
 author = {Robert Harper and Frank Pfenning},
 title = {On equivalence and canonical forms in the {LF} type theory},
 journal = {ACM Trans. Comput. Logic},
 volume = {6},
 number = {1},
 year = {2005},
 issn = {1529-3785},
 pages = {61--101},
 doi = {http://doi.acm.org/10.1145/1042038.1042041},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 }


@inproceedings{Pau93a,
    Author = {Christine {Paulin-Mohring}},
    Booktitle = {International Conference on Typed Lambda Calculi and Applications, TLCA '93},
    Date-Modified = {2007-04-25 22:40:20 -0400},
    Pages = {328--345},
    Publisher = {Springer},
    Series = {Lecture Notes in Computer Science},
    Title = {Inductive Definitions in the System {Coq}: Rules and Properties},
    Volume = {664},
    Year = {1993}} 

@MANUAL{ghc,
  author = {The GHC team},
  title = {The {Glasgow Haskell} compiler},
  url = {http://www.haskell.org/ghc/}
}

@MANUAL{coq,
  author = {{The Coq Team}},
  title = {Coq},
  url = {http://coq.inria.fr}
}

@book{            CroleBook,
author =          "Roy Crole",
title =           "Categories for Types",
publisher =       "Cambridge University Press",
year =            "1994"
}


@inproceedings{dreyer:non-parametric,
 author = {Neis, Georg and Dreyer, Derek and Rossberg, Andreas},
 title = {Non-parametric parametricity},
 booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
 year = {2009},
 isbn = {978-1-60558-332-7},
 pages = {135--148},
 location = {Edinburgh, Scotland},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

# doi = {http://doi.acm.org/10.1145/1596550.1596572},

@inproceedings{voigtlander:type-constructor,
 author = {Voigtl\"{a}nder, Janis},
 title = {Free theorems involving type constructor classes: functional pearl},
 booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
 year = {2009},
 isbn = {978-1-60558-332-7},
 pages = {173--184},
 location = {Edinburgh, Scotland},
 doi = {http://doi.acm.org/10.1145/1596550.1596577},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@inproceedings{andersson+:fastandloose,
    abstract = {Functional programmers often reason about programs as if they were written in a total language, expecting the results to carry over to non-total (partial) languages. We justify such reasoning.Two languages are defined, one total and one partial, with identical syntax. The semantics of the partial language includes partial and infinite values, and all types are lifted, including the function spaces. A partial equivalence relation (PER) is then defined, the domain of which is the total subset of the partial language. For types not containing function spaces the PER relates equal values, and functions are related if they map related values to related values.It is proved that if two closed terms have the same semantics in the total language, then they have related semantics in the partial language. It is also shown that the PER gives rise to a bicartesian closed category which can be used to reason about values in the domain of the relation.},
    address = {New York, NY, USA},
    author = {Danielsson, Nils A. and Hughes, John and Jansson, Patrik and Gibbons, Jeremy},
    booktitle = {POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
    citeulike-article-id = {558255},
    citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1111037.1111056},
    citeulike-linkout-1 = {http://dx.doi.org/10.1145/1111037.1111056},
    comment = {* Concert Reading Group: 02/13/2006},
    doi = {10.1145/1111037.1111056},
    isbn = {1-59593-027-2},
    keywords = {rg-2006},
    location = {Charleston, South Carolina, USA},
    month = {January},
    number = {1},
    pages = {206--217},
    posted-at = {2009-08-17 19:18:44},
    priority = {2},
    publisher = {ACM},
    title = {Fast and loose reasoning is morally correct},
    url = {http://dx.doi.org/10.1145/1111037.1111056},
    volume = {41},
    year = {2006}
}

#  isbn = {978-1-60558-379-2},
#  doi = {http://doi.acm.org/10.1145/1480881.1480926},
@inproceedings{mongagu-remy:modules,
 author = {Montagu, Beno\^{\i}t and R\'{e}my, Didier},
 title = {Modeling abstract types in modules with open existential types},
 booktitle = {POPL '09: Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
 year = {2009},
 pages = {354--365},
 location = {Savannah, GA, USA},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@phdthesis{dreyer:thesis,
 author = {Dreyer, Derek},
 note = {Co-Chair-Harper, Robert and Co-Chair-Crary, Karl},
 title = {Understanding and evolving the {ML} module system},
 year = {2005},
 isbn = {0-542-01550-1},
 order_no = {AAI3166274},
 publisher = {Carnegie Mellon University},
 address = {Pittsburgh, PA, USA},
 }



@inproceedings{neis+:non-parametric,
 author = {Neis, Georg and Dreyer, Derek and Rossberg, Andreas},
 title = {Non-parametric parametricity},
 booktitle = {ICFP '09: Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming},
 year = {2009},
 isbn = {978-1-60558-332-7},
 pages = {135--148},
 location = {Edinburgh, Scotland},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

# isbn = {1-59593-064-7},
#  doi = {http://doi.acm.org/10.1145/1086365.1086372},
@inproceedings{dreyer:rec-param,
 author = {Dreyer, Derek},
 title = {Recursive type generativity},
 booktitle = {ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming},
 year = {2005},
 pages = {41--53},
 location = {Tallinn, Estonia},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

# doi = {http://doi.acm.org/10.1145/888251.888274},
@inproceedings{rossberg:generativity,
 author = {Rossberg, Andreas},
 title = {Generativity and dynamic opacity for abstract types},
 booktitle = {PPDP '03: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming},
 year = {2003},
 isbn = {1-58113-705-2},
 pages = {241--252},
 location = {Uppsala, Sweden},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@article{benje+:universes,
 author = {Benke, Marcin and Dybjer, Peter and Jansson, Patrik},
 title = {Universes for generic programs and proofs in dependent type theory},
 journal = {Nordic J. of Computing},
 volume = {10},
 number = {4},
 year = {2003},
 issn = {1236-6064},
 pages = {265--289},
 publisher = {Publishing Association Nordic Journal of Computing},
 address = {, Finland},
 }

#  doi = {http://doi.acm.org/10.1145/1190315.1190324},
#  isbn = {1-59593-393-X},
@inproceedings{sulzmann+:fc-paper,
 author = {Sulzmann, Martin and Chakravarty, Manuel M. T. and {Peyton Jones}, Simon and Donnelly, Kevin},
 title = {System {F} with type equality coercions},
 booktitle = {TLDI '07: Proceedings of the 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation},
 year = {2007},
 pages = {53--66},
 location = {Nice, Nice, France},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@article{haskell98,
  author = {Simon {Peyton Jones} and others},
  title = {The {Haskell} 98 Language and Libraries: The Revised Report},
  journal = {Journal of Functional Programming},
  volume = 13,
  number = 1,
  pages = {0--255},
  month = {Jan},
  year = 2003,
  note = {\url{http://www.haskell.org/definition/}},
}

# doi = {http://doi.acm.org/10.1145/1047659.1040306},
@article{chak+:types,
 author = {Chakravarty, Manuel M. T. and Keller, Gabriele and {Peyton Jones}, Simon and Marlow, Simon},
 title = {Associated types with class},
 journal = {SIGPLAN Not.},
 volume = {40},
 number = {1},
 year = {2005},
 issn = {0362-1340},
 pages = {1--13},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

#  doi = {http://doi.acm.org/10.1145/1086365.1086397},
#  isbn = {1-59593-064-7},
@inproceedings{chak+:synonyms,
 author = {Chakravarty, Manuel M. T. and Keller, Gabriele and {Peyton Jones}, Simon},
 title = {Associated type synonyms},
 booktitle = {ICFP '05: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming},
 year = {2005},
 pages = {241--253},
 location = {Tallinn, Estonia},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@inproceedings{Kiselyov09funwith,
    author = {Oleg Kiselyov and Simon {Peyton Jones} and {Chung-chieh} Shan},
    title = {Fun with type functions},
    booktitle = "Reflections on the work of CAR Hoare",
    editor = "Cliff Jones and Bill Roscoe",
    publisher = "Springer",
    year = {2010}
}

@inproceedings{russo:existentials,
 author = {Russo, Claudio V.},
 title = {Non-dependent Types for {Standard ML} Modules},
 booktitle = {PPDP '99: Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming},
 year = {1999},
 isbn = {3-540-66540-4},
 pages = {80--97},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


@book{sml-book,
 author = {Milner, Robin and Tofte, Mads and Macqueen, David},
 title = {The  Definition of Standard ML},
 year = {1997},
 isbn = {0262631814},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
 }



@article{dybjer:ind-rec,
  author = 		  {Peter Dybjer},
  title = 		  {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory},
  journal = 	          { Journal of Symbolic Logic},
  year = 		  2000,
  volume =		  65,
  number =		  2,
  pages =		  {525--549}
}

# isbn = {978-1-59593-919-7},
#  doi = {http://doi.acm.org/10.1145/1411204.1411215},
@inproceedings{shrijvers:open-tyfuns,
 author = {Schrijvers, Tom and {Peyton Jones}, Simon and Chakravarty, Manuel and Sulzmann, Martin},
 title = {Type checking with open type functions},
 booktitle = {ICFP '08: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming},
 year = {2008},
 pages = {51--62},
 location = {Victoria, BC, Canada},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

# doi = {http://dx.doi.org/10.1007/978-3-642-03359-9_6},
#  isbn = {978-3-642-03358-2},
@inproceedings{agda,
 author = {Bove, Ana and Dybjer, Peter and Norell, Ulf},
 title = {A Brief Overview of {Agda} --- A Functional Language with Dependent Types},
 booktitle = {TPHOLs '09: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics},
 year = {2009},
 pages = {73--78},
 location = {Munich, Germany},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
 }

@phdthesis{norell:thesis,
  author  = {Ulf Norell},
  title	  = {Towards a practical programming language based on dependent type
	     theory},
  school  = {Department of Computer Science and Engineering, Chalmers University of Technology},
  year	  = 2007,
  month	  = {September},
  address = {SE-412 96 G\"{o}teborg, Sweden}
}




@TechReport{lh05dmlproofs-tr,
  author = 	 {Daniel R. Licata and Robert Harper},
  title = 	 {A Formulation of Dependent {ML} with Explicit Equality Proofs},
  institution =  {Carnegie Mellon University Department of Computer Science},
  year = 	 {2005},
  number = 	 {CMU-CS-05-178},
}

#  doi = {http://doi.acm.org/10.1145/1053468.1053469},
#  issn = {0164-0925},
@article{shao+:certbin,
 author = {Shao, Zhong and Trifonov, Valery and Saha, Bratin and Papaspyrou, Nikolaos},
 title = {A type system for certified binaries},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {27},
 number = {1},
 year = {2005},
 pages = {1--45},
 publisher = {ACM},
 address = {New York, NY, USA},
 }


@BOOK{ATTAPL,
  EDITOR = {Benjamin C. Pierce},
  TITLE = {Advanced Topics in Types and Programming Languages},
  PUBLISHER = {MIT Press},
  YEAR = 2005,
  PLCLUB = {Yes},
  BCP = {Yes},
  KEYS = {books},
  HOMEPAGE = {http://www.cis.upenn.edu/~bcpierce/attapl}
}

@inproceedings{weirich+:fc2,
 author = {Weirich, Stephanie and Vytiniotis, Dimitrios and Peyton Jones, Simon and Zdancewic, Steve},
 title = {Generative type abstraction and type-level computation},
 booktitle = {Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on {Principles} of {Programming} {Languages}},
 series = {POPL '11},
 year = {2011},
 isbn = {978-1-4503-0490-0},
 location = {Austin, Texas, USA},
 pages = {227--240},
 numpages = {14},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {haskell, newtype deriving, type functions},
} 




@inproceedings{HarperM95,
  author = {Robert Harper and Greg Morrisett},
  title = {Compiling polymorphism using intensional type analysis},
  booktitle = {POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  year = {1995},
  isbn = {0-89791-692-1},
  pages = {130--141},
  location = {San Francisco, California, United States},
  publisher = {ACM},
  address = {New York, NY, USA},
  ps = {http://www.eecs.harvard.edu/~greg/papers/ip-popl.ps}
}



@inproceedings{Altenkirch:ott,
 author = {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
 title = {Observational equality, now!},
 booktitle = {Proceedings of the 2007 workshop on Programming languages meets program verification},
 series = {PLPV '07},
 year = {2007},
 isbn = {978-1-59593-677-6},
 location = {Freiburg, Germany},
 pages = {57--68},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1292597.1292608},
 doi = {http://doi.acm.org/10.1145/1292597.1292608},
 acmid = {1292608},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {equality, type theory},
} 


@article{ott1,
author = {Thorsten Altenkirch and Conor McBride},
title = {Towards Observational Type Theory},
masid = {4008452}
}

@inproceedings{Miquel:icc,
 author = {Miquel, Alexandre},
 title = {The implicit calculus of constructions: extending pure type systems with an intersection type binder and subtyping},
 booktitle = {Proceedings of the 5th international conference on Typed lambda calculi and applications},
 series = {TLCA'01},
 year = {2001},
 isbn = {3-540-41960-8},
 location = {Krak\&\#243;w, Poland},
 pages = {344--359},
 numpages = {16},
 url = {http://portal.acm.org/citation.cfm?id=1754621.1754650},
 acmid = {1754650},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 


@inproceedings{barras:icc,
author = {Bruno Barras and Bruno Bernardo},
title = {The Implicit Calculus of Constructions as a Programming Language with Dependent Types},
booktitle = {Foundations of Software Science and Computation Structure},
year = {2008},
pages = {365--379},
doi = {10.1007/978-3-540-78499-9_26},
masid = {4259647}
}



@InProceedings{swamy+:fstar,
  author = 	 {Nikhil Swamy and Juan Chen and Cedric Fournet and Pierre-Yves Strub and Karthikeyan Bharagavan and Jean Yang},
  title = {Secure Distributed Programming with Value-dependent Types}, 
  booktitle = {Proceedings of the Sixteenth {ACM SIGPLAN} International Conference on Functional Programming (ICFP '11)},
  year = 	 2011,
  month = 	 {September},
  note = 	 {To appear.}
}


@inproceedings{tldi12,
  author = {Yorgey, Brent A. and Weirich, Stephanie and Cretin, Julien and 
           Peyton Jones, Simon and Vytiniotis, Dimitrios and
           Magalh\~aes, Jos\'e Pedro},
  title = {Giving {Haskell} a Promotion},
  booktitle = {Proceedings of the 8th ACM SIGPLAN workshop on Types in
              language design and implementation},
  series = {TLDI '12},
  year = {2012},
  location = {Philadelphia, PA, USA},
  pages = {53--66},
  doi = {10.1145/2103786.2103795},
  publisher = {ACM},
  address = {New York, NY, USA},
}

@inproceedings{flanagan-hybrid,
 author = {Flanagan, Cormac},
 title = {Hybrid type checking},
 booktitle = {Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
 series = {POPL '06},
 year = {2006},
 isbn = {1-59593-027-2},
 location = {Charleston, South Carolina, USA},
 pages = {245--256},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/1111037.1111059},
 doi = {http://doi.acm.org/10.1145/1111037.1111059},
 acmid = {1111059},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {contracts, dynamic checking, static checking, type systems},
} 

@inproceedings{wadler-blame-calculus,
 author = {Wadler, Philip and Findler, Robert Bruce},
 title = {Well-Typed Programs Can't Be Blamed},
 booktitle = {Proceedings of the 18th European Symposium on Programming Languages and Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009},
 series = {ESOP '09},
 year = {2009},
 isbn = {978-3-642-00589-3},
 location = {York, UK},
 pages = {1--16},
 numpages = {16},
 url = {http://dx.doi.org/10.1007/978-3-642-00590-9_1},
 doi = {http://dx.doi.org/10.1007/978-3-642-00590-9_1},
 acmid = {1532976},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 


@inproceedings{blame-for-all,
 author = {Ahmed, Amal and Findler, Robert Bruce and Matthews, Jacob and Wadler, Philip},
 title = {Blame for all},
 booktitle = {Proceedings for the 1st workshop on Script to Program Evolution},
 series = {STOP '09},
 year = {2009},
 isbn = {978-1-60558-543-7},
 location = {Genova, Italy},
 pages = {1--13},
 numpages = {13},
 url = {http://doi.acm.org/10.1145/1570506.1570507},
 doi = {http://doi.acm.org/10.1145/1570506.1570507},
 acmid = {1570507},
 publisher = {ACM},
 address = {New York, NY, USA},
} 


@InProceedings{siek08:_gradual_inference,
  author = 	 {Jeremy G. Siek and Manish Vachharajani},
  title = 	 {Gradual Typing with Unification-based Inference},
  booktitle =	 {Dynamic Languages Symposium},
  abstract = {Static and dynamic type systems have well-known strengths and
weaknesses. Gradual typing provides the benefits of both in a
single language by giving the programmer control over which portions
of the program are statically checked based on the presence or absence
of type annotations.  This paper studies the combination of gradual
typing and unification-based type inference with the goal of
developing a system that helps programmers increase the amount of
static checking in their program.  The key question in combining
gradual typing and type inference is how should the dynamic type of a
gradual system interact with the type variables of a type inference
system. This paper explores the design space and shows why three
straightforward approaches fail to meet our design goals.  This paper
presents a new type system based on the idea that a solution for a
type variable should be as informative as any type that constrains the
variable.  The paper also develops an efficient inference algorithm
and proves it sound and complete with respect to the type system.
},
  year =	 2008,
  month = {July}
}


@InProceedings{siek06:_gradual,
author = {Jeremy G. Siek and Walid Taha},
title = {Gradual typing for functional languages},
booktitle = {Scheme and Functional Programming Workshop},
year = 2006,
month = {September} 
}


@article{type-error-slicing,
 author = {Haack, Christian and Wells, J. B.},
 title = {Type error slicing in implicitly typed higher-order languages},
 journal = {Sci. Comput. Program.},
 volume = {50},
 issue = {1-3},
 month = {March},
 year = {2004},
 issn = {0167-6423},
 pages = {189--224},
 numpages = {36},
 url = {http://dl.acm.org/citation.cfm?id=989777.989786},
 doi = {10.1016/j.scico.2004.01.004},
 acmid = {989786},
 publisher = {Elsevier North-Holland, Inc.},
 address = {Amsterdam, The Netherlands, The Netherlands},
 keywords = {intersection types, type error location, type inference},
} 


@inproceedings{Tobin-Hochstadt:migration,
 author = {Tobin-Hochstadt, Sam and Felleisen, Matthias},
 title = {Interlanguage migration: from scripts to programs},
 booktitle = {Companion to the 21st ACM SIGPLAN symposium on Object-oriented programming systems, languages, and applications},
 series = {OOPSLA '06},
 year = {2006},
 isbn = {1-59593-491-X},
 location = {Portland, Oregon, USA},
 pages = {964--974},
 numpages = {11},
 url = {http://doi.acm.org/10.1145/1176617.1176755},
 doi = {http://doi.acm.org/10.1145/1176617.1176755},
 acmid = {1176755},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {{\$\lambda\$}-calculus, contract, interlanguage migration, module systems},
} 

@book{MacLaneS:catwm,
 author		= {Mac Lane, Saunders},
 title		= {Categories for the Working Mathematician},
 publisher	= {Springer-Verlag},
 series		= {Graduate Texts in Mathematics},
 number		= 5,
 year		= 1971,
 isbn		= 0387900357}

@inproceedings{Licata:2012:CTT:2103656.2103697,
 author = {Licata, Daniel R. and Harper, Robert},
 title = {Canonicity for 2-dimensional type theory},
 booktitle = {Proceedings of the 39th annual ACM SIGPLAN-SIGACT {Symposium} on {Principles} of {Programming} {Languages}},
 series = {POPL '12},
 year = {2012},
 isbn = {978-1-4503-1083-3},
 location = {Philadelphia, PA, USA},
 pages = {337--348},
 numpages = {12},
 url = {http://doi.acm.org/10.1145/2103656.2103697},
 doi = {10.1145/2103656.2103697},
 acmid = {2103697},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {category theory, dependent types, homotopy type theory, type theory},
} 

@book{Baader:1998:TR:280474,
 author = {Baader, Franz and Nipkow, Tobias},
 title = {Term rewriting and all that},
 year = {1998},
 isbn = {0-521-45520-0},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 


@inproceedings{Dershowitz:1983:AR:1623516.1623594,
 author = {Dershowitz, Nachum and Hsiang, Jien and Josephson, N. Alan and Plaisted, David A.},
 title = {Associative-commutative rewriting},
 booktitle = {Proceedings of the Eighth international joint conference on Artificial intelligence - Volume 2},
 series = {IJCAI'83},
 year = {1983},
 location = {Karlsruhe, West Germany},
 pages = {940--944},
 numpages = {5},
 url = {http://dl.acm.org/citation.cfm?id=1623516.1623594},
 acmid = {1623594},
 publisher = {Morgan Kaufmann Publishers Inc.},
 address = {San Francisco, CA, USA},
} 

@article{Bachmair:1985:TOA:6947.6948,
 author = {Bachmair, Leo and Plaisted, David A.},
 title = {Termination orderings for associative-commutative rewriting systems},
 journal = {J. Symb. Comput.},
 issue_date = {Dec. 1985},
 volume = {1},
 number = {4},
 month = dec,
 year = {1985},
 issn = {0747-7171},
 pages = {329--349},
 numpages = {21},
 url = {http://dx.doi.org/10.1016/S0747-7171(85)80019-5},
 doi = {10.1016/S0747-7171(85)80019-5},
 acmid = {6948},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
}