@article{benkedybjerjansson2003:gendepty,
  author =	 {Marcin Benke and Peter Dybjer and Patrik Jansson},
  title =	 {Universes for Generic Programs and Proofs in
                  Dependent Type Theory},
  volume =	 10,
  number =	 4,
  year =	 2003,
  issn =	 {1236-6064},
  pages =	 {265--289},
  publisher =	 {Publishing Association Nordic Journal of Computing},
  address =	 {Finland}
}




@InCollection{ADJ:initial,
  author =	 {J. Goguen and J. Thatcher and E. Wagner},
  title =	 {An Initial Algebra Approach to the Specification,
                  correctness, and Implementation of Abstract Data
                  Types},
  booktitle =	 {Current Trends in Programming Methodology},
  pages =	 {80-149},
  publisher =	 {Prentice-Hall},
  year =	 1978,
  editor =	 {R. Yeh},
  volume =	 4
}

@InProceedings{AMB02,
  author =	 "T. Altenkirch and C. McBride",
  title =	 "Generic Programming within Dependently Typed
                  Programming",
  editor =	 "J. Gibbons and J. Jeuring",
  booktitle =	 "Pre-Proc. WCGP'02",
  year =	 2002,
  note =	 "(Final proc. to be published by Kluwer Acad.~Publ.)",
}

