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

@inproceedings{cayenne,
    author = "Lennart Augustsson",
    title = "Cayenne - a Language with Dependent Types",
    booktitle = "International Conference on Functional Programming",
    pages = "239--250",
    year = "1998",
    url = "citeseer.nj.nec.com/augustsson98cayenne.html" 
}

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