literature.bib

@inproceedings{res-dsl-padl12,
  title =        {Resource-safe Systems Programming with Embedded
                  Domain Specific Languages},
  year =         2012,
  booktitle =    {Practical Applications of Declarative Languages
                  2012},
  author =       {Edwin Brady and Kevin Hammond},
  series =       {LNCS},
  publisher =    {Springer},
  note =         {To appear}
}

@article{lambdapi,
  author =       {Andres L\"{o}h and Conor McBride and Wouter
                  Swierstra},
  title =        {A tutorial implementation of a dependently typed
                  lambda calculus},
  year =         2010,
  journal =      {Fundamenta Informaticae},
  volume =       102,
  number =       2
}  

@article{idioms,
  author =       {McBride, Conor and Paterson, Ross},
  title =        {Applicative programming with effects},
  journal =      {J. Funct. Program.},
  volume =       18,
  issue =        1,
  month =        {January},
  year =         2008,
  issn =         {0956-7968},
  pages =        {1--13},
  numpages =     13,
  url =
                  {http://portal.acm.org/citation.cfm?id=1348940.1348941},
  doi =          {10.1017/S0956796807006326},
  acmid =        1348941,
  publisher =    {Cambridge University Press},
  address =      {New York, NY, USA},
} 

@inproceedings{lava,
  author =       {Bjesse, Per and Claessen, Koen and Sheeran, Mary and
                  Singh, Satnam},
  title =        {Lava: hardware design in {Haskell}},
  booktitle =    {Proceedings of the third ACM SIGPLAN international
                  conference on Functional programming},
  series =       {ICFP '98},
  year =         1998,
  isbn =         {1-58113-024-4},
  location =     {Baltimore, Maryland, United States},
  pages =        {174--184},
  numpages =     11,
  url =          {http://doi.acm.org/10.1145/289423.289440},
  doi =          {10.1145/289423.289440},
  acmid =        289440,
  publisher =    ACM,
  address =      {New York, NY, USA},
} 

@inproceedings{plpv11,
  author =       {Edwin Brady},
  title =        {Idris --- Systems programming meets full dependent
                  types},
  booktitle =    {Programming Languages meets Program Verification
                  {(PLPV 2011)}},
  year =         2011,
  pages =        {43--54},
  ee =           {http://doi.acm.org/10.1145/1929529.1929536},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{epic-tfp,
  author =       {Edwin Brady},
  title =        {Epic --- a library for generating compilers},
  year =         2011,
  booktitle =    {{Trends in Functional Programming} ({TFP} '11)},
  note =         {To appear}
}

@inproceedings{ynot08,
  author =       {Nanevski,, Aleksandar and Morrisett,, Greg and
                  Shinnar,, Avraham and Govereau,, Paul and Birkedal,,
                  Lars},
  title =        {Ynot: reasoning with the awkward squad},
  booktitle =    {{ICFP} '08: Proceeding of the 13th {ACM SIGPLAN}
                  international conference on Functional programming},
  year =         2008,
  isbn =         {978-1-59593-919-7},
  pages =        {229--240},
  location =     {Victoria, BC, Canada},
  doi =          {http://doi.acm.org/10.1145/1411204.1411237},
  publisher =    acm,
  address =      {New York, NY, USA},
}

@article{cbconc-fi,
  author =       {Edwin Brady and Kevin Hammond},
  title =        {Correct-by-Construction Concurrency: Using Dependent
                  Types to Verify Implementations of Effectful
                  Resource Usage Protocols},
  year =         2010,
  journal =      {Fundamenta Informaticae},
  volume =       102,
  number =       2,
  pages =        {145--176}
}  

@inproceedings{devil-osdi00,
  author =       {Fabrice M{\'e}rillon and Laurent R{\'e}veill{\`e}re
                  and Charles Consel and Renaud Marlet and Gilles
                  Muller},
  title =        {Devil: An IDL for Hardware Programming},
  booktitle =    {4th USENIX Symposium on Operating Systems Design and
                  Implementation (OSDI 2000)},
  year =         2000
}


@INPROCEEDINGS{device-osdi08,
  author =       {Dan Williams and Patrick Reynolds and Kevin Walsh
                  and Emin Gün Sirer and Fred B. Schneider},
  title =        {Device driver safety through a reference validation
                  mechanism},
  booktitle =    {8th USENIX Symposium on Operating Systems Design and
                  Implementation (OSDI 2008)},
  year =         2008
}

@inproceedings{sozeau-equations,
  author =       {Matthieu Sozeau},
  title =        {Equations: A Dependent Pattern-Matching Compiler},
  booktitle =    {First International Conference on Interactive
                  Theorem Proving (ITP 2010)},
  year =         2010,
  pages =        {419--434},
  url =           {http://dx.doi.org/10.1007/978-3-642-14052-5_29},
  crossref =     {DBLP:conf/itp/2010},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{packet-type,
  author =       "Peter J. McCann and Satish Chandra",
  title =        "Packet Types: Abstract Specification of Network
                  Protocol Messages",
  year =         2000,
  booktitle =    "SIGCOMM '00",
  publisher =    {acm}
}

@inproceedings{qs-types,
  author =       {Eelis {van der Weegen} and James McKinna},
  title =        {A Machine-checked Proof of the Average-case
                  Complexity of Quicksort in Coq},
  year =         {2009},
  pages =        {256--271},
  series =       {Lecture Notes in Computer Science},
  publisher =    {Springer}
}

@inproceedings{totalparser,
  author =       {Nils Anders Danielsson},
  title =        {Total Parser Combinators},
  booktitle =    {{ICFP} '10: Proceedings of the 15th acm {SIGPLAN}
                  International Conference on Functional Programming},
  year =         2010,
  isbn =         {978-1-60558-794-3},
  pages =        {285--296},
  location =     {Baltimore, Maryland, USA},
  doi =          {10.1145/1863543.1863587},
  publisher =    {acm},
  address =      {New York, NY, USA},
}

@misc{rfc791,
  author =       "J. Postel",
  title =        "{Internet Protocol}",
  series =       "Request for Comments",
  number =       791,
  howpublished = "RFC 791 (Standard)",
  publisher =    "IETF",
  organization = "Internet Engineering Task Force",
  year =         1981,
  month =        sep,
  note =         "Updated by RFC 1349",
  url =          "http://www.ietf.org/rfc/rfc791.txt",
}


@misc{rfc792,
  author =       "J. Postel",
  title =        "{Internet Control Message Protocol}",
  series =       "Request for Comments",
  number =       792,
  howpublished = "RFC 792 (Standard)",
  publisher =    "IETF",
  organization = "Internet Engineering Task Force",
  year =         1981,
  month =        sep,
  note =         "Updated by RFCs 950, 4884",
  url =          "http://www.ietf.org/rfc/rfc792.txt",
}

@INPROCEEDINGS{Dybjer-indrec,
  author =       {Peter Dybjer and Anton Setzer},
  title =        {A Finite Axiomatization of Inductive-Recursive
                  Definitions},
  booktitle =    {Tyed Lambda Calculi and Applications},
  volume =       1581,
  series =       {Lecture Notes in Computer Science},
  year =         1998,
  pages =        {129--146},
  publisher =    {Springer}
}

@book{stevenstcpip,
  author =       {W. Richard Stevens},
  title =        {{TCP/IP} Illustrated Volume 1: The Protocols},
  year =         1994,
  publisher =    {Addison Wesley},
  isbn =         {0-201-63346-9}
}

@inproceedings{coqtypeclasses,
  author =       {Sozeau, Matthieu and Oury, Nicolas},
  title =        {First-Class Type Classes},
  booktitle =    {TPHOLs '08: Proceedings of the 21st International
                  Conference on Theorem Proving in Higher Order
                  Logics},
  year =         2008,
  isbn =         {978-3-540-71065-3},
  pages =        {278--293},
  location =     {Montreal, P.Q., Canada},
  doi =          {10.1007/978-3-540-71067-7_23},
  publisher =    {Springer-Verlag},
  address =      {Berlin, Heidelberg},
}


@inproceedings{kipling,
  author =       {McBride, Conor},
  title =        {Outrageous but meaningful coincidences: dependent
                  type-safe syntax and evaluation},
  booktitle =    {WGP '10: Proceedings of the 6th acm {SIGPLAN}
                  workshop on Generic programming},
  year =         2010,
  isbn =         {978-1-4503-0251-7},
  pages =        {1--12},
  location =     {Baltimore, Maryland, USA},
  doi =          {10.1145/1863495.1863497},
  publisher =    {acm},
  address =      {New York, NY, USA},
}

@inproceedings{padsml,
  author =       {Yitzhak Mandelbaum and Kathleen Fisher and David
                  Walker and Mary F. Fern{\'a}ndez and Artem Gleyzer},
  title =        {{PADS/ML}: a functional data description language},
  booktitle =    {POPL '07: Proceedings of the 34th acm
                  {SIGPLAN}-SIGACT Symposium on Principles of
                  Programming Languages, POPL 2007, Nice, France,
                  January 17-19, 2007},
  year =         2007,
  pages =        {77-83},
  url =          {http://doi.acm.org/10.1145/1190216.1190231},
  crossref =     {DBLP:conf/popl/2007},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/popl/2007,
  editor =       {Martin Hofmann and Matthias Felleisen},
  title =        {Proceedings of the 34th acm {SIGPLAN}-SIGACT
                  Symposium on Principles of Programming Languages,
                  POPL 2007, Nice, France, January 17-19, 2007},
  booktitle =    {POPL},
  publisher =    {acm},
  year =         2007,
  isbn =         {1-59593-575-4},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{melange,
  author =       {Madhavapeddy, Anil and Ho, Alex and Deegan, Tim and
                  Scott, David and Sohan, Ripduman},
  title =        {Melange: creating a "functional" internet},
  booktitle =    {EuroSys '07: Proceedings of the 2nd acm
                  SIGOPS/EuroSys European Conference on Computer
                  Systems 2007},
  year =         2007,
  isbn =         {978-1-59593-636-3},
  location =     {Lisbon, Portugal},
  doi =          {http://doi.acm.org/10.1145/1272996.1273009},
  publisher =    {acm},
  address =      {New York, NY, USA},
}



@article{next700data,
  author =       {Fisher, Kathleen and Mandelbaum, Yitzhak and Walker,
                  David},
  title =        {The next 700 data description languages},
  journal =      {{SIGPLAN} Not.},
  volume =       41,
  number =       1,
  year =         2006,
  issn =         {0362-1340},
  pages =        {2--15},
  doi =          {http://doi.acm.org/10.1145/1111320.1111039},
  publisher =    {acm},
  address =      {New York, NY, USA},
}


@INPROCEEDINGS{xi-ats,
  author =       {Hongwei Xi},
  title =        {{Applied Type System} (extended abstract)},
  booktitle =    {Types for Proofs and Programs 2003},
  editor =       {Stefano Berardi and Mario Coppo and Ferruccio
                  Damiani},
  publisher =    {Springer},
  series =       {Lecture Notes in Computer Science},
  volume =       3085,
  year =         2004,
  pages =        {394--408}
}

@inproceedings{powerpi,
  author =       {Nicolas Oury and Wouter Swierstra},
  title =        {The power of {Pi}},
  booktitle =    {{ICFP} '08: Proceedings of the 13th acm {SIGPLAN}
                  International Conference on Functional Programming,
                  {ICFP} 2008, Victoria, BC, Canada, September 20-28,
                  2008},
  year =         2008,
  pages =        {39--50},
  ee =           {http://doi.acm.org/10.1145/1411204.1411213},
  crossref =     {DBLP:conf/ICFP/2008},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ICFP/2008,
  editor =       {James Hook and Peter Thiemann},
  title =        {Proceeding of the 13th acm {SIGPLAN} international
                  conference on Functional programming, {ICFP} 2008,
                  Victoria, BC, Canada, September 20-28, 2008},
  booktitle =    {{ICFP}},
  publisher =    {acm},
  year =         2008,
  isbn =         {978-1-59593-919-7},
  bibsource =    {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{security-types,
  author =       {Morgenstern, Jamie and Licata, Daniel R.},
  title =        {Security-typed programming within dependently typed
                  programming},
  booktitle =    {{ICFP} '10: Proceedings of the 15th acm {SIGPLAN}
                  International Conference on Functional Programming},
  year =         2010,
  isbn =         {978-1-60558-794-3},
  pages =        {169--180},
  location =     {Baltimore, Maryland, USA},
  doi =          {10.1145/1863543.1863569},
  publisher =    {acm},
  address =      {New York, NY, USA},
}

@INPROCEEDINGS{awkward,
    author = {Simon {Peyton Jones}},
    title = {Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in {Haskell}},
    booktitle = {Engineering theories of software construction},
    year = 2001,
    pages = {47--96}
}

@inproceedings{scrap-engine,
  author =       {Brady, Edwin and Hammond, Kevin},
  title =        {Scrapping your inefficient engine: using partial
                  evaluation to improve domain-specific language
                  implementation},
  booktitle =    {{ICFP} '10: Proceedings of the 15th acm {SIGPLAN}
                  International Conference on Functional Programming},
  year =         2010,
  isbn =         {978-1-60558-794-3},
  pages =        {297--308},
  location =     {Baltimore, Maryland, USA},
  doi =          {10.1145/1863543.1863587},
  publisher =    {acm},
  address =      {New York, NY, USA},
}

@article{urweb,
  author =       {Chlipala, Adam},
  title =        {Ur: statically-typed metaprogramming with type-level
                  record computation},
  journal =      {{SIGPLAN} Not.},
  volume =       45,
  number =       6,
  year =         2010,
  issn =         {0362-1340},
  pages =        {122--133},
  doi =          {10.1145/1809028.1806612},
  publisher =    {acm},
  address =      {New York, NY, USA},
}



@phdthesis{norell-thesis,
  author =       {Ulf Norell},
  title =        {Towards a practical programming language based on
                  dependent type theory},
  school =       {Chalmers University of Technology},
  year =         2007,
  month =        {September},
}

@inproceedings{open-type,
  author =       {Schrijvers, Tom and Peyton Jones, Simon and
                  Chakravarty, Manuel and Sulzmann, Martin},
  title =        {Type checking with open type functions},
  booktitle =    {International Conf. on Functional Programming
                  ({ICFP} 2008)},
  year =         {2008},
  pages =        {51--62},
  doi =          {http://doi.acm.org/10.1145/1411203.1411215},
  publisher =    {acm},
  address =      {New York, NY, USA},
}

@inproceedings{ngna-dsl,
  title =        {Domain Specific Languages ({DSL}s) for Network
                  Protocols},
  author =       {Saleem Bhatti and Edwin Brady and Kevin Hammond and
                  James McKinna},
  year =         2009,
  booktitle =    {International Workshop on Next Generation Network
                  Architecture ({NGNA} 2009)}
}

@phdthesis{gill-thesis,
  title =        {Cheap deforestation for non-strict functional
                  languages},
  author =       {A Gill},
  institution =  {University of Glasgow},
  month =        {January},
  year =         1996
}

@misc{llvm-haskell,
  title =        {Low Level Virtual Machine for {Glasgow Haskell
                  Compiler}},
  author =       {David Terei},
  year =         2009,
  howpublished = {Bachelor's Thesis, Computer Science and Engineering
                  Dept., The University of New South Wales, Sydney,
                  Australia}
}

@mastersthesis{llvm,
  title =        {{LLVM}: An Infrastructure for Multi-Stage
                  Optimization},
  author =       {Chris Lattner},
  year =         2002,
  month =        {December},
  institution =  {Computer Science Dept., University of Illinois at
                  Urbana-Champaign}
}

@inproceedings{gpu-arrays,
  title =        {GPU Kernels as Data-Parallel Array Computations in
                  Haskell},
  author =       {Sean Lee and Manuel M. T. Chakravarty and Vinod
                  Grover and Gabriele Keller.},
  year =         2009,
  booktitle =    {Workshop on Exploiting Parallelism using GPUs and
                  other Hardware-Assisted Methods (EPAHM 2009)}
}

@misc{cryptol,
  author =       {Galois, Inc.},
  title =        {Cryptol},
  year =         2009,
  howpublished = {Online]},
  url =          {http://cryptol.net/}
}

@inproceedings{paradise-dsl,
  author =       {Lennart Augustsson and Howard Mansell and Ganesh
                  Sittampalam},
  title =        {{Paradise: a two-stage DSL embedded in Haskell}},
  booktitle =    {International Conf. on Functional Programming
                  ({ICFP} 2008)},
  year =         {2008},
  publisher =    {acm},
  pages =        {225--228}
}

@misc{dsl-bib,
  author =       {Arie {van Deursen} and Paul Klint and Joost Visser},
  title =        {Domain-Specific Languages --- an annotated
                  bibliography},
  year =         2000,
  howpublished = {Online},
  url =          {http://homepages.cwi.nl/~arie/papers/dslbib/}
}

@inproceedings{imperative-pe,
  author =       {Debois, S{\o}ren},
  title =        {Imperative program optimization by partial
                  evaluation},
  booktitle =    {PEPM '04: Proceedings of the 2004 acm {SIGPLAN}
                  symposium on Partial evaluation and semantics-based
                  program manipulation},
  year =         {2004},
  isbn =         {1-58113-835-0},
  pages =        {113--122},
  location =     {Verona, Italy},
  doi =          {http://doi.acm.org/10.1145/1014007.1014019},
  publisher =    {acm},
  address =      {New York, NY, USA},
}


@inproceedings{offline-pe-termination,
  author =       {Andersen, Peter Holst and Holst, Carsten Kehler},
  title =        {Termination Analysis for Offline Partial Evaluation
                  of a Higher Order Functional Language},
  booktitle =    {Proc. SAS '96: Intl. Symp. on Static Analysis},
  year =         {1996},
  isbn =         {3-540-61739-6},
  pages =        {67--82},
  publisher =    {Springer},
  notaddress =   {London, UK},
}


@inproceedings{stage-duplication,
  author =       {Swadi, Kedar and Taha, Walid and Kiselyov, Oleg and
                  Pasalic, Emir},
  title =        {A monadic approach for avoiding code duplication
                  when staging memoized functions},
  notbooktitle = {PEPM '06: Proceedings of the 2006 acm {SIGPLAN}
                  symposium on Partial evaluation and semantics-based
                  program manipulation},
  booktitle =    {Proc. PEPM '06:acm Symp. on Partial Evaluation and
                  Semantics-based Program Manipulation},
  year =         2006,
  isbn =         {1-59593-196-1},
  pages =        {160--169},
  location =     {Charleston, South Carolina},
  doi =          {http://doi.acm.org/10.1145/1111542.1111570},
  notpublisher = {acm},
  notaddress =   {New York, NY, USA},
}


@inproceedings{concoqtion,
 author = {Fogarty, Seth and Pasalic, Emir and Siek, Jeremy and Taha, Walid},
 title = {Concoqtion: indexed types now!},
 booktitle = {PEPM '07: Proceedings of the 2007 acm {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
 year = {2007},
 isbn = {978-1-59593-620-2},
 pages = {112--121},
 location = {Nice, France},
 doi = {http://doi.acm.org/10.1145/1244381.1244400},
 publisher = {acm},
 address = {New York, NY, USA},
 }

@inproceedings{metahaskell,
    author = "Tim Sheard and Simon {Peyton Jones}",
    title = "Template metaprogramming for {Haskell}",
    booktitle = "acm Haskell Workshop",
    year = 2002,
    month = oct, 
    pages = "1-16",
    noteditor = "Manuel M. T. Chakravarty",
    notpublisher = "acm Press"
}

@misc{shark-profiler,
    title = {Optimizing your application with {Shark 4}},
    year = 2009,
    howpublished = {\url{http://developer.apple.com/tools/sharkoptimize.html}}
}

@misc{shootout,
    title = {The Computer Language Benchmark Game},
    year = {2009},
    howpublished = {\url{http://shootout.alioth.debian.org/}}
}

@article{futamura,
    author = {Yoshihiko Futamura},
    year = 1971,
    title = "Partial Evaluation of Computation Process --– An Approach to a Compiler-Compiler",
    journal = {Systems, Comps., Controls},
    volume = 2,
    number = 5,
    pages = {45-–50}
}

@book{pebook,
    title = {Partial Evaluation and Automatic Program Generation},
    author = {N.D. Jones and C.K. Gomard and P. Sestoft},
    year = 1993,
    publisher = {Prentice Hall International}
}

@inproceedings{pantheon,
    author = {Sean Seefried and Manuel Chakravarty and Gabriele Keller},
    title = {Optimising Embedded {DSLs} using {Template Haskell}},
    year = {2004},
    booktitle = {{Proc. GPCE~'04: Conf. Generative Prog. and Component Eng.}},
    publisher = {Springer},
    series = {LNCS}
}

@article{pan,
 author = {Elliott, Conal and Finne, Sigbj\orn and De Moor, Oege},
 title = {Compiling embedded languages},
 journal = {J. Funct. Program.},
 volume = {13},
 number = {3},
 year = {2003},
 issn = {0956-7968},
 pages = {455--481},
 doi = {http://dx.doi.org/10.1017/S0956796802004574},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }


@inproceedings{russell,
 author = {Sozeau, Matthieu},
 title = {Program-ing finger trees in Coq},
 booktitle = {{ICFP} '07: Proceedings of the 12th acm {SIGPLAN} international conference on Functional programming},
 year = {2007},
 isbn = {978-1-59593-815-2},
 pages = {13--24},
 location = {Freiburg, Germany},
 doi = {http://doi.acm.org/10.1145/1291151.1291156},
 publisher = {acm},
 address = {New York, NY, USA},
 }

@inproceedings{turner-total,
    author = {D. A. Turner},
    title = {Elementary Strong Functional Programming},
    year = 1995,
    booktitle = "First International Symposium on Functional Programming Languages in Education", 
    publisher = {Springer},
    series = {LNCS},
    volume = {1022},
    pages = {1--13}
}

@incollection{free-theorems,
    author = "P. Wadler",
    title = "Theorems for Free!",
    booktitle = "{Proc. 4th Int.\ Conf.\ on Funct.\ Prog.\ Languages and Computer Arch., {FPCA}'89, London, {UK}, 11--13 Sept 1989}",
    publisher = "acm Press",
    address = "New York",
    pages = "347--359",
    year = "1989",
    url = "citeseer.ist.psu.edu/wadler89theorems.html" 
}

@inproceedings{TrulyConcurrent,
 author = {Naiyong Jin and Jifeng He},
 title = {Towards A Truly Concurrent Model for Processes Sharing Resources},
 booktitle = {Proc. 3rd {IEEE} International Conf. on Soft. Eng. and Formal Methods},
 year = {2005},
 isbn = {0-7695-2435-4},
 pages = {231--239},
 doi = {http://dx.doi.org/10.1109/SEFM.2005.50},
 publisher = {{IEEE} Computer Society},
 address = {Washington, DC, USA},
 }

@misc{GPCE2006,
   note = {Omitted to preserve anonymity, contact PC chair for details}
}

@misc{IFL2006,
   note = {Omitted to preserve anonymity, contact PC chair for details}
}

@misc{ivor-anon,
   note = {Omitted to preserve anonymity, contact PC chair for details}
}

@inproceedings{HaskellIO,
 author = {Simon L. {Peyton Jones} and Philip Wadler},
 title = {Imperative functional programming},
 booktitle = {Proc. 20th acm Symposium on Principles of programming languages},
 year = {1993},
 isbn = {0-89791-560-7},
 pages = {71--84},
 location = {Charleston, South Carolina, United States},
 doi = {http://doi.acm.org/10.1145/158511.158524},
 publisher = {acm},
 address = {New York, NY, USA},
 }

@article{CorrectnessConstruction,
author = "P. Amey",
title  = "{Correctness by Construction: Better can also be Cheaper}",
journal = "{CrossTalk: the Journal of Defense Software Engineering}",
month = mar,
year = 2002,
pages = "24--28"
}



@INPROCEEDINGS{hj:popl03,
  AUTHOR =       {M. Hofmann and S. Jost},
  TITLE =        {Static Prediction of Heap Space Usage for First-Order Function
al Programs},
booktitle = "Proc. {POPL 2003 --- 2003 acm Symp. on Principles of Programming La
nguages}",
  KEY =          {HJ_POPL03},
  PAGES =        {185--197},
  YEAR =         {2003},
  ORGANIZATION = {acm}
}


@article{kobayashi-lock,
 author = {Naoki Kobayashi},
 title = {A type system for lock-free processes},
 journal = {Inf. Comput.},
 volume = {177},
 number = {2},
 year = {2002},
 issn = {0890-5401},
 pages = {122--159},
 doi = {http://dx.doi.org/10.1016/S0890-5401(02)93171-8},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 }

@techreport{linear-alias,
  title = {Linear types for aliased resources},
  author = {Chris Hawblitzel},
  year = {2005},
  institution = {Microsoft Research},
  number = {MSR-TR-2005-141}
}

@article{kobayashi-esop,
  title = {Type-Based Analysis of Deadlock fora Concurrent Calculus with Interrupts},
  author = {Kohei Suenaga and Naoki Kobayashi},
  year = {2007},
  booktitle = {ESOP}
}

@inproceedings{res-c,
    title = {A Path Sensitive Type System for Resource Usage Verification of C Like Languages},
    author = {Hyun-Goo Kang and Youil Kim and Taisook Han and Hwansoo Han},
    year = 2005,
    publisher = {Springer-Verlag},
    booktitle = {Programming Languages and Systems},
    pages = {264--280},
    series = {LNCS},
    volume = {3780}
}

@miscs{lsr,
    title = {Lightweight static resources: Sexy types for embedded and systems programming},
    author = {Oleg Kiselyov and Chung-Chieh Shan},
    year = 2007,
    note = {Draft}
}

@inproceedings{scoped-res,
    title = {Resource Usage Analysis Via Scoped Methods},
    author = {Gang Tan and Xinming Ou and David Walker},
    booktitle = {Foundations of Object-Oriented Languages},
    year = {2003}
}

@article{igarashi-res,
 author = {Igarashi, Atsushi and Kobayashi, Naoki},
 title = {Resource usage analysis},
 journal = {ACM Trans. Program. Lang. Syst.},
 volume = {27},
 issue = {2},
 month = {March},
 year = {2005},
 issn = {0164-0925},
 pages = {264--313},
 numpages = {50},
 url = {http://doi.acm.org/10.1145/1057387.1057390},
 doi = {http://doi.acm.org/10.1145/1057387.1057390},
 acmid = {1057390},
 publisher = acm,
 address = {New York, NY, USA},
 keywords = {Resource usage, type inference},
} 

@phdthesis{monitoring,
    title = {Policy Enforcement via Program Monitoring},
    author = {Jarred Adam Ligatti},
    year = 2006,
    month = {May}
}

@inproceedings{sec-policy,
    title = {A Type System for Expressive Security Policies},
    author = {David Walker},
    booktitle = {Twenty-Seventh acm {SIGPLAN} Symposium on Principles of Programming Languages},
    pages = {254--267},
    year = 2000}

@inproceedings{res-dfa,
    author = {K. Marriott and P.J. Stuckey and M. Sulzmann},
    title = {Resource Usage Verification},
    year = 2003,
    booktitle = {In  Proc. of First Asian Symposium, APLAS 2003},
    pages = {212--229},
    publisher = {Springer-Verlag}
}

@incollection{ hancock-interactive,
    author = "Peter Hancock and Anton Setzer",
    title = "Interactive Programs in Dependent Type Theory",
    booktitle = "Proc.\ of 14th Ann.\ Conf.\ of {EACSL}, {CSL}'00, Fischbau, Germany, 21--26 Aug 2000",
    volume = "1862",
    publisher = "Springer-Verlag",
    address = "Berlin",
    editor = "P. Clote and H. Schwichtenberg",
    pages = "317--331",
    year = "2000",
    url = "citeseer.ist.psu.edu/hancock00interactive.html" }

@inproceedings{popeea-resources,
 author = {Corneliu Popeea and Wei-Ngan Chin},
 title = {A type system for resource protocol verification and its correctness proof},
 booktitle = {PEPM '04: Proceedings of the 2004 acm {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
 year = {2004},
 isbn = {1-58113-835-0},
 pages = {135--146},
 location = {Verona, Italy},
 doi = {http://doi.acm.org/10.1145/1014007.1014021},
 publisher = {acm Press},
 address = {New York, NY, USA},
 }

@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-Verlag},
  series = {LNCS},
  booktitle = {Implementation and Application of Functional Languages 2006}
}

@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}},
    notnote = {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,
   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 = {2009},
   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}
}

@article{pe-problems,
 author = {Jones, N. D.},
 title = {Challenging problems in partial evaluation and mixed computation},
 journal = {New Gen. Comput.},
 volume = {6},
 number = {2-3},
 year = {1988},
 issn = {0288-3635},
 pages = {291--302},
 doi = {http://dx.doi.org/10.1007/BF03037143},
 publisher = {Ohmsha},
 address = {Tokyo, Japan, Japan},
 }

@inproceedings{tag-elim,
   title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},
   year = {2000},
   booktitle = {Subtyping and Dependent Types in Programming, APPSEM Workshop},
   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},
   series = {Lecture Notes in Computer Science},
   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,
   nothowpublished = {\url{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/+}
 }

@misc{gmail-outage,
    title = {Update on today's {Gmail} Outage},
    author = {{Official Gmail Blog}},
    howpublished = {\url{http://gmailblog.blogspot.com/2009/02/update-on-todays-gmail-outage.html}},
    note = {Retrieved 26th February 2009},
    year = 2009
}