@inproceedings{sheard-langfuture,
  author = {Tim Sheard},
  title = "Languages of the future",
  booktitle = "ACM Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA'04)",
  year = "2004"
}

@inproceedings{ivor,
  author = {Edwin Brady},
  title = {{Ivor}, a proof engine},
  year = {2007},
  publisher = {Springer},
  series = {LNCS},
  booktitle = {Implementation and Application of Functional Languages 2006},
  note = {To appear}
}

@misc{coq-in-coq,
  author = {Bruno Barras and Benjamin Werner},
  year = 1997,
  title = {{Coq} in {Coq}}
}

@article{hudak-edsl,
  author = {Paul Hudak},
  title = {Building Domain-Specific Embedded Languages},
  year = {1996},
  month = {December},
  journal = {ACM Computing Surveys},
  volume = {28A},
  number = {4}
}

@inproceedings{concon,
  author = {Conor McBride and Healfdene Goguen and James McKinna},
  title = {Some Constructions On Constructors},
  year = 2005,
  booktitle = {TYPES 2004},
  publisher = {Springer},
  series = {LNCS},
  volume = {3839}
}

@InProceedings{Hume-GPCE,
author = {K. Hammond and G.J. Michaelson},
title = {{Hume: a Domain-Specific Language for Real-Time Embedded Systems}},
booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'03)}},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
year = {2003},
}

@inproceedings{lcf-milner,
  author = {Robin Milner},
  title = {{LCF}: A Way of Doing Proofs with a Machine},
  booktitle = {Mathematical Foundations of Computer Science 1978},
  pages = {146-159},
  year = 1979,
  series = {LNCS},
  volume = {64}
}


@inproceedings{epireloaded,
  title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},
  author = {James Chapman and Thorsten Altenkirch and Conor McBride},
  year = 2006,
  booktitle = {Trends in Functional Programming 2005},
  note = {To appear}
}