@Unpublished{Benke00,
  author =	 {M. Benke},
  title =	 {Automatic deriving of properties of algebraic
                  datatypes in {Martin-L\"of} type theory},
  note =	 {Presentation at Annual ESPRIT BRA TYPES Meeting,
                  Durham. Submitted for publication},
  year =	 2000,
  month =	 {December}
}



@InProceedings{Benke01c,
  author =	 {M. Benke},
  title =	 {Some tools for computer-assisted theorem proving in
                  {Martin-L\"of} type theory},
  booktitle =	 {TPHOLs --- Supplemental Proceedings},
  year =	 2001,
  editor =	 {R. J. Boulton and P. B. Jackson},
  organization = {University of Edinburgh}
}

@Unpublished{Benke02,
  author =	 {M. Benke},
  title =	 {Towards generic programming in type theory},
  note =	 {Presentation at Annual ESPRIT BRA TYPES Meeting,
                  Berg en Dal. Submitted for publication, available
                  from
                  \texttt{http://www.cse.chalmers.se/\hskip0pt\textasciitilde{}marcin/Papers/Notes/nijmegen.ps.gz}},
  year =	 2002,
  month =	 {April}
}

@article{DybjerP:indf,
  author =	 "P. Dybjer",
  title =	 "Inductive Families",
  journal =	 "Formal Aspects of Computing",
  volume =	 6,
  pages =	 "440--465",
  year =	 1994
}

@incollection{DybjerP:indsfm,
  author =	 "P. Dybjer",
  booktitle =	 "Logical Frameworks",
  title =	 "Inductive sets and families in {Martin-L{\"o}f's}
                  Type Theory and their set-theoretic semantics",
  year =	 1991,
  publisher =	 "Cambridge University Press",
  editor =	 "G. Huet and G. Plotkin",
  pages =	 "280--306"
}

@InProceedings{HallgrenRanta00,
  author =	 {T. Hallgren and A. Ranta},
  title =	 {An Extensible Proof Text Editor},
  booktitle =	 {Logic for Programming and Automated Reasoining},
  volume =	 1955,
  series =	 {LNCS},
  year =	 2000,
  publisher =	 {Springer},
  pages =	 {70--84}
}

@InCollection{PfeiferRuess99,
  author =	 "H. Pfeifer and H. Rue{\ss}",
  title =	 "Polytypic Proof Construction",
  editor =	 "Y. Bertot",
  booktitle =	 "Proc.\ TPHOLs'99",
  series =	 "LNCS",
  volume =	 1690,
  pages =	 "55--72",
  publisher =	 "Springer-Verlag",
  year =	 1999,
  url =
                  "http://www.informatik.uni-ulm.de/ki/Pfeifer/polytypic.ps.gz",
}


@inproceedings{augustsson:cayenne,
  AUTHOR =	 {L. Augustsson},
  TITLE =	 {{Cayenne --- a language with dependent types}},
  BOOKTITLE =	 {Proc.\ ICFP'98},
  PUBLISHER =	 {ACM Press},
  MONTH =	 {September},
  YEAR =	 1998
}


@inproceedings{backhouse91a,
  AUTHOR =	 "Backhouse, R.C. and others",
  TITLE =	 "Relational catamorphisms",
  BOOKTITLE =	 "Constructing Programs from Specifications",
  EDITOR =	 "B. M{\"o}ller",
  YEAR =	 1991,
  PUBLISHER =	 "North-Holland",
  PAGES =	 "287--318"
}

@inproceedings{backhouseetal98,
  AUTHOR =	 "Backhouse, R. and Jansson, P. and Jeuring, J. and
                  Meertens, L.",
  TITLE =	 "Generic Programming: An Introduction",
  booktitle =	 "Advanced Functional Programming",
  EDITORS =	 "Swierstra, S.D. and Henriques, P.R. and Oliveira,
                  J.N.",
  PAGES =	 "28--115",
  series =	 {LNCS},
  VOLUME =	 1608,
  PUBLISHER =	 {Springer Verlag},
  YEAR =	 1999
}


@PhdThesis{bayley:thesis,
  author =	 {A. Bayley},
  title =	 {The Machine-Checked Literate Formalisation of
                  Algebra in Type Theory},
  school =	 {University of Manchester},
  year =	 1998
}

@Article      {birddemoorhoogendijk93,
  title =	 {Generic functional programming with types and
                  relations},
  author =	 {R. Bird and O. de Moor and P. Hoogendijk},
  pages =	 {1--28},
  journal =	 "J. of {F}unc. {P}rog.",
  year =	 1996,
  volume =	 6,
  number =	 1
}

@article{bohmberarducci85,
  AUTHOR =	 "B{\"o}hm, C. and Berarducci, A.",
  TITLE =	 "Automatic synthesis of typed {$\Lambda$}-programs on
                  term algebras",
  JOURNAL =	 "Theoretical Computer Science",
  VOLUME =	 39,
  PAGES =	 "135--154",
  PUBLISHER =	 "North-Holland",
  YEAR =	 1985
}

@inproceedings{capretta:1999,
  author =	 "V. Capretta",
  title =	 "Universal Algebra in Type Theory",
  booktitle =	 "Proc.\ TPHOLs '99",
  editor =	 "Y. Bertot and others",
  pages =	 "131--148",
  publisher =	 "Springer-Verlag",
  series =	 "LNCS",
  volume =	 1690,
  year =	 1999
}

@inproceedings{capretta:2000,
  title =	 "Recursive Families of Inductive Types",
  author =	 "V. Capretta",
  booktitle =	 "Proc.\ TPHOLs 2000",
  editor =	 "J. Harrison and M. Aagaard",
  pages =	 "73--89",
  publisher =	 "Springer-Verlag",
  series =	 "LNCS",
  volume =	 1869,
  year =	 2000
}


@PhdThesis{capretta:thesis,
  author =	 {V. Capretta},
  title =	 {Abstraction and Computation},
  school =	 {Univ. of Nijmegen, the Netherlands},
  year =	 2002,
  month =	 {April}
}

@unpublished{agda-homepage,
  author =	 "Catharina Coquand",
  title =	 "{{The AGDA Proof System Homepage}}",
  year =	 1998,
  howpublished = {Online document},
  note =	 {\verb!http://www.cse.chalmers.se/~catarina/agda/!},
  documenturl =	 "http://www.cse.chalmers.se/~catarina/agda/"
}

@inproceedings{coquand:tallinn,
  author =	 "T. Coquand and C. Paulin",
  title =	 "Inductively defined types, preliminary version",
  booktitle =	 "COLOG '88, International Conference on Computer
                  Logic",
  series =	 "LNCS",
  volume =	 417,
  publisher =	 "Springer-Verlag",
  year =	 1990
}

@article{dybjer:apal,
  title =	 {Induction-Recursion and Initial Algebras},
  author =	 {Peter Dybjer and Anton Setzer},
  journal =	 {Annals of Pure and Applied Logic},
  volume =	 124,
  pages =	 {1--47},
  year =	 2003
}

@InProceedings{dybjer:dagstuhl,
  author =	 {P. Dybjer and A. Setzer},
  title =	 {Indexed Induction-Recursion},
  booktitle =	 {Proof Theory in Computer Science},
  pages =	 {93--113},
  year =	 2001,
  editor =	 {R. Kahle et al},
  volume =	 2183,
  series =	 {LNCS},
  month =	 {October},
  publisher =	 {Springer Verlag}
}



@article{dybjer:facs,
  author =	 "P. Dybjer",
  title =	 "Inductive Families",
  journal =	 "Formal Aspects of Computing",
  volume =	 6,
  pages =	 "440--465",
  year =	 1994
}

@Unpublished{dybjer:indexed,
  author =	 {P. Dybjer and A. Setzer},
  title =	 {Indexed Induction-Recursion},
  note =	 {long version, submitted for publication, available
                  from \verb!http://www.cse.chalmers.se/~peterd/!},
  year =	 2001
}

@article{dybjer:jsl,
  author =	 {P. Dybjer},
  title =	 {A General Formulation of Simultaneous
                  Inductive-Recursive Definitions in Type Theory},
  journal =	 {J. of Symbolic Logic},
  volum =	 65,
  number =	 2,
  month =	 {June},
  year =	 2000,
  pages =	 "525--549"
}

@InCollection{dybjer:laquila,
  author =	 "P. Dybjer and A. Setzer",
  title =	 "A Finite Axiomatization of Inductive-Recursive
                  Definitions",
  editor =	 "J.-Y. Girard",
  booktitle =	 "Proc.\ TLCA'99",
  series =	 "LNCS",
  volume =	 1581,
  pages =	 "129--146",
  publisher =	 "Springer-Verlag",
  address =	 "Berlin",
  year =	 1999,
  url =		 "http://www.math.uu.se/~setzer/articles/tlca99.ps.gz",
}

@incollection{dybjer:sophia,
  author =	 "P. Dybjer",
  booktitle =	 "Logical Frameworks",
  title =	 "Inductive sets and families in {Martin-L{\"o}f's}
                  Type Theory and their set-theoretic semantics",
  year =	 1991,
  publisher =	 "Cambridge University Press",
  editor =	 "G. Huet and G. Plotkin",
  pages =	 "280--306"
}

@Article{dybjer:well,
  author =	 {P. Dybjer},
  title =	 {Representing Inductively Defined Sets by
                  Wellorderings in {Martin-L\"of's} Type Theory},
  journal =	 {Theoretical Computer Science},
  year =	 1997,
  volume =	 176,
  pages =	 {329-335}
}

@Book{gratzer:book,
  author =	 {G. Grätzer},
  title =	 {Universal Algebra},
  publisher =	 {Springer-Verlag},
  year =	 1979,
  edition =	 {Second}
}

@Unpublished{hinzejeuring02:GenericHaskell,
  author =	 {Hinze, Ralf and Jeuring, Johan},
  title =	 {Generic {H}askell: Practice and Theory},
  booktitle =	 {Generic Programming, Advanced Lectures},
  series =	 LNCS,
  volume =	 2793,
  editors =	 {Roland Backhouse and Jeremy Gibbons},
  publisher =	 {Springer-{V}erlag},
  year =	 2003,
  pages =	 {1--56},
}

@PhdThesis{jansson-phdthesis,
  author =	 {Jansson, P.},
  title =	 {Functional Polytypic Programming},
  school =	 {Computing Science, Chalmers Univ. of Tech. and
                  Göteborg Univ., Sweden},
  month =	 may,
  isbn =	 {91-7197-895-X},
  year =	 2000
}

@Misc{janssonjeuring-polylib,
  TITLE =	 "{PolyLib} -- a polytypic function library",
  AUTHOR =	 "Jansson, P. and Jeuring, J.",
  howpublished = "Workshop on Generic Programming, Marstrand",
  documentURL =
                  "http://www.cse.chalmers.se/~patrikj/poly/polylib/polylib.ps.gz",
  month =	 "June",
  YEAR =	 1998
}


@inproceedings{janssonjeuring1997a,
  author =	 "Jansson, P. and Jeuring, J.",
  title =	 "Poly{P} --- a polytypic programming language
                  extension",
  booktitle =	 {Proc. {POPL}'97},
  publisher =	 "ACM Press",
  pages =	 "470--482",
  year =	 1997,
  documentURL =
                  "http://www.cse.chalmers.se/~patrikj/poly/polypPOPL97/"
}

@InCollection{jay-tlca,
  author =	 "Jay, C.B.",
  title =	 "Distinguishing Data Structures and Functions: The
                  Constructor Calculus and Functorial Types",
  editor =	 "S. Abramsky",
  booktitle =	 "Proc.\ TLCA'01",
  series =	 "LNCS",
  volume =	 2044,
  pages =	 "217--239",
  publisher =	 "Springer-Verlag",
  address =	 "Berlin",
  year =	 2001,
}

@article      {jayscp,
  AUTHOR =	 "Jay, C.B.",
  TITLE =	 "A semantics for shape",
  JOURNAL =	 "Science of Computer Programming",
  VOLUME =	 25,
  PAGES =	 "251--283",
  YEAR =	 1995
}

@book{martinlof:padova,
  author =	 "Martin-L{\"o}f, P.",
  title =	 "Intuitionistic Type Theory",
  year =	 1984,
  publisher =	 "Bibliopolis"
}

@MastersThesis{norell02:thesis,
  author =	 "U. Norell",
  title =	 "Functional Generic Programming and Type Theory",
  school =	 "Computing Science, Chalmers University of
                  Technology",
  year =	 2002,
  note =	 "Available from
                  \texttt{http://www.cse.chalmers.se/\textasciitilde{}ulfn}"
}

@inproceedings{petersson:manchester,
  author =	 "K. Petersson and D. Synek",
  title =	 "A Set Constructor for Inductive Sets in
                  {Martin-L{\"o}f's} Type Theory",
  booktitle =	 "Category Theory and Computer Science",
  publisher =	 "Springer-Verlag, LNCS 389",
  year =	 1989,
  pages =	 "128-140"
}

@PhdThesis{ruys:thesis,
  author =	 {M. Ruys},
  title =	 {Studies in Mechanical Verification of Mathematical
                  Proofs},
  school =	 {Katholieke Universiteit Nijmegen},
  year =	 1999
}