@phdthesis{ brady-thesis,
    author = {Edwin Brady},
    title = {Practical Implementation of a Dependently Typed Functional Programming Language},
    year = 2005,
    school = {University of Durham}
}

@article{view-left,
   journal = {Journal of Functional Programming},
   number = {1},
   volume = {14},
   title = {The View From The Left},
   year = {2004},
   author = {Conor McBride and James McKinna},
   pages = {69--111}
}

@misc{epigram-afp,
    author = {Conor McBride},
    title = {Epigram: Practical Programming with Dependent Types},
    year = {2004},
    howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
}

@misc{coq-manual,
   howpublished = {\verb+http://coq.inria.fr/+},
   title = {The {Coq} Proof Assistant --- Reference Manual},
   year = {2004},
   author = {{Coq Development Team}}
}

@inproceedings{extraction-coq,
   title = {A New Extraction for {Coq}},
   year = {2002},
   booktitle = {Types for proofs and programs},
   editor = {Herman Geuvers and Freek Wiedijk},
   publisher = {Springer},
   author = {Pierre Letouzey},
   series = {LNCS}
}

@techreport{lego-manual,
   title = {\textsc{Lego} Proof Development System: User's Manual},
   year = {1992},
   institution = {Department of Computer Science, University of Edinburgh},
   author = {Zhaohui Luo and Robert Pollack}
}

@book{luo94,
   title = {Computation and Reasoning -- A Type Theory for Computer Science},
   year = {1994},
   publisher = {OUP},
   author = {Zhaohui Luo},
   series = {International Series of Monographs on Computer Science}
}

@phdthesis{goguen-thesis,
   school = {University of Edinburgh},
   title = {A Typed Operational Semantics for Type Theory},
   year = {1994},
   author = {Healfdene Goguen}
}

@phdthesis{mcbride-thesis,
   month = {May},
   school = {University of Edinburgh},
   title = {Dependently Typed Functional Programs and their         proofs},
   year = {2000},
   author = {Conor McBride}
}

@misc{mckinnabrady-phase,
   title = {Phase Distinctions in the Compilation of {Epigram}},
   year = 2005,
   author = {James McKinna and Edwin Brady},
   note = {Draft}
}

@article{pugh-omega,
   title =  "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis", 
   author = "William Pugh", 
   journal = "Communication of the ACM", 
   year = 1992, 
   pages = {102--114}
}

@Article{RegionTypes,
  refkey =       "C1753",
  title =        "Region-Based Memory Management",
  author =       "M. Tofte and J.-P. Talpin",
  pages =        "109--176",
  journal =      "Information and Computation",
  month =        "1~" # feb,
  year =         "1997",
  volume =       "132",
  number =       "2"
}

@phdthesis{ pedro-thesis,
    author = {Pedro Vasconcelos},
    title = {Space Cost Modelling for Concurrent Resource Sensitive Systems},
    year = 2006,
    school = {University of St Andrews}
}

@book{curry-feys,
   title = {Combinatory Logic, volume 1},
   year = {1958},
   publisher = {North Holland},
   author = {Haskell B. Curry and Robert Feys}
}
@inproceedings{howard,
   title = {The formulae-as-types notion of construction},
   year = {1980},
   booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
   editor = {Jonathan P. Seldin and J. Roger Hindley},
   publisher = {Academic Press},
   author = {William A. Howard},
   note = {A reprint of an unpublished manuscript from 1969}
}

@misc{ydtm,
    author = {Thorsten Altenkirch and Conor McBride and James McKinna},
    title = {Why Dependent Types Matter},
    note = {Submitted for publication},
    year = 2005}

@inproceedings{regular-types,
    author = { Peter Morris and Conor McBride and Thorsten Altenkirch},
    title = {Exploring The Regular Tree Types},
    year = 2005,
    booktitle = {Types for Proofs and Programs 2004}
}

@inproceedings{xi_arraybounds,
author = "Hongwei Xi and Frank Pfenning",
title = {Eliminating Array Bound Checking through Dependent Types},
booktitle = "Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation",
year = 1998,
month = "June",
address = "Montreal",
pages = "249--257",
}

@misc{interp-cayenne,
   url = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
   title = {An exercise in dependent types: A well-typed interpreter},
   year = {1999},
   author = {Lennart Augustsson and Magnus Carlsson}
}