@TECHREPORT{why-tool,
  AUTHOR = {J.-C. Filli\^atre},
  TITLE = {{Why: a multi-language multi-prover verification tool}},
  INSTITUTION = {{LRI, Universit\'e Paris Sud}},
  TYPE = {{Research Report}},
  NUMBER = {1366},
  MONTH = {March},
  YEAR = 2003,
  URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
}

@misc{ large-extraction,
  author = "Lu\'iz Cruz-Filipe and Bas Spitters",
  title = "Program Extraction from Large Proof Developments",
  year = 2003,
  url = "citeseer.ist.psu.edu/cruz-filipe03program.html" }

@inproceedings{ fta,
    author = "Herman Geuvers and Freek Wiedijk and Jan Zwanenburg",
    title = "A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals",
    booktitle = "{TYPES 2000}",
    pages = "96--111",
    year = "2000",
    url = "citeseer.ist.psu.edu/geuvers01constructive.html" }

@article{mckinna-expr,
   title = {A type-correct, stack-safe, provably correct, expression compiler in {Epigram}},
   author = {James McKinna and Joel Wright},
   year = 2007,
   journal = 	 {Journal of Functional Programming},
   note = {To appear}
}

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

@misc{four-colour,
  author = "Georges Gonthier",
  title = "A computer-checked proof of the {Four Colour Theorem}",
  year = 2005,
  howpublished = {\url{http://research.microsoft.com/~gonthier/4colproof.pdf}}}

@inproceedings{sparkle,
  author = "Maarten {de Mol} and Marko {van Eekelen} and Rinus Plasmeijer",
  title = "Theorem Proving for Functional Programmers",
  url = "citeseer.ist.psu.edu/654423.html",
  BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2002)},
  publisher = {Springer},
  series = {LNCS},
  volume = {2312},
  year = 2002
 }

@misc{agda,
   title = {Agda},
   author = {Catarina Coquand},
   howpublished= {\url{http://agda.sourceforge.net/}},
   year = 2005
}

@misc{cover,
   title = {Cover Translator},
   howpublished = {\url{http://coverproject.org/CoverTranslator/}}
}

@misc{parsec,
  title = {Parsec, a fast combinator parser},
  author = {Daan Leijen},
  year = {2001},
  howpublished = {\url{http://www.cs.uu.nl/~daan/parsec.html}}
}

@inproceedings{dtpmsp-gpce,
    author = {Edwin Brady and Kevin Hammond},
    title = {A Verified Staged Interpreter is a Verified Compiler},
    booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'06)}},
    year = 2006
}

@misc{haddock,
  title = {Haddock: A {Haskell} Documentation Tool},
  howpublished = {\url{http://www.haskell.org/haddock/}}
}

@inproceedings{offshoring,
  title = {Implicitly Heterogeneous Multi-Stage Programming},
  author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},
  booktitle = {Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005)},
  publisher = {Springer},
  series = {LNCS},
  volume = {3676},
  year = 2005
}

@misc{alti-partial,
  title = {Stop thinking about bottoms when writing programs},
  author = {Thorsten Altenkirch},
  year = 2006,
  note = {Talk at BCTCS 2006}
}

@misc{tarmo-partial,
  title = {Partiality is an Effect},
  author = {Tarmo Uustalu},
  year = 2004,
  note = {Talk at Dagstuhl workshop on Dependently Typed Progamming}
}

@inproceedings{McKinnaPOPL06,
 author = {James McKinna},
 title = {Why dependent types matter},
 booktitle = {Proc. ACM Symp. on Principles of Programming Languages (POPL 2006)},
 year = {2006},
 issn = {0362-1340},
 pages = {1--1},
 doi = {http://doi.acm.org/10.1145/1111320.1111038},
}


@inproceedings{leroy-compiler,
  title = {Formal Certification of a Compiler Back-end},
  author = {Xavier Leroy},
  year = 2006,
  booktitle = {Principles of Programming Languages 2006},
  pages = {42--54},
  publisher = {ACM Press}
}

@inproceedings{hutton-exceptions,
   title = {Compiling Exceptions Correctly},
   year = 2004,
   author = {Graham Hutton and Joel Wright},
   booktitle = {Mathematics of Program Construction},
   publisher = {Springer},
   series = {LNCS},
   volume = {3125}
}

@inproceedings{tagless-staged,
  title = {Tagless Staged Interpreters for Typed Languages},
  year = {2002},
  booktitle = {Proc. 2002 International Conf. on Functional Programming (ICFP 2002)},
  author = {Emir Pa\v{s}al\'{i}c and Walid Taha and Tim Sheard},
  publisher = {ACM}
}

@inproceedings{env-classifiers,
   title = {Environment Classifiers},
   year = 2003,
   author = {Walid Taha},
   booktitle = {Proc. ACM Symp. on Principles of Programming Languages (POPL 2003)},
   pages = {26--37},
}

@inproceedings{dsl-msp,
   title = {{DSL} Implementation in {MetaOCaml}, {Template Haskell}, {and C++}},
   booktitle = {Domain Specific Program Genearation 2004},
   author = {Krzysztof Czarnecki and John O'Donnell and J\"{o}rg Striegnitz and Walid Taha},
   publisher = {Springer},
   series = {LNCS},
   volume = {3016},
   year = 2004
}

@misc{ gadt-extk,
    author = {Tim Sheard and James Hook and Nathan Linger},
    title = {{GADTs} + Extensible Kinds = Dependent Programming},
    year = 2005,
    misc = {Submitted to ICFP '05}
}

@INPROCEEDINGS{dt-framework,
  TITLE = {A Dependently Typed Framework for Static Analysis of Program Execution Costs},
  YEAR = {2006},
  BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
  AUTHOR = {Edwin Brady and Kevin Hammond},
  VOLUME = {4015},
  SERIES = {LNCS},
  PAGES = {74--90},
  PUBLISHER = {Springer}
}

@INPROCEEDINGS{step-counting,
  TITLE = {Accurate Step Counting},
  YEAR = {2006},
  BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
  AUTHOR = {Catherine Hope and Graham Hutton},
  PUBLISHER = {Springer}
}

@misc{multi-taha,
    author = {Walid Taha},
    title = {A Gentle Introduction to Multi-stage Programming},
    year = {2003},
    note = {Available from \url{http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf}}
}

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

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

@phdthesis{ taha-thesis,
    author = {Walid Taha},
    title = {Multi-stage Programming:  Its Theory and Applications},
    year = 1999,
    school = {Oregon Graduate Inst. of Science and Technology}
}

@phdthesis{ pasalic-thesis,
    author = {Emir Pa\v{s}al\'{i}c},
    title = {The Role of Type-Equality in Meta-programming},
    year = 2004,
    school = {OGI School of Science and Engineering}
}

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


@inproceedings { wadler-listless,
    author = {Philip Wadler},
    title = {Listlessness is better than laziness: {Lazy} evaluation and garbage collection at compile-time},
    booktitle = {Proceedings of the 1984 ACM Symposium on LISP and functional programming},
    year = 1984,
    pages = {45--52}
}

@techreport { gofer-impl,
    author = {Mark P. Jones},
    title = {The implementation of the Gofer functional programming system},
    month = {May},
    year = {1994},
    number = {YALEU/DCS/RR-1030},
    institution = {Yale University}
}

@techreport { pm-opt1,
    author = {Kevin Scott and Norman Ramsey},
    title = {When do match-compilation heuristics matter?},
    month = {May},
    year = {2000},
    number = {CS-2000-13},
    institution = {Department of Computer Science, University of Virginia}
}

@inproceedings{ pm-opt2,
    author = "Fabrice Le Fessant and Luc Maranget",
    title = "Optimizing Pattern Matching",
    booktitle = "International Conference on Functional Programming",
    pages = "26-37",
    year = "2001",
    url = "citeseer.ist.psu.edu/lefessant01optimizing.html" }

@incollection{con-engine,
  author = {G\'{e}rard Huet},
  title = {The constructive engine},
  booktitle = {A Perspective in Theoreticak Computer Science},
  publisher = {World Scientific Publishing},
  year = {1989},
  editor = {R. Narasimhan},
  note = {Commemorative Volume for Gift Siromoney},
  pages = {38--69}
}

@inproceedings{gadts,
  title = {Simple unification-based type inference for {GADTs}},
  author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
  year = {2006},
  booktitle = {Proc. 2006 International Conf. on Functional Programming (ICFP 2006)}
}

@misc{wobbly,
  author = {Simon {Peyton Jones} and Geoffrey Washburn and Stephanie Weirich},
  title = {Wobbly types: type inference for generalised algebraic data types},
  year = {2004},
  note = {Submitted to POPL 2005}
}

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

@book{ml85,
    author = {Per Martin-L\"{o}f},
    title = "Intuitionistic Type Theory",
    year = "1985",
    publisher = "Bibliopolis"
}   

@article{modular-fulllazy,
  title = {A Modular Fully Lazy Lambda Lifter in {Haskell}},
  author = {Simon {Peyton Jones} and David Lester},
  year = {1991},
  month = {May},
  journal = {Software Practice and Experience},
  volume = {21},
  number = {5},
  pages = {479--506}
}

@article{ghani-jay95,
  author = 	 {Barry Jay and Neil Ghani},
  title = 	 {The Virtues of Eta-Expansion},
  journal = 	 {Journal of Functional Programming},
  year = 	 {1995},
  volume = 	 {5},
  number = 	 {2},
  pages = 	 {135-154},
}

@misc{nkpat,
    author = {Lennart Augustsson},
    title = {n+k patterns},
    year = {1993},
    howpublished = {Message to the haskell mailing list, Mon, 17 May 93}
}

@article{ danvy98functional,
    author = "Olivier Danvy",
    title = "Functional Unparsing",
    journal = "Journal of Functional Programming",
    volume = "8",
    number = "6",
    pages = "621-625",
    year = "1998",
    url = "citeseer.ist.psu.edu/danvy98functional.html" }

@inproceedings{SeveriPoll94,
   author = {Paula Severi and Erik Poll},
   booktitle = {Logical Foundations of Computing Science, LFCS'94},
   editor = {A. Nerode and Yu. V. Matiyasevich},
   number = {813},
   pages = {316--328},
   publisher = {Springer},
   series = {LNCS},
   title = {{P}ure {T}ype {S}ystems with {D}efinitions},
   year = {1994}
}

@inproceedings{coinductive,
  title = {An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol},
  booktitle = {Proceedings of the 1995 Workshop on Types for Proofs and Programs},
  series = {LNCS},
  year = {1995},
  volume = {1158}, 
  pages = {135-152},
  publisher = {Springer-Verlag},
  author = {Eduardo Gim\'{e}nez}
}

@book{erlang,
    author = "Joe Armstrong and Robert Virding and Claes Wikstr{\"o}m and Mike Williams",
    title = "Concurrent Programming in Erlang",
    edition = "Second",
    publisher = "Prentice-Hall",
    year = "1996",
    url = "citeseer.ist.psu.edu/armstrong93concurrent.html" 
}

@PhdThesis{alti:phd93,
  author =       "Thorsten Altenkirch",
  title =        "Constructions, Inductive Types and Strong Normalization",
  school =       "University of Edinburgh",
  year =         "1993",
  month =        "November",
}

@inproceedings{coq-modules,
  author = "Jacek Chrzaszcz",
  title = "Modules in {Coq} Are and Will Be Correct",
  year = {2004},
   booktitle = {Types for Proofs and Programs 2003},
   editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
   publisher = {Springer},
   volume = {3085}
}

@inproceedings{comp-polymorphism,
  author = "Robert Harper and Greg Morrisett",
  title = "Compiling Polymorphism Using Intensional Type Analysis",
  year = "1995",
  booktitle = "Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages",
  pages = "130 -- 141"
}

@misc{runtime-loader,
  author = "Andre Pang",
  title = "{GHC} Runtime Loading",
  year = "2004",
  howpublished = {Available from \verb+http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading+}
}

@article{mccarthy-lisp,
  author = "John McCarthy",
  title = "Recursive Functions of Symbolic Expressions and Their Computation By Machine",
  year = "1960",
  journal = "Communications of the ACM",
  volume = "3",
  number = "4",
  pages = "184--195"
}

@book{stl,
  author = " David R. Musser and Atul Saini and Gillmer J. Derge",
  title= "The {STL} Tutorial and Reference Guide: {C++} Programming with the Standard Template Library",
  year = "2001",
  publisher = "Addison Wesley"
}

@misc{ phase-distinction,
    author = "Luca Cardelli",
    title = "Phase Distinctions in Type Theory",
    howpublished = "Manuscript",
    year = "1988",
    url = "citeseer.ist.psu.edu/cardelli88phase.html" }

@book {pierce-types,
  author = "Benjamin C. Pierce",
  title = "Type and Programming Languages",
  year = "2002",
  publisher = "MIT Press"
}

@article{ coqcc,
  Author = "Thierry Coquand and G\'{e}rard Huet",
  title = "The calculus of constructions",
  year = "1988",
  journal = "Information and Computation",
  volume = "76",
  pages = "95--120"
}

@article{ miller91jlc,
  Author = "Dale Miller",
  Title = "A Logic Programming Language with Lambda-Abstraction,
    Function Variables, and Simple Unification",
  Journal = "Journal of Logic and Computation",
  Volume = "1",
  Number = "4",
  Pages = "497-536",
  Year = "1991",
  URL = "citeseer.ist.psu.edu/miller91logic.html",
  URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" }

@article{miller-unity,
   author = "Dale Miller",
   title = "Unification Under a Mixed Prefix",
   journal = "Journal of Symbolic Computation",
   volume = "14",
   pages = "321--358",
   year = 1992
}

@inproceedings{ cynthia,
    author = "Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe",
    title = "An {ML} Editor Based on Proofs-As-Programs",
    booktitle = "Automated Software Engineering",
    pages = "166-173",
    year = "1999",
    url = "citeseer.ist.psu.edu/whittle99ml.html" }


@misc{ewd340,
   title={The Humble Programmer},
   author={Edsger Dijkstra},
   year={1972},
   note={Turing Award Lecture, EWD 340}
}

@misc{fortran,
   title={Specifications for the {IBM} Mathematical FORmula TRANslating System, {FORTRAN}},
   author={{IBM Applied Science Division}},
   key={IBM},
   year={1954},
   month={November}
}

@inproceedings{quickcheck,
   title = {{QuickCheck}: A Lightweight Tool For Random Testing Of {Haskell} Programs},
   author = {Koen Claessen and John Hughes},
   year = {2000},
   booktitle = {International Conference on Functional Programming}
}

@inproceedings{currylam,
   title = {Functionality in Combinatory Logic},
   author = {Haskell Curry},
   year = {1934},
   booktitle = {Proc. Nat. Acad. Sci, USA},
   volume = {20},
   pages = {584--590}
}

@article{churchsimplelam1,
   title = {A set of postulates for the foundation of logic},
   author = {Alonzo Church},
   year = {1932},
   journal = {Annals of Mathematics},
   volume = {2},
   number = {33},
   pages = {346--366}
}

@article{churchsimplelam2,
   title = {A set of postulates for the foundation of logic},
   author = {Alonzo Church},
   year = {1933},
   journal = {Annals of Mathematics},
   volume = {2},
   number = {34},
   pages = {839--864}
}

@article{churchlam,
   title = {A Formulation of the Simple Theory of Types},
   author = {Alonzo Church},
   year = {1940},
   journal = {Journal of Symbolic Logic},
   volume = {5},
   pages = {56--58}
}

@book{mitchell,
   title = {Concepts in Programming Languages},
   author = {John C. Mitchell},
   year = {2003},
   publisher = {Cambridge University Press}
}

@inproceedings{harrison-hol99,
   title = {A Machine-Checked Theory of Floating Point Arithmetic},
   year = {1999},
   booktitle = {Theorem Proving in Higher Order Logics: 12th International Conference, TP},
   pages = {113--130},
   author = {John Harrison},
   crossref = {hol99}
}

@inproceedings{c--,
   title = {C--: A portable assembly language},
   year = {1997},
   booktitle = {Workshop on Implementing Functional Languages, St Andrews},
   author = {Simon {Peyton Jones} and Thomas Nordin and Dino Oliva},
   crossref = {func-imp97}
}

@proceedings{func-imp97,
   title = {Workshop on Implementing Functional Languages, St Andrews},
   year = {1997},
   editor = {C Clack},
   publisher = {Springer-Verlag}
}

@proceedings{hol99,
   volume = {1690},
   title = {Theorem Proving in Higher Order Logics:        12th International Conference, TPHOLs'99},
   year = {1999},
   editor = {Yves Bertot and Gilles Dowek and Andr{\'e}        Hirschowitz and Christine Paul},
   publisher = {Springer-Verlag},
   address = {Nice, France},
   series = {LNCS}
}

@book{mathlogic,
   title = {Mathematical Logic and Programming Languages},
   year = {1985},
   editor = {C.A.R. Hoare and J.C. Shepherdson},
   publisher = {Prentice-Hall}
}

@book{automath,
   title = {Selected Papers on Automath},
   year = {1994},
   editor = {S. Abramsky and J. Barwise and K. Fine and H.J. Keisler and        A.S. Troelstr},
   publisher = {North-Holland}
}

@misc{gimps,
   howpublished = {http://www.mersenne.org/prime.htm},
   title = {Great Internet Mersenne Prime Search}
}

@misc{haskell-report,
   title = {Haskell 98 Language and Libraries --- The Revised Report},
   year = {2002},
   month = {December},
   author = {Simon {Peyton Jones} and others},
   howpublished = {Available from \verb+http://www.haskell.org/+}
}

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


@misc{equality-cayenne,
   howpublished = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
   title = {Equality Proofs in Cayenne},
   year = {1999},
   author = {Lennart Augustsson}
}

@misc{interp-cayenne,
   howpublished = {\url{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}
}

@inproceedings{balaa00fixpoint,
   title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
   year = {2000},
   booktitle = {Theorem Proving in Higher Order Logics},
   pages = {1-16},
   author = {Antonia Balaa and Yves Bertot}
}

@inproceedings{isabelle-maple,
   title = {Theorems and algorithms: An interface between Isabelle and Maple},
   year = {1995},
   booktitle = {International Symposium on Symbolic and Algebraic Computation},
   author = {Ballarin, C. and Homann, K., and Calmet, J.}
}

@book{barendregt-num,
   title = {The Lambda Calculus, Its Syntax and Semantics},
   year = {1984},
   publisher = {North-Holland},
   author = {Henk Barendregt}
}

@book{beiler,
   title = {Recreations in the Theory of Numbers},
   year = {1964},
   publisher = {Dover},
   author = {Albert H. Beiler}
}

@article{multidigit,
   journal = {Advances in Applied Mathematics},
   title = {Multidigit Multiplication for Mathematicians},
   year = {1998},
   author = {Daniel J. Bernstein}
}

@article{buhler-fox,
   journal = {ACM Crossroads 2.1.},
   month = {September},
   title = {The Fox project: A language-structured approach to networking        software.},
   year = {1995},
   author = {Buhler, J.},
   note = {Available at http://www.acm.org/crossroads/xrds2-1/foxnet.html}
}

@techreport{burstall91,
   title = {Computer Assisted Proof for Mathematics: an Introduction Using        the \textsc{Lego} Proof System},
   year = {1991},
   institution = {University of Edinburgh},
   author = {Rod Burstall}
}

@article{plastic,
   title = {An Implementation of {LF} with Coercive Subtyping and Universes}, 
   author = {Paul Callaghan and Zhaohui Luo},
   journal = {Journal of Automated Reasoning},
   volume = {27},
   number = {1},
   pages = {3--27},
   year = {2001}
}

@article{coercive,
   title = {Coercive subtyping},
   author = {Zhaohui Luo},
   journal = {J. Logic Comput.},
   volume = {9},
   number = {1},
   year = {1991},
   pages = {105--130}
}

@inproceedings{calmet-homann,
   title = {Classification of communication and cooperation mechanisms for        logical and symbolic computation systems},
   year = {1996},
   booktitle = {Proceedings of the First International Workshop 'Frontiers of        Combining S},
   pages = {133-146},
   publisher = {Kluwer},
   author = {J. Calmet and K. Homann}
}

@techreport{comm-proofs,
   title = {On Communicating Proofs in Interactive Mathematical Documents},
   year = {2000},
   institution = {Eindhoven University of Technology},
   author = {Olga Caprotti and Martijn Oostdijk}
}

@article{prime2999,
   title = {How to formally and efficiently prove Prime(2999)},
   year = {2001},
   author = {Olga Caprotti and Martijn Oostdijk},
   journal = {Symbolic Computation and Automated Reasoning},
   pages = {114--125}
}

@book{church-num,
   title = {The Calculi of Lambda-Conversion},
   year = {1941},
   publisher = {Princeton University Press},
   author = {Alonzo Church}
}

@book{nuprl86,
   title = {Implementing Mathematics with the NuPrl Proof Development System},
   year = {1986},
   publisher = {Prentice-Hall},
   address = {NJ},
   author = {Constable, Robert L. and others}
}

@book{conway,
   title = {On Numbers and Games},
   year = {1976},
   publisher = {Academic Press},
   author = {J.H. Conway}
}

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

@misc{tt-prog,
   month = {June},
   title = {Type Theory and Programming},
   year = {1994},
   author = {Thierry Coquand and Bengt Nordstr\"{o}m and Jan M. Smith and Bj\"{o}rn von Sydow}
}

@book{func-appr,
   title = {The Functional Approach to Programming},
   year = {1998},
   publisher = {Cambridge University Press},
   author = {Guy Cousineau and Michel Mauny}
}

@misc{ibmspec,
   howpublished = {http://www2.hursley.ibm.com/decimal/},
   month = {January},
   title = {Standard Decimal Arithmetic Specification},
   year = {2001},
   author = {Mike Cowlishaw},
   note = {\copyright IBM Corporation 2001}
}

@book{dummett,
   title = {Elements of Intuitionism},
   year = {2000},
   edition = {2nd},
   publisher = {Oxford: Clarendon},
   author = {Michael A.E. Dummet}
}

@article{dybjer94,
   title = {Inductive Families},
   year = {1994},
   author = {Peter Dybjer},
   journal = {Formal Aspects Of Computing},
   volume = {6},
   pages = {440--465}
}

@misc{octave,
   howpublished = {http://www.octave.org/},
   month = {February},
   title = {GNU Octave --        A high-level interactive language for numerical computations},
   year = {1997},
   author = {John W. Eaton}
}

@book{comp-methods,
   title = {Computing methods for scientists and engineers},
   year = {1968},
   publisher = {Oxford : Clarendon Press},
   author = {L. Fox and D.F. Mayers}
}

@misc{guile,
   howpublished = {http://www.gnu.org/software/guile/guile.html},
   title = {Guile -- Project GNU's extension language},
   year = {2001},
   author = {{Free Software Foundation}}
}

@article{need-dep,
   journal = {Journal of Functional Programming},
   number = {4},
   volume = {10},
   title = {Do we need dependent types?},
   year = {2000},
   pages = {409-415},
   author = {Daniel Fridlender and Mia Indrika}
}

@book{primes-programming,
   title = {Primes and Programming -- An Introduction to Number Theory with Computing},
   year = {1993},
   publisher = {Cambridge University Press},
   author = {Peter Giblin}
}

@misc{rec-coq,
   month = {May},
   title = {A Tutorial on Recursive Types in \textsc{Coq}},
   year = {1998},
   author = {Eduardo Gim\'{e}nez}
}

@article{goldberg91,
   journal = {ACM Computing Surveys},
   number = {1},
   volume = {23},
   title = {What every computer scientist should know about floating point        arithmetic},
   year = {1991},
   pages = {5-48},
   author = {D. Goldberg}
}

@article{binary-lambda,
   journal = {Journal of Functional Programming},
   number = {6},
   volume = {10},
   title = {An adequate and efficient left associated binary numeral        system in the $\lambda$-calculus},
   year = {2000},
   author = {Mayer Goldberg}
}

@book{hol,
   title = {Introduction to HOL},
   year = {1993},
   publisher = {Cambridge University Press},
   author = {M. Gordon and T. Melham}
}

@misc{gmp,
   howpublished = {Available from \verb+http://www.swox.com/gmp/manual/+},
   title = {The {GNU Multiple Precision} Arithmetic Library 4.1.3 --- Manual},
   year = {2004},
   author = {Torbj\"{o}rn Granlund and others}
}

@article{harrison-fmsd94,
   journal = {Formal Methods in System Design},
   volume = {5},
   title = {Constructing the Real Numbers in {HOL}},
   year = {1994},
   pages = {35--59},
   author = {John Harrison}
}

@book{harrison-thesis,
   title = {Theorem Proving with the Real Numbers},
   year = {1998},
   publisher = {Springer-Verlag},
   author = {John Harrison}
}

@techreport{hol-maple,
   title = {Reasing about the Reals: the marriage of HOL and Maple},
   year = {1993},
   institution = {University of Cambridge Computer Laboratory},
   author = {John Harrison and Laurent Th\'{e}ry}
}

@misc{coq-tutorial,
   howpublished = {http://pauillac.inria.fr/coq},
   title = {The \textsc{Coq} Proof Assistant - A Tutorial},
   author = {G\'{e}rard Huet and Gilles Kahn and Christine Paulin-Mohring}
}

@misc{restr-haskell,
   howpublished = {http://citeseer.nj.nec.com/253599.html},
   month = {September},
   title = {Restricted Data Types in Haskell},
   year = {1999},
   author = {John Hughes}
}

@misc{javadec,
   howpublished = {http://www2.hursley.ibm.com/decimalj/decimald.html},
   month = {September},
   title = {Decimal Arithmetic for Java -- a Proposal},
   year = {2000},
   author = {{IBM Corporation}}
}

@misc{ieee754,
   title = {IEEE Standard for Binary Floating Point Arithmetic},
   year = {1985},
   author = {{IEEE Standard 754}}
}

@misc{ieee854,
   title = {IEEE Standard for Radix-Independent Floating-Point Arithmetic},
   year = {1987},
   author = {{IEEE Standard 854}}
}

@inproceedings{jon91,
   title = {Completing the Rational and Metric Spaces in \textsc{Lego}},
   year = {1991},
   booktitle = {Proceedings of the Second Workshop on Logical Frameworks},
   author = {Claire Jones}
}

@misc{ typinghaskell,
  author = "Mark Jones",
  title = "Typing {Haskell} in {Haskell}",
  howpublished = "In Haskell Workshop, September 1999.",
  year = "1999",
  url = "citeseer.ist.psu.edu/article/jones99typing.html" }

@article{karatsuba,
   journal = {Soviet Physics-Doklady},
   volume = {7},
   title = {Multiplication of multidigit numbers by automata},
   year = {1963},
   pages = {595--596},
   author = {A. Karatsuba and Y. Ofman}
}

@book{knuth2,
   volume = {2},
   title = {The Art of Computer Programming - Seminumerical Algorithms},
   year = {1969},
   publisher = {Addison Wesley},
   author = {Donald E. Knuth}
}

@article{next700,
   journal = {Communications of the ACM},
   number = {3},
   month = {March},
   volume = {9},
   title = {The next 700 programming languages},
   year = {1966},
   author = {P.J. Landin}
}

@techreport{luo-spec,
   month = {January},
   title = {Program Specification and Data Refinement in Type Theory},
   year = {1993},
   institution = {Department of Computer Science, University of Edinburgh},
   author = {Zhaohui Luo}
}

@phdthesis{luo90,
   school = {University of Edinburgh},
   title = {An Extended Calculus Of Constructions},
   year = {1990},
   author = {Zhaohui Luo}
}

@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{alf,
   title = {The {ALF} proof editor and its proof engine},
   year = {1994},
   booktitle = {Formal Proceeding of the 1993 Workshop on Types for Proofs        and Programs},
   author = {Lena Magnusson and Bengt N\"{o}rdstrom}
}

@misc{happy,
   howpublished = {http://www.haskell.org/happy/},
   title = {Happy User Guide},
   year = {2001},
   author = {Simon Marlow and Andy Gill}
}

@inproceedings{generic-haskell,
   title = {Generic Haskell, Specifically},
   author = {Dave Clarke and Andres L\"{o}h},
   editor = {Jeremy Gibbons and Johan Jeuring},
   booktitle = {Proceedings of the IFIP TC2 Working Conference on Generic Programming},
   year = {2002},
   publisher = {Kluwer Academic Publishers},
   pages = {21--48}
}

@article{faking-it,
   title = {Faking It -- Simulating Dependent Types in {Haskell}},
   year = {2002},
   author = {Conor McBride},
   journal = {Journal of Functional Programming},
   volume = {12},
   number = {4+5},
   pages = {375--392}
}

@misc{mcbride-inverting,
   title = {Inverting Inductively Defined Relations in \textsc{Lego}},
   year = {1996},
   author = {Conor McBride}
}

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

@article{mcbride-unification,
   title = {First-Order Unification by Structural Recursion},
   year = {2003},
   author = {Conor McBride},
   journal = {Journal of Functional Programming},
   volume = {13},
   number = {6},
   pages = {1061--1075}
}

@misc{mckinna-pollack,
   howpublished = {Kluwer Academic Publishers},
   title = {Some Lambda Calculus and Type Theory formalized},
   year = {1998},
   author = {James McKinna and Robert Pollack}
}

@book{num-theory,
   title = {An Introduction to the Theory of Numbers},
   year = {1980},
   publisher = {John Wiley and Sons},
   author = {Ivan Niven and Herbert S. Zuckerman}
}

@book{prog-mltt,
   title = {Programming in Martin-L\"{o}f's Type Theory -- An Introduction},
   year = {1990},
   publisher = {Oxford University Press},
   author = {Bengt Nordstr\"{o}m and Kent Petersson and Jan M. Smith},
   note = {Out of print. Available from http://www.cs.chalmers.se/Cs/Research/Logic}
}

@book{okasaki,
   title = {Purely Functional Data Structures},
   year = {1998},
   publisher = {Cambridge University Press},
   author = {Chris Okasaki}
}

@book{arith-systems,
   title = {Computer Arithmetic Systems},
   year = {1994},
   publisher = {Prentice-Hall},
   author = {Amos R. Omondi}
}

@book{pj-imp,
   title = {The Implementation of Functional Programming Languages},
   year = {1987},
   publisher = {Prentice-Hall},
   author = {Simon {Peyton Jones}}
}

@book{cp-bjc,
   title = {Computational Numerical Methods},
   year = {1986},
   publisher = {John Wiley and Sons},
   author = {C. Phillips and B. Cornelius}
}

@book{nag,
   title = {The NAG Library: a beginner's guide},
   year = {1986},
   publisher = {Oxford : Clarendon Press},
   author = {Jen Phillips}
}

@misc{believe,
   month = {September},
   title = {How to Believe a Machine-Checked Proof},
   year = {1996},
   author = {Robert Pollack}
}

@phdthesis{pollack94,
   school = {University of Edinburgh},
   title = {The Theory of LEGO -- A Proof Checker for the Extended Calculus of Constructions},
   year = {1994},
   author = {Robert Pollack}
}

@inproceedings{intel-bug,
   series = {LNCS},
   volume = {915},
   title = {Anatomy of the Pentium Bug},
   publisher = {Springer-Verlag},
   year = {1995},
   pages = {97--107},
   author = {V.R. Pratt}
}

@book{maple,
   title = {The Maple Handbook: Maple V Release 4},
   year = {1996},
   publisher = {Springer},
   author = {Darren Redfern}
}

@book{crypto,
   title = {Applied Cryptography: protocols, algorithms and source code in C.},
   year = {1996},
   publisher = {Wiley},
   author = {Bruce Schneier}
}

@article{adts,
   journal = {Mathematical Structures in Computer Science},
   number = {2},
   volume = {10},
   title = {On lists and other abstract data types in the calculus of        construction},
   year = {2000},
   pages = {261-276},
   author = {Jonathan P. Seldin}
}

@article{seldin97,
   journal = {Annals of Pure and Applied Logic},
   number = {1},
   month = {January},
   volume = {83},
   title = {On the proof theory of Coquand's calculus of constructions},
   year = {1997},
   pages = {23--101},
   author = {Jonathan P. Seldin}
}

@article{wichmann,
   journal = {The Computer Journal},
   volume = {32},
   title = {Towards a Formal Specification of Floating Point},
   year = {1989},
   pages = {432-436},
   author = {B.A. Wichmann}
}

@book{mathematica,
   title = {Mathematica : a system for doing mathematics by computer},
   year = {1991},
   publisher = {Addison Wesley},
   author = {Stephen Wolfram}
}

@inproceedings{xi-imp,
author = "Hongwei Xi",
title = {{Imperative Programming with Dependent Types}},
booktitle = "Proceedings of 15th IEEE Symposium on Logic in Computer Science",
year = 2000,
month = "June",
address = "Santa Barbara",
pages = "375--387"
}

@phdthesis{xi-thesis,
   month = {December},
   school = {Department of Mathematical Sciences, Carnegie Mellon University},
   title = {Dependent Types in Practical Programming},
   year = {1998},
   author = {Hongwei Xi}
}


@techreport{dtal,
author = {Hongwei Xi and Robert Harper},
title = {A Dependently Typed Assembly Language},
institution = {Computer Science and Engineering Department, Oregon Graduate Institute},
year = 1999,
number = {OGI-CSE-99-008},
month = {July},
}

@misc{bignum-cmp,
   month = {February},
   title = {Comparison of three public-domain multiprecision libraries:        BigNum, Gmp and Pari},
   year = {1998},
   author = {Paul Zimmerman}
}

@book{perl,
   title = {Programming Perl},
   author = {Larry Wall and Tom Christiansen and Jon Orwant},
   year = {2000},
   edition = {3rd},
   publisher = {O'Reilly}
}

@misc{python,
   howpublished = {http://www.python.org/doc/current/tut/tut.html},
   month = {April},
   title = {Python Tutorial},
   year = {2001},
   author = {Guido van {Rossum} and Fred L. {Drake, Jr}}
}

@book{logic,
   title = {The Language of First Order Logic},
   year = {1992},
   publisher = {CSLI Lecture Notes},
   author = {Jon Barwise and John Etchemendy}
}

@book{haskell,
   title = {Haskell -- The Craft of Functional Programming},
   year = {1999},
   publisher = {Addison Wesley},
   author = {Simon Thompson}
}

@inproceedings{coq-hol,
   title = {A Comparative Study of Coq and HOL},
   year = {1997},
   booktitle = {Theorem Proving in Higher Order Logics},
   pages = {323-337},
   author = {Vincent Zammit}
}

@misc{gay90,
   month = {November},
   title = {Correctly Rounded Binary-Decimal and Decimal-Binary Conversions},
   year = {1990},
   author = {David M. Gay},
   note = {AT&T Bell Laboratories, Numerical Analysis Manuscript 90-10}
}

@article{hughes-matters,
   journal = {Computer Journal},
   number = {2},
   volume = {32},
   title = {Why Functional Programming Matters},
   year = {1989},
   pages = {98--107},
   author = {J. Hughes}
}

@inproceedings{proofpointing,
   title = {Proof by Pointing},
   year = {1994},
   booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer So},
   pages = {141--160},
   editor = {M. Hagiya and J. C. Mitchell},
   publisher = {Springer-Verlag},
   series = {LNCS},
   volume = {789},
   address = {Sendai, Japan},
   author = {Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry}
}

@misc{inductive-coq,
   month = {December},
   title = {Inductive Definitions in the System Coq -- Rules and Properties},
   year = {1992},
   author = {Christine Paulin-Mohring}
}

@misc{leiserson98,
   month = {July},
   title = {Using de Bruijn Sequences to Index a 1 in a Computer Word},
   year = {1998},
   author = {{Charles E. Leiserson} and {Harald Prokop} and {Keith H. Randall}}
}

@inproceedings{proofchecking,
   title = {A two-level approach towards lean proof-checking},
   year = {1996},
   booktitle = {TYPES},
   pages = {16--35},
   author = {G. Barthe and M.P.J. Ruys and H.P. Barendregt}
}

@inproceedings{congruence,
   title = {Congruence Types},
   year = {1995},
   booktitle = {CSL},
   pages = {36--51},
   author = {Gilles Barthe and Herman Geuvers}
}

@phdthesis{geuvers-thesis,
   title = {Logic and Type Systems},
   author = {Herman Geuvers},
   year = 1993,
   school = {Katholieke Universiteit Nijmegen}
}

@techreport{multiple-values,
   title = {Multiple Values in {Standard ML}},
   year = {1994},
   number = {94-312},
   institution = {LFCS, Dept of Computer Science, University of Edinburgh},
   author = {Kevin Mitchell}
}

@inproceedings{oracle-checking,
   month = {January},
   title = {Oracle-Based Checking of Untrusted Software},
   year = {2001},
   booktitle = {Proceedings of the 28th ACM Symposium on Principles of Programming Languages},
   pages = {142--154},
   author = {{George C. Necula} and {S.P. Rahul}}
}

@article{adams93jfp,
   journal = {Journal of Functional Programming},
   number = {4},
   volume = {3},
   title = {Efficient Sets -- A Balancing Act},
   year = {1993},
   pages = {553--561},
   author = {Stephen Adams}
}

@inproceedings{hughes-sized,
   title = {Proving the Correctness of Reactive Systems Using Sized Types},
   year = {1996},
   booktitle = {Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programmin},
   pages = {410--423},
   author = {John Hughes and Lars Pareto and Amr Sabry}
}

@inproceedings{whittle99ml,
   title = {An {ML} Editor Based on Proofs-As-Programs},
   year = {1999},
   booktitle = {Automated Software Engineering},
   pages = {166--173},
   author = {Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe}
}

@book{efp-typeinf,
   title = {Elements of Functional Programming},
   year = {1989},
   publisher = {Addison-Wesley},
   author = {Chris Reade},
   series = {International Computer Science Series}
}

@incollection{ wadler-views,
    author = "Philip Wadler",
    title = "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction",
    booktitle = "Proceedings, 14th Symposium on Principles of Programming Languages",
    publisher = "Association for Computing Machinery",
    editor = "Steve Munchnik",
    pages = "307--312",
    year = "1987",
    url = "citeseer.nj.nec.com/wadler87views.html" }

@article{ coquand-checking,
    author = "Thierry Coquand",
    title = "An Algorithm for Type-Checking Dependent Types",
    journal = "Science of Computer Programming",
    volume = "26",
    number = "1-3",
    pages = "167-177",
    year = "1996",
    url = "citeseer.nj.nec.com/coquand96algorithm.html" }

@misc{coquand-pm,
    author = "Thierry Coquand",
    title = "Pattern Matching with Dependent Types",
    year = "1992",
    howpublished = "Available from \verb+http://www.cs.chalmers.se/~coquand/type.html+"
}

@misc{pollack-records,
   month = {August},
   title = {Dependently Typed Records for Representing Mathematical Structure},
   year = {2000},
   author = {Robert Pollack}
}

@article{checking-betarte,
   journal = {Journal of Functional Programming},
   number = {2},
   month = {March},
   volume = {10},
   title = {Type checking dependent (record) types and subtyping},
   year = {2000},
   pages = {137--166},
   author = {Gustavo Betarte}
}


@article{ gcode,
    author = "Thomas Johnsson",
    title = "Efficient Compilation of Lazy Evaluation",
    booktitle = "Proceedings of the {ACM} {SIGPLAN}'84 Symposium on Compiler Con struction",
    journal = "SIGPLAN Notices",
    volume = "19",
    number = "6",
    month = "June",
    publisher = "ACM Press",
    pages = "58--69",
    year = "1984",
    url = "citeseer.nj.nec.com/johnsson84efficient.html" }

@misc{kamareddine01,
   month = {February},
   title = {Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems},
   year = {2001},
   author = {Fairouz Kamareddine}
}

@book{prooftheory,
   title = {Basic Proof Theory},
   year = {1996},
   publisher = {Cambridge University Press},
   author = {A.S. Troelstra and H. Schwichtenberg},
   series = {Cambridge Tracts in Theoretical Computer Science}
}

@misc{nbe_staged,
   title = {Integrating Normalization-by-Evaluation into a Staged Programming Language},
   year = {1998},
   author = {Tim Sheard}
}

@inproceedings{nbe2,
   title = {Normalization by evaluation},
   year = {1998},
   author = {Ulrich Berger and Matthias Eberl and Helmut Schwichtenberg},
   booktitle = {Prospects for Hardware Foundations 1998},
   pages = {117--137},
   series = {LNCS}
}



@misc{rtcg_jfp,
   title = {Compiling for Run-time Code Generation},
   year = {2000},
   author = {Frederick Smith and Dan Grossman and Greg Morrisett and Luke Hornof and Trevor J},
   note = {Under consideration for J. Functional Programming}
}

@phdthesis{fredsmith_thesis,
   month = {January},
   school = {Cornell University},
   title = {Certified Run-time Code Generation},
   year = {2002},
   author = {Frederick Smith}
}

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

@inproceedings{xi_deadcode,
author = "Hongwei Xi",
title = {Dead Code Elimination through Dependent Types},
booktitle = "The First International Workshop on Practical Aspects of Declarative Languages",
year = 1999,
month = "January",
address = "San Antonio",
pages = "228--242"
}

@book{compilers,
   title = {Compilers --- Principles, Techniques and Tools},
   year = {1986},
   publisher = {Addison-Wesley},
   author = {Alfred Aho and Ravi Sethi and Jeffrey Ullman}
}

@inproceedings{nhc,
   title = {Highlights from nhc: A space efficient {Haskell} Compiler},
   year = {1995},
   author = "Niklas R{\"o}jemo",
   booktitle = "Functional Programming Languages and Computer Architecture",
   pages = "282--292"
}


@misc{mlmatch,
   title = {SML/NJ Match Compiler Notes},
   year = {1992},
   author = {William Aitken}
}

@misc{mlmatch_sestoft,
   title = {ML pattern match compilation and partial evaluation},
   year = {1992},
   author = {Peter Sestoft}
}

@inproceedings{compiledstrongreduction,
   title = {A Compiled Implementation of Strong Reduction},
   year = {2002},
   author = {Benjamin Gr\'{e}goire and Xavier Leroy},
   booktitle = {Proc. 2002 International Conf. on Functional Programming (ICFP 2002)},
   pages = {235--246}
}

@misc{tclhaskell,
   howpublished = {http://www.dcs.gla.ac.uk/~meurig/TclHaskell/usermanual.html},
   month = {August},
   title = {TclHaskell - User Manual},
   year = {1999},
   author = {Meurig Sage}
}


@InProceedings{nbe-cat,
  author =	 "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
  title =	 "Categorical reconstruction of a reduction free
		  normalization proof",
  year =	 "1995",
  booktitle = 	 "Category Theory and Computer Science",
  editor =	 {David Pitt and David E. Rydeheard and Peter Johnstone},
  series =	 {LNCS},
  volume = {953},
  pages =	 {182-199}
}

@inproceedings{presburgerEFSM,
   title = {A Comparison of Presburger Engines for EFSM Reachability},
   year = {1998},
   booktitle = {Computer Aided Verification '98},
   pages = {280--292},
   author = {Thomas R. Shiple and James H. Kukula and Rajeev K. Ranjan}
}

@misc{typesafecast,
   title = {Type-Safe Cast},
   year = {2000},
   author = {Stephanie Weirich}
}

@phdthesis{grobauer-thesis,
   school = {University of Aarhus},
   title = {Topics in Semantics Based Program Manipulation},
   year = {2001},
   author = {Bernd Grobauer}
}

@misc{monads-moggi,
   title = {Computational Lambda Calculus and Monads},
   year = {1989},
   author = {Eugenio Moggi}
}

@article{gmp-proof,
   title = {A proof of {GMP} square root},
   year = {2002},
   journal = {Journal of Automated Reasoning},
   volume = {29},
   pages = {225--252},
   author = {Yves Bertot and Nicolas Magaud and Paul Zimmerman}
}

@article{F-tal,
   journal = {ACM Transactions on Programming Languages and Systems},
   number = {3},
   month = {May},
   volume = {21},
   title = {From {System F} to Typed Assembly Language},
   year = {1999},
   pages = {528--569},
   author = {Greg Morrisett and David Walker and Karl Crary and Neal Glew}
}

@techreport{nbe-rtcg,
   month = {December},
   title = {Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation},
   year = {1997},
   institution = {BRICS},
   author = {Vincent Balat and Oliver Danvy}
}

@misc{yong-schemata,
   howpublished = {http://www.dur.ac.uk/yong.luo/},
   title = {A Methodology for Implementing Inductive Schemata},
   year = {2002},
   author = {Yong Luo and Zhaohui Luo}
}

@inproceedings{harper93,
   title = {Explicit Polymorphism and CPS Conversion},
   year = {1993},
   booktitle = {20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
   pages = {206--219},
   publisher = {ACM Press, New York, NY, USA},
   author = {Robert Harper and Mark Lillibridge}
}

@techreport{backends,
   month = {November},
   title = {Functional Back-Ends within the Lambda-Sigma Calculus},
   year = {1996},
   institution = {INRIA},
   author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
}

@article{stg,
   title = {Implementing lazy functional languages on stock hardware -- the {Spineless Tagless G-machine}},
   year = {1992},
   journal = {Journal of Functional Programming},
   volume = {2},
   number = {2},
   pages = {127--202},
   month = {April},
   author = {Simon {Peyton Jones}}
}

@article{debruijn,
   journal = {Indagationes Mathematicae},
   volume = {34},
   title = {Lambda calculus notation with nameless dummies},
   year = {1972},
   pages = {381--392},
   author = {N.G. de Bruijn}
}

@book{assembly,
   month = {January},
   title = {PC Assembly Language},
   year = {2002},
   publisher = {http://www.drpaulcarter.com/},
   author = {Paul A. Carter}
}

@inproceedings{poly99,
   title = {Once Upon A Polymorphic Type},
   year = {1999},
   booktitle = {26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
   publisher = {ACM},
   author = {Keith Wansbrough and Simon {Peyton Jones}}
}

@misc{lazy_intro,
   title = {Compiling Lazy Functional Languages: An introduction},
   year = {1986},
   author = {Thomas Johnsson}
}

@inproceedings{unboxed-fp,
   month = {Sept},
   title = {Unboxed Values as First Class Citizens in a Non-Strict Functional Language},
   year = {1991},
   author = {Simon {Peyton Jones} and John Launchbury},
   booktitle = {Functional Programming Languages and Computer Architecture (FPCA'91)},
   crossref = {fplca91},
   pages = {636--666}
}

@inproceedings{abc-machine,
 author = {Sjaak Smetsers and Eric N{\"{o}}cker and John {van Groningen} and Rinus Plasmeijer},
 title = {Generating efficient code for lazy functional languages},
 booktitle = {Functional programming Languages and Computer Architecture},
 year = {1991},
 pages = {592--617},
 crossref = {fplca91}
}

@proceedings{fplca91,
   title = {Functional programming Languages and Computer Architecture},
   year = {1991},
   volume = {523},
   series = {LNCS},
   publisher = {Springer-Verlag},
   editor = {John Hughes}
}



@inproceedings{nbe,
   title = {An inverse of the evaluation functional for typed $\lambda$-calculus},
   year = {1991},
   booktitle = {Proc. 1991 IEEE Symp. on Logic in Comp. Sci.},
   pages = {203--211},
   editor = {R. Vemuri},
   author = {Ulrich Berger and Helmut Schwichtenberg}
}

@inproceedings{typed-closure,
   title = {Typed Closure Conversion},
   year = {1996},
   booktitle = {Symposium on Principles of Programming Languages},
   pages = {271--283},
   author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper}
}

@misc{ghc-commentary,
   howpublished = {http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/},
   title = {The Glasgow Haskell Compiler (GHC) Commentary},
   year = {2002},
   author = {Manuel M. T. Chakravarty and Sigbjorn Finne and Simon Marlow and Simon {Peyton Jones} and Julian Seward and Reuben Thomas},
   note = {Available from GHC CVS repository}
}

@inproceedings{lambdalift,
   month = {September},
   title = {Lambda Lifting: Transforming Programs to Recursive Equations},
   year = {1985},
   booktitle = {Functional Programming Languages and Computer Architecture},
   pages = {190--203},
   editor = {Jean-Pierre Jouannaud},
   publisher = {Springer-Verlag},
   author = {Thomas Johnsson}
}

@inproceedings{til,
   title = {TIL: A Type-Directed Optimizing Compiler for ML},
   year = {1996},
   booktitle = {Proc. {ACM} {SIGPLAN} '96 Conference on Programming Language Design and Implementation},
   pages = {181--192},
   author = {D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee}
}

@phdthesis{shao94,
   school = {Princeton University},
   title = {Compiling Standard {ML} for Efficient Execution on Modern Machines},
   year = {1994},
   author = {Zhong Shao}
}

@inproceedings{gmachine,
   month = {September},
   title = {The {G-Machine}: A fast, graph-reduction evaluator},
   year = {1985},
   booktitle = {Functional Programming Languages and Computer Architecture},
   pages = {400--413},
   editor = {Jean-Pierre Jouannaud},
   publisher = {Springer-Verlag},
   author = {R.B. Kieburtz}
}

@inproceedings{strictness,
   month = {September},
   title = {Strictness Analysis - A practical approach},
   year = {1985},
   booktitle = {Functional Programming Languages and Computer Hardware},
   pages = {35--49},
   editor = {Jean-Pierre Jouannaud},
   publisher = {Springer-Verlag},
   author = {Chris Clack and Simon {Peyton Jones}}
}

@book{fl-impl,
   title = {Implementing Functional Languages - A Tutorial},
   year = {1992},
   publisher = {Prentice Hall International},
   author = {Simon {Peyton Jones} and David Lester}
}

@phdthesis{capretta-thesis,
   school = {Katholieke Universiteit Nijmegen},
   title = {Abstraction and Computation},
   year = {2002},
   author = {Venanzio Capretta}
}

@article{bird-pointer,
   journal = {Journal of Functional Programming},
   number = {3},
   month = {May},
   volume = {11},
   title = {Unfolding Pointer Algorithms},
   year = {2001},
   pages = {347--358},
   author = {Richard S. Bird}
}

@article{impl-tp,
   journal = {Journal of Functional Programming},
   number = {2},
   month = {March},
   volume = {9},
   title = {Implementing Theorem Provers in a Purely Functional Style},
   year = {1999},
   pages = {147--166},
   author = {Keith Hanna}
}

@article{shrink-lambda,
   journal = {Journal of Functional Programming},
   number = {5},
   month = {September},
   volume = {7},
   title = {Shrinking Lambda Expressions in Linear Time},
   year = {1997},
   pages = {515--540},
   author = {Andrew W. Appel and Trevor Jim}
}

@article{stack-tal,
   journal = {Journal of Functional Programming},
   number = {1},
   month = {January},
   volume = {12},
   title = {Stack-based Typed Assembly Language},
   year = {2002},
   pages = {43--88},
   author = {Greg Morrisset and Karl Crart and Neal Glew and David Walker}
}

@article{runtime-lamsig,
   journal = {Journal of Functional Programming},
   number = {2},
   month = {March},
   volume = {8},
   title = {Functional Runtime Systems within the lambda-sigma Calculus},
   year = {1998},
   pages = {131--176},
   author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
}

@article{busylazy,
   journal = {Journal of Functional Programming},
   number = {6},
   month = {November},
   volume = {11},
   title = {How to look busy while being as lazy as ever: the Implementation of a lazy functional debugger},
   year = {2001},
   pages = {629--671},
   author = {Henrik Nilsson}
}

@article{lazyveager,
   journal = {Journal of Functional Programming},
   number = {5},
   month = {September},
   volume = {7},
   title = {More haste, less speed: lazy versus eager evaluation},
   year = {1997},
   pages = {541--547},
   author = {Richard Bird and Geraint Jones and Oege {de Moor}}
}

@article{jvm-fp,
   journal = {Journal of Functional Programming},
   number = {6},
   month = {November},
   volume = {9},
   title = {Compiling lazy functional programs for the Java Virtual Machine},
   year = {1999},
   pages = {579--603},
   author = {David Wakeling}
}

@book{isabelle,
   publisher = {Springer-Verlag},
   series = {LNCS},
   volume = {2283},
   month = {March},
   title = {Isabelle/HOL - A proof assistant for higher order logic},
   year = {2002},
   author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}
}

@article{ghc-inliner,
   journal = {Journal of Functional Programming},
   number = {4},
   month = {September},
   volume = {12},
   title = {Secrets of the {Glasgow Haskell Compiler} inliner},
   year = {2002},
   pages = {393--434},
   author = {Simon {Peyton Jones} and Simon Marlow}
}

@article{dynamic-fp,
   journal = {Journal of Functional Programming},
   number = {1},
   month = {January},
   volume = {8},
   title = {The dynamic compiliation of lazy functional programs},
   year = {1998},
   pages = {61--81},
   author = {David Wakeling}
}

@misc{isabelle-ref,
   month = {March},
   title = {Isabelle Reference Manual},
   year = {2002},
   author = {Lawrence C. Paulson}
}

@article{debruijn-nested,
   journal = {Journal of Functional Programming},
   number = {1},
   month = {January},
   volume = {9},
   title = {de Bruijn notation as a nested datatype},
   year = {1999},
   pages = {77--91},
   author = {Richard S. Bird and Ross Paterson}
}

@article{perfect-trees,
   journal = {Journal of Functional Programming},
   number = {3},
   month = {May},
   volume = {10},
   title = {Perfect trees and bit-reversal permutations},
   year = {2000},
   pages = {305--317},
   author = {Ralf Hinze}
}

@phdthesis{paulin-extraction,
   school = {Paris 7},
   title = {Extraction de programmes dans le Calcul des Constructions},
   year = {1989},
   author = {Christine Paulin-Mohring}
}

@phdthesis{santos95,
   school = {University of Glasgow},
   title = {Compilation By Transformation In Non-Strict Functional Languages},
   year = {1995},
   author = {{Andr\'{e} Lu\'{i}s de Medeiros} Santos}
}

@book{cps,
   title = {Compiling With Continuations},
   year = {1992},
   publisher = {Cambridge University Press},
   author = {Andrew W. Appel}
}

@techreport{SKIM,
   number = {31},
   title = {The {SKIM} microprogrammer's guide},
   year = {1983},
   institution = {University of Cambridge},
   author = {W.R. Stoye}
}

@misc{NORMA,
   title = {An Overview of Burroughs {NORMA}},
   year = {1985},
   author = {H. Richards}
}

@book{ml,
   title = {The Definition of Standard ML --- Revised},
   year = {1997},
   publisher = {MIT Press},
   author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}
}

@misc{ml71,
   title = {An intuitionistic theory of types},
   year = {1971},
   author = {Per Martin-L\"{o}f}
}

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

@inproceedings{ml75,
   title = {An intuitionistic theory of types: predicative part},
   year = {1975},
   booktitle = {Logic Colloquium '73},
   editor = {H. Rose and J.C. Shepherdson},
   publisher = {North-Holland},
   author = {Per Martin-L\"{o}f}
}

@inproceedings{cpm90,
   title = {Inductively defined types},
   year = {1990},
   author = {Thierry Coquand and Christine Paulin-Mohring},
   series = {LNCS},
   volume = {417},
   publusher = {Springer-Verlag}
}

@phdthesis{fpcustom,
   month = {May},
   school = {Computer Lab, University of Cambridge},
   title = {The Implementation of Functional Languages using Custom Hardware},
   year = {1985},
   author = {W.R. Stoye}
}

@phdthesis{hughesthesis,
   month = {September},
   school = {Programming Research Group, Oxford},
   title = {The design and implementation of programming languages},
   year = {1984},
   author = {John Hughes}
}

@inproceedings{tim,
   volume = {274},
   title = {{TIM} -- A simple lazy abstract machine to execute supercombinators},
   year = {1987},
   booktitle = {Functional Programming Languages and Computer Architecture},
   publisher = {Springer-Verlag},
   author = {John Fairbairn and Stuart Wray},
   pages = {34--45},
   series = {LNCS}
}

@techreport{abc,
   title = {The {ABC} machine -- A Sequential Stack-based Abstract Machine For Graph Rewriting},
   year = {1990},
   institution = {University of Nijmegen},
   author = {P.W.M.  Koopman and M.C.J.D. van {Eekelen} and E.G.J.M.H. Ncker and J.E.W. Smetsers and M.J. Plasmeijer}
}

@techreport{implicit,
   title = {On Implicit Arguments},
   year = {1994},
   institution = {Faculty of Science, University of Tokyo},
   author = {Masami Hagiya and Yozo Toda}
}

@book{semantics,
   title = {Denotational Semantics},
   year = {1986},
   publisher = {Wm. C. Brown},
   author = {David A. Schmidt}
}

@inproceedings{lazyml,
   month = {August},
   title = {A compiler for {Lazy} {ML}},
   year = {1984},
   booktitle = {Proceedings of the {ACM} Symposium on Lisp and Functional Programming},
   pages = {218--227},
   author = {Lennart Augustsson}
}

@inproceedings{nu-g,
   title = {Parallel graph reduction with the $\langle\nu,G\rangle$-machine},
   year = {1989},
   booktitle = {Functional Programming Languages and Computer Architecture},
   publisher = {ACM Press},
   author = {Lennart Augustsson and Thomas Johnsson}
}

@book{k&r,
   title = {The C programming language},
   year = {1988},
   publisher = {Prentice-Hall},
   author = {Brian W. Kernighan and Dennis M. Ritchie}
}

@misc{c--garbage,
   title = {C--: a portable assembly language that supports garbage collection},
   year = {1999},
   author = {Simon {Peyton Jones} and Norman Ramsey and Fermin Reig},
   note = {Invited talk at PPDP'99}
}

@misc{epigram,
   howpublished = {http://www.dur.ac.uk/CARG/epigram.html},
   title = {Project Proposal: {Epigram}: Innovative Programming via Inductive Families},
   year = {2002},
   author = {Zhaohui Luo and James McKinna and Paul Callaghan and Conor McBride}
}

@misc{ghc-rewrite,
   title = {Playing by the Rules: Rewriting as a practical optimisation technique in {GHC}},
   year = {2001},
   author = {Simon {Peyton Jones} and Andrew Tolmach and Tony Hoare}
}

@UNPUBLISHED{implicit-pollack,
  AUTHOR = {Robert Pollack},
  TITLE = {Implicit Syntax},
  NOTE = {Informal Proceedings of First Workshop on 
                 Logical Frameworks, Antibes},
  YEAR = {1990},
  MONTH = MAY
}


@article{transform-haskell,
   journal = {Science of Computer Programming},
   volume = {32},
   title = {A transformation-based optimiser for {Haskell}},
   year = {1998},
   pages = {3--47},
   author = {Simon {Peyton Jones} and Andr\'{e} L. M. Santos}
}

@inproceedings{knuth-bendix,
   title = {Simple Word Problems in Universal Algebras},
   year = {1970},
   booktitle = {Computational Problems in Abstract Algebra},
   pages = {263--298},
   editor = {John Leech},
   publisher = {Pergamon Press},
   author = {Donald E. Knuth and Peter B. Bendix}
}

@inproceedings{phantomfun,
   title = {Fun With Phantom Types},
   author = {Ralf Hinze},
   pages = {245--262},
   year = {2003},
   crossref = {funprogramming},
   booktitle = {The Fun Of Programming},
   publisher = {Palgrave}
}

@book{funprogramming,
   month = {March},
   title = {The Fun Of Programming},
   year = {2003},
   editor = {Jeremy Gibbons and Oege {de Moor}},
   publisher = {Palgrave},
   series = {Cornerstones of Computing}
}

@inproceedings{anderson-proof,
   title = {Representing Proof Transformations For Program Optimization},
   year = {1994},
   booktitle = {International Conference On Automated Deduction},
   publisher = {Springer Verlag},
   author = {Penny Anderson}
}

@phdthesis{daria-thesis,
   month = {April},
   school = {Institute of Informatics, Warsaw University},
   title = {Termination of Rewriting in the Calculus of Constructions},
   year = {2003},
   author = {Daria Walukiewicz-Chrzaszcz}
}

@inproceedings{change-data,
   title = {Changing Data Structures In Type Theory: A Study Of Natural Numbers},
   year = {2001},
   booktitle = {Types For Proofs And Programs 2000},
   pages = {181--196},
   editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
   publisher = {Springer},
   author = {Nicolas Magaud and Yves Bertot}
}

@phdthesis{nico-thesis,
   title = {Changement de Representation des donn\'{e}es dans le Calcul de Constructions},
   author = {Nicolas Magaud},
   year = {2003},
   month = {October},
   school = {Universit\'{e} de Nice - Sophia Antipolis}
}
   

@book{patterns,
   title = {Design Patterns},
   year = {1995},
   publisher = {Addison Wesley},
   author = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides}
}

@misc{ghchugs,
   month = {August},
   title = {The New {GHC}/{Hugs} Runtime System},
   year = {1998},
   author = {Simon Marlow and Simon {Peyton Jones}}
}

@misc{stgrevised,
   month = {February},
   title = {The {STG} runtime system (revised)},
   year = {1999},
   author = {Simon {Peyton Jones} and Simon Marlow and Alastair Reid},
   howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
}

@inproceedings{optimistic,
   month = {March},
   title = {Optimistic Evaluation --- an adaptive evaluation strategy for non-strict programs},
   year = {2003},
   author = {Robert Ennals and Simon {Peyton Jones}},
   booktitle = {International Conference on Functional Programming},
   pages = {287--298}
}

@phdthesis{ennals-thesis,
   title = {Adaptive Evaluation of Non-Strict Programs},
   author = {Robert Ennals},
   year = {2003},
   month = {December},
   school = {King's College, University of Cambridge}
}

@article{garbage,
   journal = {ACM Computing Surveys},
   number = {3},
   volume = {13},
   title = {Garbage Collection of Linked Data Structures},
   year = {1981},
   pages = {341--367},
   author = {Jacques Cohen}
}

@article{baker-gc,
   journal = {Communications of the ACM},
   number = {4},
   month = {April},
   volume = {21},
   title = {List Processing In Real Time On A Serial Computer},
   year = {1978},
   pages = {280--294},
   author = {Henry G. {Baker Jr}}
}

@misc{bc-rec,
   month = {February},
   title = {Modelling General Recursion in Type Theory},
   year = {2003},
   note = {Under consideration for publication in Math. Struct. in Comp. Science. Draft, DCS, CTH --- INRIA, Sophia Antipolis, France},
   author = {Ana Bove and Venanzio Capretta}
}

@misc{global-tag,
   title = {Global Tagging Optimization by Type Inference},
   year = {1992},
   author = {Fritz Henglein}
}

@book{esr,
   month = {October},
   title = {The Cathedral And The Bazaar},
   year = {1999},
   publisher = {O'Reilly},
   author = {Eric Raymond}
}

@book{manmonth,
   title = {The Mythical Man-month: Essays on Software Engineering},
   year = {1975},
   publisher = {Addison Wesley},
   author = {Frederick P. Brooks}
}

@inproceedings{evalpush,
   title = {How to make a fast curry: push/enter vs eval/apply},
   year = {2004},
   author = {Simon Marlow and Simon {Peyton Jones}},
   booktitle = {International Conference on Functional Programming, Snowbird},
   pages = {4--15}
}

@phdthesis{boquist-thesis,
   month = {April},
   school = {Chalmers University of Technology},
   title = {Code Optimisation Techniques for Lazy Functional Languages},
   year = {1999},
   author = {Urban Boquist}
}

@book{formal-spec,
   title = {Formal Specification Of Programming Languages},
   year = {1981},
   publisher = {Prentice-Hall},
   author = {Frank G. Pagan}
}

@inproceedings{elim-motive,
   title = {Elimination With A Motive},
   year = {2000},
   booktitle = {Types for Proofs and Programs},
   pages = {197--216},
   editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
   publisher = {Springer},
   author = {Conor McBride}
}

@article{telescope,
   journal = {Information and Computation},
   number = {2},
   month = {April},
   volume = {91},
   title = {Telescoping Mappings in Typed Lambda Calculus},
   year = {1991},
   pages = {189--204},
   author = {N.G. de Bruijn}
}

@misc{typeintype,
   title = {Typechecking is undecidable when 'type' is a type},
   year = {1989},
   author = {Mark B. Reinhold}
}

@misc{core,
   month = {September},
   title = {An External Representation for the {GHC} Core Language},
   year = {2001},
   author = {Andrew Tolmach and {The GHC Team}}
}

@article{deforestation,
   journal = {Theoretical Computer Science},
   volume = {73},
   title = {Deforestation: Transforming programs to eliminate trees},
   year = {1990},
   pages = {231--248},
   author = {Philip Wadler}
}

@misc{hep,
   month = {July},
   title = {Architecture of the {Haskell} Execution Platform},
   year = {1999},
   author = {Julian Seward and Simon Marlow and Andy Gill and Sigbjorn Finne and Simon {Peyton Jones} },
   note = {Version 6},
   howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
}

@mastersthesis{wahlstedt-thesis,
   month = {October},
   school = {Chalmers University Of Technology},
   title = {Detecting Termination Using Size Change In Parameter Values},
   year = {2000},
   author = {David Wahlstedt}
}

@inproceedings{size-change,
   title = {The size-change principle for program termination},
   year = {2001},
   booktitle = {Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
   author = {Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. }
}

@article{ski-turner,
   journal = {Software -- Practice and Experience},
   volume = {9},
   title = {A new implementation technique for applicative languages},
   year = {1979},
   pages = {31--49},
   author = {David Turner}
}

@inproceedings{turner-strong,
   number = {1022},
   title = {Elementary Strong Functional Programming},
   year = {1996},
   booktitle = {First International Symposium on Functional Programming Languages in Education, Nijmegen, Netherlands, December 1995.},
   pages = {1--13},
   publisher = {Springer},
   author = {David Turner},
   series = {LNCS}
}

@misc{clean,
   title = {The {Concurrent CLEAN} Language Report (draft)},
   year = {2003},
   author = {Rinus Plasmeijer and Marko van Eekelen},
   howpublished = {Available from \verb+http://www.cs.kun.nl/~clean/+}
}

@article{burstall-struct,
   journal = {Computer Journal},
   number = {1},
   volume = {12},
   title = {Proving Properties of Programs By Structural Induction},
   year = {1969},
   pages = {41--48},
   author = {Rod Burstall}
}

@incollection{ barendregt-types,
    author = "Henk Barendregt",
    title = "Lambda Calculi with Types",
    booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky \& Gabbay \& Maibaum (Eds.)",
    publisher = "Clarendon",
    volume = "2",
    year = "1992",
    url = "citeseer.nj.nec.com/barendregt92lambda.html" }

@book{curry-feys,
   title = {Combinatory Logic, volume 1},
   year = {1958},
   publisher = {North Holland},
   author = {Haskell B. Curry and Robert Feys}
}

@phdthesis{bove-thesis,
   month = {November},
   school = {Chalmers University of Technology},
   title = {General Recursion in Type Theory},
   year = {2002},
   author = {Ana Bove}
}

@inbook{ml-cm,
   title = {Constructive Mathematics and Computer Programming},
   year = {1985},
   booktitle = {Mathematical Logic and Programming Languages},
   publisher = {Prentice Hall},
   author = {Per Martin-L\"{o}f}
}

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

@inproceedings{talx86,
   title = {TALx86: A Realistic Typed Assembly Language},
   year = {1999},
   booktitle = {ACM SIGPLAN Workshop on Compiler Support for System Software},
   pages = {25--35},
   author = {Greg Morrisett and Karl Crary and Neal Glew and Dan Grossman and Richard Samuels and Frederick Smith and David Walker and Stephanie Weirich and Steve Zdancewic}
}

@inproceedings{bove-capretta,
   volume = {2152},
   title = {Nested General Recursion and Partiality in Type Theory},
   year = {2001},
   booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLS 2001},
   pages = {121--135},
   editor = {Richard J. Boulton and Paul B. Jackson},
   publisher = {Springer-Verlag},
   author = {Ana Bove and Venanzio Capretta},
   series = {LNCS}
}

@misc{lvm,
   month = {November},
   title = {LVM, the lazy virtual machine},
   year = {2002},
   author = {Daan Leijen}
}

@misc{ocaml,
   howpublished = {\verb+http://caml.inria.fr/ocaml/htmlman/+},
   month = {August},
   title = {The {Objective Caml} system release 3.06},
   year = {2002},
   author = {Xavier Leroy}
}

@misc{lambdagoto,
   title = {Lambda : The Ultimate Goto},
   year = {1977},
   author = {Guy L. {Steele Jr}},
   note = {MIT AI Memo 443}
}

@inproceedings{ liu-tail,
    author = "Yanhong A. Liu and Scott D. Stoller",
    title = "From Recursion to Iteration: What are the Optimizations?",
    booktitle = "Partial Evaluation and Semantic-Based Program Manipulation",
    pages = "73-82",
    year = "2000",
    url = "citeseer.nj.nec.com/liu00from.html" }

@inproceedings{aczel77,
   title = {An Introduction To Inductive Definitions},
   year = {1977},
   booktitle = {Handbook of Mathematical Logic},
   editor = {J. Barwise},
   publisher = {North Holland},
   author = {Peter Aczel}
}

@inproceedings{inductive-plastic,
   volume = {1956},
   title = {Implementation Techniques for Inductive Types in {Plastic}},
   year = {1999},
   booktitle = {Types for Proofs and Programs},
   pages = {94--113},
   editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith},
   publisher = {Springer-Verlag},
   author = {Paul Callaghan and Zhaohui Luo},
   series = {LNCS}
}

@misc{graham,
   howpublished = {Available from \verb+http://www.paulgraham.com/+},
   month = {April},
   title = {The Hundred Year Language},
   year = {2003},
   author = {Paul Graham},
   note = {Keynote address at PyCon 2003}
}

@inproceedings{gimenez98,
   volume = {1443},
   title = {Structural Recursive Definitions in Type Theory},
   year = {1998},
   booktitle = {Proceedings of ICALP '98},
   publisher = {Springer-Verlag},
   author = {Eduardo Gim\'{e}nez},
   series = {LNCS}
}

@article{quicksort,
   journal = {Computer Journal},
   number = {1},
   volume = {5},
   title = {Quicksort},
   year = {1962},
   pages = {10--15},
   author = {C.A.R. Hoare}
}

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

@article{ph-universes,
   journal = {Theoretical Computer Science},
   number = {1},
   volume = {89},
   title = {Type Checking With Universes},
   year = {1991},
   pages = {107--136},
   author = {Robert Harper and Randy Pollack}
}

@inproceedings{pm-compile,
   month = {September},
   title = {Compiling Pattern Matching},
   year = {1985},
   booktitle = {Functional Programming Languages and Computer Architecture},
   pages = {368--381},
   editor = {Jean-Pierre Jouannaud},
   publisher = {Springer-Verlag},
   author = {Lennart Augustsson}
}

@phdthesis{lena-thesis,
   school = {Chalmers University of Technology, G\"{o}teborg},
   title = {The implementation of {ALF} -- A Proof Editor based on {Martin-L\"{o}f}'s Monomorphic Type Theory with Explicit Substitutions},
   year = {1994},
   author = {Lena Magnusson}
}

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

@inproceedings{not-a-number,
  author = {Conor McBride and James McKinna},
  title = {I am not a number, {I} am a free variable},
  year = {2004},
  booktitle = {Proceedings of the ACM SIGPLAN Haskell Workshop}
}


@misc{profiling,
   title = {Time and Space Profiling for Non-Strict, Higher Order  Functional Languages},
   year = {1995},
   author = {Patrick M. Sansom and Simon {Peyton Jones}}
}

@inbook{pattern-matching,
   title = {The Implementation of Functional Programming Languages},
   year = {1987},
   booktitle = {The Implementation of Functional Programming Languages},
   pages = {78--103},
   editor = {Simon {Peyton Jones}},
   chapter = {5},
   publisher = {Prentice Hall},
   author = {Philip Wadler},
   crossref = {pj-imp}
}

@misc{tag-elim,
   title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},
   year = {2000},
   author = {Walid Taha and Henning Makholm}
}

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

@phdthesis{mcbride-snr-thesis,
   school = {Queen's University of Belfast},
   title = {Computer Aided Manipulation of Symbols},
   year = {1970},
   author = {Fred McBride}
}

@article{ho-strictness,
   journal = {Science of Computer Programming},
   volume = {7},
   title = {Strictness analysis for higher-order functions},
   year = {1986},
   pages = {249--278},
   author = { Geoffrey L. Burn and Chris Hankin and Samson Abramsky}
}

@phdthesis{mycroft-thesis,
   school = {Dept Computer Science, University of Edinburgh},
   title = {Abstract interpretation and optimising transformations for applicative programs},
   year = {1981},
   author = {A. Mycroft}
}

@inproceedings{bc-nested,
   month = {September},
   volume = {2152},
   title = {Nested General Recursion and Partiality in Type Theory},
   year = {2001},
   booktitle = {Theorem Proving In Higher Order Logics: 14th International Conferences, TPHOLS 2001},
   pages = {121--135},
   publisher = {Springer--Verlag},
   author = {Ana Bove and Venanzio Capretta},
   series = {LNCS}
}

@techreport{bove-mutual,
   month = {May},
   title = {Mutual General Recursion in Type Theory},
   year = {2002},
   institution = {Department of Computing Science, Chalmers University of Technology},
   author = {Ana Bove}
}

@article{berardi-pruning,
   journal = {Journal of Logic and Computation},
   number = {5},
   volume = {6},
   title = {Pruning Simply Typed Lambda Terms},
   year = {1996},
   pages = {663--681},
   author = {Stefano Berardi}
}

@article{milner-tc,
   journal = {Journal of Computer and System Science},
   volume = {17},
   title = {A Theory of Type Polymorphism in Programming},
   year = {1978},
   pages = {348--75},
   author = {R. Milner}
}

@inproceedings{extt,
   title = {Inductive Families Need Not Store Their Indices},
   year = {2004},
   booktitle = {Types for Proofs and Programs 2003},
   author = {Edwin Brady and Conor McBride and James McKinna},
   editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
   publisher = {Springer},
   volume = {3085},
   pages = {115--129}
}

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

@article{backus78,
   journal = {Communications of the ACM},
   month = {August},
   volume = {21},
   title = {Can Programming Be Liberated From the {Von Neumann} Style?},
   year = {1978},
   pages = {280--294},
   author = {John Backus}
}

@misc{henk,
   month = {May},
   title = {Henk: A Typed Intermediate Language},
   year = {1997},
   author = {Simon {Peyton Jones} and Erik Meijer}
}

@article{thunks,
   journal = {Journal of Functional Programming},
   number = {3},
   month = {May},
   volume = {7},
   title = {Thunks and the $\lambda$-calculus},
   year = {1997},
   pages = {303--319},
   author = {John Hatcliff and Olivier Danvy}
}

@inproceedings{grin-project,
    author = "Urban Boquist and Thomas Johnsson",
    title = "The {GRIN} Project: A Highly Optimising Back End for Lazy Functional Languages",
    booktitle = "Implementation of Functional Languages",
    pages = "58--84",
    year = "1996",
    url = "citeseer.ist.psu.edu/boquist96grin.html" }

@misc{boehm-gc,
   howpublished = {\verb+http://www.hpl.hp.com/personal/Hans_Boehm/gc/+},
   title = {A garbage collector for {C} and {C++}},
   year = {2001},
   author = {Hans-J. Boehm and Alan J. Demers and {Xerox Corporation Silicon Graphic} and {Hewlett-Packard Company}}
}

@misc{art-interpreter,
   month = {May},
   title = {The Art of the Interpreter or, the Modularity Complex (Parts Zero, One, and Two)},
   year = {1978},
   author = {Guy Lewis {Steele, Jr.} and Gerald Jay Sussman},
   note = {MIT AI Lab. AI Lab Memo AIM-453}
}

@inproceedings{gimenez,
   title = {Codifying Guarded Definitions With Recursive Schemes},
   year = {1994},
   booktitle = {Proceedings of TYPES 1994},
   pages = {39--59},
   author = {Eduardo Gim\'{e}nez}
}

@manual{ghc-manual,
   title = {The Glasgow Haskell Compiler User's Guide, Version 6.0},
   year = {2003},
   author = {The {GHC Team}}
}

@article{rbtree,
   journal = {Journal of Functional Programming},
   number = {4},
   month = {May},
   volume = {9},
   title = {Red-Black Trees In A Functional Setting},
   year = {1999},
   pages = {471--477},
   author = {Chris Okasaki}
}

@inproceedings{dt-data,
author = "Hongwei Xi",
title = {{Dependently Typed Data Structures}},
booktitle = "Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99)",
year = 1999,
month = "September",
pages = "17--32",
address = "Paris",
}

@misc{krivine,
   title = {On the Correctness and Efficiency of the {Krivine} Machine},
   year = {2003},
   month = {October},
   author = {Mitchell Wand and Daniel P. Friedman},
   howpublished = {Submitted for publication}
   }

@inproceedings{nbe-filinski,
   title = {Normalization by Evaluation for the Computational Lambda-Calculus},
   year = {2001},
   month = {May},
   booktitle = {Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001},
   author = {Andrzej Filinski},
   pages = {151--165},
   publisher = {Springer-Verlag},
   series = {LNCS},
   volume = {2044}
}

@inproceedings{filinski-nbesem,
   title = {A semantic account of type-directed partial evaluation},
   year = {1999},
   author = {Andrzej Filinski},
   editor = {G. Nadathur},
   booktitle = {International Conference on Principles and Practice of Declarative Programming},
   volume = {1702},
   series = {LNCS},
   pages = {378--395},
   publisher = {Springer-Verlag}
}

@article{secd,
   title = {The mechanical evaluation of expressions},
   author = {P.J. Landin},
   year = {1964},
   journal = {Computer Journal},
   volume = {6},
   pages = {308--320}
}

@misc{lispkit,
   title = {The {LispKit} Manual},
   author = {Peter Henderson and Geraint Jones and Simon Jones},
   year = {1982},
   howpublished = {Oxford University Computing Laboratory}
}

@inproceedings{wells-undecidable,
   title = {Typability and Type Checking in the Second-order $\lambda$-calculus are equivalent and undecidable},
   author = {J. Wells},
   year = {1994},
   month = {July},
   booktitle = {Proc. 9th Ann. IEEE Symp. Logic Comput. Sci.}
}

@misc{patguards,
   title = {Pattern Guards and Transformational Patterns},
   author = {Martin Erwig and Simon {Peyton Jones}},
   year = {2000},
   howpublished = {Haskell Workshop}
}

@misc{alfa-manual,
  title = {Alfa Users' Guide},
  author = {Thomas Hallgren},
  year = {2001},
  howpublished = {Available from \verb+http://www.cs.chalmers.se/~hallgren/Alfa/+}
}
   
@inproceedings{nofib,
  title = {The nofib Benchmark Suite of {Haskell} Programs},
  author = {Will Partain},
  year = {1992},
  booktitle = {Functional Programming},
  editor = {J. Launchbury and P.L. Sansom},
  series = {Workshops in Computing},
  publisher = {Springer Verlag}
}

@article{shape,
   title = {Shape in Computing},
   author = {Barry Jay},
   journal = 	 "{ACM} Computing Surveys",
   year = 	 "1996",
   volume = 	 "28",
   number = 	 "2",
   pages = 	 "355--357",
}

@misc{ffi,
   title = {The {Haskell 98} Foreign Function Interface 1.0: An Addendum to the {Haskell 98} Report},
   editor = {Manuel Chakravarty},
   key = {FFI},
   year = {2002},
   month = {December},
   howpublished = {Available from \verb+http://www.haskell.org/+}
}

@misc{perlxs,
   title = {Perl {XS} Reference Manual},
   author = {Dean Roehrich and {The Perl Porters}},
   year = {1996},
   howpublished = {\verb+http://www.perldoc.com/perl5.6/pod/perlxs.html+}
}

@misc{swig,
   title = {{SWIG} : An Easy to Use Tool for Integrating Scripting Languages with {C} and {C++}},
   author = {David M. Beazley},
   year = {1996},
   howpublished = {\verb+http://www.swig.org/papers/Tcl96/tcl96.html+}
}

@inproceedings{types-prog,
   title = {Type Systems for Programming Languages},
   booktitle = {Handbook of Theoretical Computer Science},
   author = {John C. Mitchell},
   pages = {365--458},
   year = {1990},
   crossref = {htcs}
}

@book{htcs,
   title = {Handbook of Theoretical Computer Science},
   editor = {J. van Leeuwen},
   publisher = {Elsevier Science},
   year = {1990}
}

@misc{r5rs,
   title = {Revised$^5$ Report on the Algorithmic Language Scheme},
   author = {Richard Kelsey and William Clinger and Jonathan Rees},
   year = {1998},
   month = {February},
   howpublished = {Available from \verb+http://www.schemers.org/+}
 }