@inproceedings{sheard-langfuture,
author = {Tim Sheard},
title = "Languages of the future",
booktitle = "ACM Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA'04)",
year = "2004"
}
@inproceedings{ivor,
author = {Edwin Brady},
title = {{Ivor}, a proof engine},
year = {2007},
publisher = {Springer},
series = {LNCS},
booktitle = {Implementation and Application of Functional Languages 2006},
note = {To appear}
}
@misc{coq-in-coq,
author = {Bruno Barras and Benjamin Werner},
year = 1997,
title = {{Coq} in {Coq}}
}
@article{hudak-edsl,
author = {Paul Hudak},
title = {Building Domain-Specific Embedded Languages},
year = {1996},
month = {December},
journal = {ACM Computing Surveys},
volume = {28A},
number = {4}
}
@inproceedings{concon,
author = {Conor McBride and Healfdene Goguen and James McKinna},
title = {Some Constructions On Constructors},
year = 2005,
booktitle = {TYPES 2004},
publisher = {Springer},
series = {LNCS},
volume = {3839}
}
@InProceedings{Hume-GPCE,
author = {K. Hammond and G.J. Michaelson},
title = {{Hume: a Domain-Specific Language for Real-Time Embedded Systems}},
booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'03)}},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
year = {2003},
}
@inproceedings{lcf-milner,
author = {Robin Milner},
title = {{LCF}: A Way of Doing Proofs with a Machine},
booktitle = {Mathematical Foundations of Computer Science 1978},
pages = {146-159},
year = 1979,
series = {LNCS},
volume = {64}
}
@inproceedings{epireloaded,
title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},
author = {James Chapman and Thorsten Altenkirch and Conor McBride},
year = 2006,
booktitle = {Trends in Functional Programming 2005},
note = {To appear}
}
@TECHREPORT{why-tool,
AUTHOR = {J.-C. Filli\^atre},
TITLE = {{Why: a multi-language multi-prover verification tool}},
INSTITUTION = {{LRI, Universit\'e Paris Sud}},
TYPE = {{Research Report}},
NUMBER = {1366},
MONTH = {March},
YEAR = 2003,
URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
}
@misc{ large-extraction,
author = "Lu\'iz Cruz-Filipe and Bas Spitters",
title = "Program Extraction from Large Proof Developments",
year = 2003,
url = "citeseer.ist.psu.edu/cruz-filipe03program.html" }
@inproceedings{ fta,
author = "Herman Geuvers and Freek Wiedijk and Jan Zwanenburg",
title = "A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals",
booktitle = "{TYPES 2000}",
pages = "96--111",
year = "2000",
url = "citeseer.ist.psu.edu/geuvers01constructive.html" }
@article{mckinna-expr,
title = {A type-correct, stack-safe, provably correct, expression compiler in {Epigram}},
author = {James McKinna and Joel Wright},
year = 2007,
journal = {Journal of Functional Programming},
note = {To appear}
}
@article{pugh-omega,
title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",
author = "William Pugh",
journal = "Communication of the ACM",
year = 1992,
pages = {102--114}
}
@misc{four-colour,
author = "Georges Gonthier",
title = "A computer-checked proof of the {Four Colour Theorem}",
year = 2005,
howpublished = {\url{http://research.microsoft.com/~gonthier/4colproof.pdf}}}
@inproceedings{sparkle,
author = "Maarten {de Mol} and Marko {van Eekelen} and Rinus Plasmeijer",
title = "Theorem Proving for Functional Programmers",
url = "citeseer.ist.psu.edu/654423.html",
BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2002)},
publisher = {Springer},
series = {LNCS},
volume = {2312},
year = 2002
}
@misc{agda,
title = {Agda},
author = {Catarina Coquand},
howpublished= {\url{http://agda.sourceforge.net/}},
year = 2005
}
@misc{cover,
title = {Cover Translator},
howpublished = {\url{http://coverproject.org/CoverTranslator/}}
}
@misc{parsec,
title = {Parsec, a fast combinator parser},
author = {Daan Leijen},
year = {2001},
howpublished = {\url{http://www.cs.uu.nl/~daan/parsec.html}}
}
@inproceedings{dtpmsp-gpce,
author = {Edwin Brady and Kevin Hammond},
title = {A Verified Staged Interpreter is a Verified Compiler},
booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'06)}},
year = 2006
}
@misc{haddock,
title = {Haddock: A {Haskell} Documentation Tool},
howpublished = {\url{http://www.haskell.org/haddock/}}
}
@inproceedings{offshoring,
title = {Implicitly Heterogeneous Multi-Stage Programming},
author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},
booktitle = {Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005)},
publisher = {Springer},
series = {LNCS},
volume = {3676},
year = 2005
}
@misc{alti-partial,
title = {Stop thinking about bottoms when writing programs},
author = {Thorsten Altenkirch},
year = 2006,
note = {Talk at BCTCS 2006}
}
@misc{tarmo-partial,
title = {Partiality is an Effect},
author = {Tarmo Uustalu},
year = 2004,
note = {Talk at Dagstuhl workshop on Dependently Typed Progamming}
}
@inproceedings{McKinnaPOPL06,
author = {James McKinna},
title = {Why dependent types matter},
booktitle = {Proc. ACM Symp. on Principles of Programming Languages (POPL 2006)},
year = {2006},
issn = {0362-1340},
pages = {1--1},
doi = {http://doi.acm.org/10.1145/1111320.1111038},
}
@inproceedings{leroy-compiler,
title = {Formal Certification of a Compiler Back-end},
author = {Xavier Leroy},
year = 2006,
booktitle = {Principles of Programming Languages 2006},
pages = {42--54},
publisher = {ACM Press}
}
@inproceedings{hutton-exceptions,
title = {Compiling Exceptions Correctly},
year = 2004,
author = {Graham Hutton and Joel Wright},
booktitle = {Mathematics of Program Construction},
publisher = {Springer},
series = {LNCS},
volume = {3125}
}
@inproceedings{tagless-staged,
title = {Tagless Staged Interpreters for Typed Languages},
year = {2002},
booktitle = {Proc. 2002 International Conf. on Functional Programming (ICFP 2002)},
author = {Emir Pa\v{s}al\'{i}c and Walid Taha and Tim Sheard},
publisher = {ACM}
}
@inproceedings{env-classifiers,
title = {Environment Classifiers},
year = 2003,
author = {Walid Taha},
booktitle = {Proc. ACM Symp. on Principles of Programming Languages (POPL 2003)},
pages = {26--37},
}
@inproceedings{dsl-msp,
title = {{DSL} Implementation in {MetaOCaml}, {Template Haskell}, {and C++}},
booktitle = {Domain Specific Program Genearation 2004},
author = {Krzysztof Czarnecki and John O'Donnell and J\"{o}rg Striegnitz and Walid Taha},
publisher = {Springer},
series = {LNCS},
volume = {3016},
year = 2004
}
@misc{ gadt-extk,
author = {Tim Sheard and James Hook and Nathan Linger},
title = {{GADTs} + Extensible Kinds = Dependent Programming},
year = 2005,
misc = {Submitted to ICFP '05}
}
@INPROCEEDINGS{dt-framework,
TITLE = {A Dependently Typed Framework for Static Analysis of Program Execution Costs},
YEAR = {2006},
BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
AUTHOR = {Edwin Brady and Kevin Hammond},
VOLUME = {4015},
SERIES = {LNCS},
PAGES = {74--90},
PUBLISHER = {Springer}
}
@INPROCEEDINGS{step-counting,
TITLE = {Accurate Step Counting},
YEAR = {2006},
BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
AUTHOR = {Catherine Hope and Graham Hutton},
PUBLISHER = {Springer}
}
@misc{multi-taha,
author = {Walid Taha},
title = {A Gentle Introduction to Multi-stage Programming},
year = {2003},
note = {Available from \url{http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf}}
}
@misc{mckinnabrady-phase,
title = {Phase Distinctions in the Compilation of {Epigram}},
year = 2005,
author = {James McKinna and Edwin Brady},
note = {Draft}
}
@phdthesis{ brady-thesis,
author = {Edwin Brady},
title = {Practical Implementation of a Dependently Typed Functional Programming Language},
year = 2005,
school = {University of Durham}
}
@phdthesis{ taha-thesis,
author = {Walid Taha},
title = {Multi-stage Programming: Its Theory and Applications},
year = 1999,
school = {Oregon Graduate Inst. of Science and Technology}
}
@phdthesis{ pasalic-thesis,
author = {Emir Pa\v{s}al\'{i}c},
title = {The Role of Type-Equality in Meta-programming},
year = 2004,
school = {OGI School of Science and Engineering}
}
@misc{ydtm,
author = {Thorsten Altenkirch and Conor McBride and James McKinna},
title = {Why Dependent Types Matter},
note = {Draft},
year = 2005}
@inproceedings { wadler-listless,
author = {Philip Wadler},
title = {Listlessness is better than laziness: {Lazy} evaluation and garbage collection at compile-time},
booktitle = {Proceedings of the 1984 ACM Symposium on LISP and functional programming},
year = 1984,
pages = {45--52}
}
@techreport { gofer-impl,
author = {Mark P. Jones},
title = {The implementation of the Gofer functional programming system},
month = {May},
year = {1994},
number = {YALEU/DCS/RR-1030},
institution = {Yale University}
}
@techreport { pm-opt1,
author = {Kevin Scott and Norman Ramsey},
title = {When do match-compilation heuristics matter?},
month = {May},
year = {2000},
number = {CS-2000-13},
institution = {Department of Computer Science, University of Virginia}
}
@inproceedings{ pm-opt2,
author = "Fabrice Le Fessant and Luc Maranget",
title = "Optimizing Pattern Matching",
booktitle = "International Conference on Functional Programming",
pages = "26-37",
year = "2001",
url = "citeseer.ist.psu.edu/lefessant01optimizing.html" }
@incollection{con-engine,
author = {G\'{e}rard Huet},
title = {The constructive engine},
booktitle = {A Perspective in Theoreticak Computer Science},
publisher = {World Scientific Publishing},
year = {1989},
editor = {R. Narasimhan},
note = {Commemorative Volume for Gift Siromoney},
pages = {38--69}
}
@inproceedings{gadts,
title = {Simple unification-based type inference for {GADTs}},
author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
year = {2006},
booktitle = {Proc. 2006 International Conf. on Functional Programming (ICFP 2006)}
}
@misc{wobbly,
author = {Simon {Peyton Jones} and Geoffrey Washburn and Stephanie Weirich},
title = {Wobbly types: type inference for generalised algebraic data types},
year = {2004},
note = {Submitted to POPL 2005}
}
@misc{epigram-afp,
author = {Conor McBride},
title = {Epigram: Practical Programming with Dependent Types},
year = {2004},
howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
}
@book{ml85,
author = {Per Martin-L\"{o}f},
title = "Intuitionistic Type Theory",
year = "1985",
publisher = "Bibliopolis"
}
@article{modular-fulllazy,
title = {A Modular Fully Lazy Lambda Lifter in {Haskell}},
author = {Simon {Peyton Jones} and David Lester},
year = {1991},
month = {May},
journal = {Software Practice and Experience},
volume = {21},
number = {5},
pages = {479--506}
}
@article{ghani-jay95,
author = {Barry Jay and Neil Ghani},
title = {The Virtues of Eta-Expansion},
journal = {Journal of Functional Programming},
year = {1995},
volume = {5},
number = {2},
pages = {135-154},
}
@misc{nkpat,
author = {Lennart Augustsson},
title = {n+k patterns},
year = {1993},
howpublished = {Message to the haskell mailing list, Mon, 17 May 93}
}
@article{ danvy98functional,
author = "Olivier Danvy",
title = "Functional Unparsing",
journal = "Journal of Functional Programming",
volume = "8",
number = "6",
pages = "621-625",
year = "1998",
url = "citeseer.ist.psu.edu/danvy98functional.html" }
@inproceedings{SeveriPoll94,
author = {Paula Severi and Erik Poll},
booktitle = {Logical Foundations of Computing Science, LFCS'94},
editor = {A. Nerode and Yu. V. Matiyasevich},
number = {813},
pages = {316--328},
publisher = {Springer},
series = {LNCS},
title = {{P}ure {T}ype {S}ystems with {D}efinitions},
year = {1994}
}
@inproceedings{coinductive,
title = {An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol},
booktitle = {Proceedings of the 1995 Workshop on Types for Proofs and Programs},
series = {LNCS},
year = {1995},
volume = {1158},
pages = {135-152},
publisher = {Springer-Verlag},
author = {Eduardo Gim\'{e}nez}
}
@book{erlang,
author = "Joe Armstrong and Robert Virding and Claes Wikstr{\"o}m and Mike Williams",
title = "Concurrent Programming in Erlang",
edition = "Second",
publisher = "Prentice-Hall",
year = "1996",
url = "citeseer.ist.psu.edu/armstrong93concurrent.html"
}
@PhdThesis{alti:phd93,
author = "Thorsten Altenkirch",
title = "Constructions, Inductive Types and Strong Normalization",
school = "University of Edinburgh",
year = "1993",
month = "November",
}
@inproceedings{coq-modules,
author = "Jacek Chrzaszcz",
title = "Modules in {Coq} Are and Will Be Correct",
year = {2004},
booktitle = {Types for Proofs and Programs 2003},
editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
publisher = {Springer},
volume = {3085}
}
@inproceedings{comp-polymorphism,
author = "Robert Harper and Greg Morrisett",
title = "Compiling Polymorphism Using Intensional Type Analysis",
year = "1995",
booktitle = "Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages",
pages = "130 -- 141"
}
@misc{runtime-loader,
author = "Andre Pang",
title = "{GHC} Runtime Loading",
year = "2004",
howpublished = {Available from \verb+http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading+}
}
@article{mccarthy-lisp,
author = "John McCarthy",
title = "Recursive Functions of Symbolic Expressions and Their Computation By Machine",
year = "1960",
journal = "Communications of the ACM",
volume = "3",
number = "4",
pages = "184--195"
}
@book{stl,
author = " David R. Musser and Atul Saini and Gillmer J. Derge",
title= "The {STL} Tutorial and Reference Guide: {C++} Programming with the Standard Template Library",
year = "2001",
publisher = "Addison Wesley"
}
@misc{ phase-distinction,
author = "Luca Cardelli",
title = "Phase Distinctions in Type Theory",
howpublished = "Manuscript",
year = "1988",
url = "citeseer.ist.psu.edu/cardelli88phase.html" }
@book {pierce-types,
author = "Benjamin C. Pierce",
title = "Type and Programming Languages",
year = "2002",
publisher = "MIT Press"
}
@article{ coqcc,
Author = "Thierry Coquand and G\'{e}rard Huet",
title = "The calculus of constructions",
year = "1988",
journal = "Information and Computation",
volume = "76",
pages = "95--120"
}
@article{ miller91jlc,
Author = "Dale Miller",
Title = "A Logic Programming Language with Lambda-Abstraction,
Function Variables, and Simple Unification",
Journal = "Journal of Logic and Computation",
Volume = "1",
Number = "4",
Pages = "497-536",
Year = "1991",
URL = "citeseer.ist.psu.edu/miller91logic.html",
URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" }
@article{miller-unity,
author = "Dale Miller",
title = "Unification Under a Mixed Prefix",
journal = "Journal of Symbolic Computation",
volume = "14",
pages = "321--358",
year = 1992
}
@inproceedings{ cynthia,
author = "Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe",
title = "An {ML} Editor Based on Proofs-As-Programs",
booktitle = "Automated Software Engineering",
pages = "166-173",
year = "1999",
url = "citeseer.ist.psu.edu/whittle99ml.html" }
@misc{ewd340,
title={The Humble Programmer},
author={Edsger Dijkstra},
year={1972},
note={Turing Award Lecture, EWD 340}
}
@misc{fortran,
title={Specifications for the {IBM} Mathematical FORmula TRANslating System, {FORTRAN}},
author={{IBM Applied Science Division}},
key={IBM},
year={1954},
month={November}
}
@inproceedings{quickcheck,
title = {{QuickCheck}: A Lightweight Tool For Random Testing Of {Haskell} Programs},
author = {Koen Claessen and John Hughes},
year = {2000},
booktitle = {International Conference on Functional Programming}
}
@inproceedings{currylam,
title = {Functionality in Combinatory Logic},
author = {Haskell Curry},
year = {1934},
booktitle = {Proc. Nat. Acad. Sci, USA},
volume = {20},
pages = {584--590}
}
@article{churchsimplelam1,
title = {A set of postulates for the foundation of logic},
author = {Alonzo Church},
year = {1932},
journal = {Annals of Mathematics},
volume = {2},
number = {33},
pages = {346--366}
}
@article{churchsimplelam2,
title = {A set of postulates for the foundation of logic},
author = {Alonzo Church},
year = {1933},
journal = {Annals of Mathematics},
volume = {2},
number = {34},
pages = {839--864}
}
@article{churchlam,
title = {A Formulation of the Simple Theory of Types},
author = {Alonzo Church},
year = {1940},
journal = {Journal of Symbolic Logic},
volume = {5},
pages = {56--58}
}
@book{mitchell,
title = {Concepts in Programming Languages},
author = {John C. Mitchell},
year = {2003},
publisher = {Cambridge University Press}
}
@inproceedings{harrison-hol99,
title = {A Machine-Checked Theory of Floating Point Arithmetic},
year = {1999},
booktitle = {Theorem Proving in Higher Order Logics: 12th International Conference, TP},
pages = {113--130},
author = {John Harrison},
crossref = {hol99}
}
@inproceedings{c--,
title = {C--: A portable assembly language},
year = {1997},
booktitle = {Workshop on Implementing Functional Languages, St Andrews},
author = {Simon {Peyton Jones} and Thomas Nordin and Dino Oliva},
crossref = {func-imp97}
}
@proceedings{func-imp97,
title = {Workshop on Implementing Functional Languages, St Andrews},
year = {1997},
editor = {C Clack},
publisher = {Springer-Verlag}
}
@proceedings{hol99,
volume = {1690},
title = {Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99},
year = {1999},
editor = {Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and Christine Paul},
publisher = {Springer-Verlag},
address = {Nice, France},
series = {LNCS}
}
@book{mathlogic,
title = {Mathematical Logic and Programming Languages},
year = {1985},
editor = {C.A.R. Hoare and J.C. Shepherdson},
publisher = {Prentice-Hall}
}
@book{automath,
title = {Selected Papers on Automath},
year = {1994},
editor = {S. Abramsky and J. Barwise and K. Fine and H.J. Keisler and A.S. Troelstr},
publisher = {North-Holland}
}
@misc{gimps,
howpublished = {http://www.mersenne.org/prime.htm},
title = {Great Internet Mersenne Prime Search}
}
@misc{haskell-report,
title = {Haskell 98 Language and Libraries --- The Revised Report},
year = {2002},
month = {December},
author = {Simon {Peyton Jones} and others},
howpublished = {Available from \verb+http://www.haskell.org/+}
}
@inproceedings{cayenne-icfp,
author = "Lennart Augustsson",
title = "Cayenne - a Language with Dependent Types",
booktitle = "Proc. 1998 International Conf. on Functional Programming (ICFP '98)",
pages = "239--250",
year = "1998",
url = "citeseer.nj.nec.com/augustsson98cayenne.html"
}
@misc{equality-cayenne,
howpublished = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
title = {Equality Proofs in Cayenne},
year = {1999},
author = {Lennart Augustsson}
}
@misc{interp-cayenne,
howpublished = {\url{http://www.cs.chalmers.se/~augustss/cayenne/}},
title = {An exercise in dependent types: A well-typed interpreter},
year = {1999},
author = {Lennart Augustsson and Magnus Carlsson}
}
@inproceedings{balaa00fixpoint,
title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
year = {2000},
booktitle = {Theorem Proving in Higher Order Logics},
pages = {1-16},
author = {Antonia Balaa and Yves Bertot}
}
@inproceedings{isabelle-maple,
title = {Theorems and algorithms: An interface between Isabelle and Maple},
year = {1995},
booktitle = {International Symposium on Symbolic and Algebraic Computation},
author = {Ballarin, C. and Homann, K., and Calmet, J.}
}
@book{barendregt-num,
title = {The Lambda Calculus, Its Syntax and Semantics},
year = {1984},
publisher = {North-Holland},
author = {Henk Barendregt}
}
@book{beiler,
title = {Recreations in the Theory of Numbers},
year = {1964},
publisher = {Dover},
author = {Albert H. Beiler}
}
@article{multidigit,
journal = {Advances in Applied Mathematics},
title = {Multidigit Multiplication for Mathematicians},
year = {1998},
author = {Daniel J. Bernstein}
}
@article{buhler-fox,
journal = {ACM Crossroads 2.1.},
month = {September},
title = {The Fox project: A language-structured approach to networking software.},
year = {1995},
author = {Buhler, J.},
note = {Available at http://www.acm.org/crossroads/xrds2-1/foxnet.html}
}
@techreport{burstall91,
title = {Computer Assisted Proof for Mathematics: an Introduction Using the \textsc{Lego} Proof System},
year = {1991},
institution = {University of Edinburgh},
author = {Rod Burstall}
}
@article{plastic,
title = {An Implementation of {LF} with Coercive Subtyping and Universes},
author = {Paul Callaghan and Zhaohui Luo},
journal = {Journal of Automated Reasoning},
volume = {27},
number = {1},
pages = {3--27},
year = {2001}
}
@article{coercive,
title = {Coercive subtyping},
author = {Zhaohui Luo},
journal = {J. Logic Comput.},
volume = {9},
number = {1},
year = {1991},
pages = {105--130}
}
@inproceedings{calmet-homann,
title = {Classification of communication and cooperation mechanisms for logical and symbolic computation systems},
year = {1996},
booktitle = {Proceedings of the First International Workshop 'Frontiers of Combining S},
pages = {133-146},
publisher = {Kluwer},
author = {J. Calmet and K. Homann}
}
@techreport{comm-proofs,
title = {On Communicating Proofs in Interactive Mathematical Documents},
year = {2000},
institution = {Eindhoven University of Technology},
author = {Olga Caprotti and Martijn Oostdijk}
}
@article{prime2999,
title = {How to formally and efficiently prove Prime(2999)},
year = {2001},
author = {Olga Caprotti and Martijn Oostdijk},
journal = {Symbolic Computation and Automated Reasoning},
pages = {114--125}
}
@book{church-num,
title = {The Calculi of Lambda-Conversion},
year = {1941},
publisher = {Princeton University Press},
author = {Alonzo Church}
}
@book{nuprl86,
title = {Implementing Mathematics with the NuPrl Proof Development System},
year = {1986},
publisher = {Prentice-Hall},
address = {NJ},
author = {Constable, Robert L. and others}
}
@book{conway,
title = {On Numbers and Games},
year = {1976},
publisher = {Academic Press},
author = {J.H. Conway}
}
@misc{coq-manual,
howpublished = {\verb+http://coq.inria.fr/+},
title = {The {Coq} Proof Assistant --- Reference Manual},
year = {2001},
author = {{Coq Development Team}}
}
@misc{tt-prog,
month = {June},
title = {Type Theory and Programming},
year = {1994},
author = {Thierry Coquand and Bengt Nordstr\"{o}m and Jan M. Smith and Bj\"{o}rn von Sydow}
}
@book{func-appr,
title = {The Functional Approach to Programming},
year = {1998},
publisher = {Cambridge University Press},
author = {Guy Cousineau and Michel Mauny}
}
@misc{ibmspec,
howpublished = {http://www2.hursley.ibm.com/decimal/},
month = {January},
title = {Standard Decimal Arithmetic Specification},
year = {2001},
author = {Mike Cowlishaw},
note = {\copyright IBM Corporation 2001}
}
@book{dummett,
title = {Elements of Intuitionism},
year = {2000},
edition = {2nd},
publisher = {Oxford: Clarendon},
author = {Michael A.E. Dummet}
}
@article{dybjer94,
title = {Inductive Families},
year = {1994},
author = {Peter Dybjer},
journal = {Formal Aspects Of Computing},
volume = {6},
pages = {440--465}
}
@misc{octave,
howpublished = {http://www.octave.org/},
month = {February},
title = {GNU Octave -- A high-level interactive language for numerical computations},
year = {1997},
author = {John W. Eaton}
}
@book{comp-methods,
title = {Computing methods for scientists and engineers},
year = {1968},
publisher = {Oxford : Clarendon Press},
author = {L. Fox and D.F. Mayers}
}
@misc{guile,
howpublished = {http://www.gnu.org/software/guile/guile.html},
title = {Guile -- Project GNU's extension language},
year = {2001},
author = {{Free Software Foundation}}
}
@article{need-dep,
journal = {Journal of Functional Programming},
number = {4},
volume = {10},
title = {Do we need dependent types?},
year = {2000},
pages = {409-415},
author = {Daniel Fridlender and Mia Indrika}
}
@book{primes-programming,
title = {Primes and Programming -- An Introduction to Number Theory with Computing},
year = {1993},
publisher = {Cambridge University Press},
author = {Peter Giblin}
}
@misc{rec-coq,
month = {May},
title = {A Tutorial on Recursive Types in \textsc{Coq}},
year = {1998},
author = {Eduardo Gim\'{e}nez}
}
@article{goldberg91,
journal = {ACM Computing Surveys},
number = {1},
volume = {23},
title = {What every computer scientist should know about floating point arithmetic},
year = {1991},
pages = {5-48},
author = {D. Goldberg}
}
@article{binary-lambda,
journal = {Journal of Functional Programming},
number = {6},
volume = {10},
title = {An adequate and efficient left associated binary numeral system in the $\lambda$-calculus},
year = {2000},
author = {Mayer Goldberg}
}
@book{hol,
title = {Introduction to HOL},
year = {1993},
publisher = {Cambridge University Press},
author = {M. Gordon and T. Melham}
}
@misc{gmp,
howpublished = {Available from \verb+http://www.swox.com/gmp/manual/+},
title = {The {GNU Multiple Precision} Arithmetic Library 4.1.3 --- Manual},
year = {2004},
author = {Torbj\"{o}rn Granlund and others}
}
@article{harrison-fmsd94,
journal = {Formal Methods in System Design},
volume = {5},
title = {Constructing the Real Numbers in {HOL}},
year = {1994},
pages = {35--59},
author = {John Harrison}
}
@book{harrison-thesis,
title = {Theorem Proving with the Real Numbers},
year = {1998},
publisher = {Springer-Verlag},
author = {John Harrison}
}
@techreport{hol-maple,
title = {Reasing about the Reals: the marriage of HOL and Maple},
year = {1993},
institution = {University of Cambridge Computer Laboratory},
author = {John Harrison and Laurent Th\'{e}ry}
}
@misc{coq-tutorial,
howpublished = {http://pauillac.inria.fr/coq},
title = {The \textsc{Coq} Proof Assistant - A Tutorial},
author = {G\'{e}rard Huet and Gilles Kahn and Christine Paulin-Mohring}
}
@misc{restr-haskell,
howpublished = {http://citeseer.nj.nec.com/253599.html},
month = {September},
title = {Restricted Data Types in Haskell},
year = {1999},
author = {John Hughes}
}
@misc{javadec,
howpublished = {http://www2.hursley.ibm.com/decimalj/decimald.html},
month = {September},
title = {Decimal Arithmetic for Java -- a Proposal},
year = {2000},
author = {{IBM Corporation}}
}
@misc{ieee754,
title = {IEEE Standard for Binary Floating Point Arithmetic},
year = {1985},
author = {{IEEE Standard 754}}
}
@misc{ieee854,
title = {IEEE Standard for Radix-Independent Floating-Point Arithmetic},
year = {1987},
author = {{IEEE Standard 854}}
}
@inproceedings{jon91,
title = {Completing the Rational and Metric Spaces in \textsc{Lego}},
year = {1991},
booktitle = {Proceedings of the Second Workshop on Logical Frameworks},
author = {Claire Jones}
}
@misc{ typinghaskell,
author = "Mark Jones",
title = "Typing {Haskell} in {Haskell}",
howpublished = "In Haskell Workshop, September 1999.",
year = "1999",
url = "citeseer.ist.psu.edu/article/jones99typing.html" }
@article{karatsuba,
journal = {Soviet Physics-Doklady},
volume = {7},
title = {Multiplication of multidigit numbers by automata},
year = {1963},
pages = {595--596},
author = {A. Karatsuba and Y. Ofman}
}
@book{knuth2,
volume = {2},
title = {The Art of Computer Programming - Seminumerical Algorithms},
year = {1969},
publisher = {Addison Wesley},
author = {Donald E. Knuth}
}
@article{next700,
journal = {Communications of the ACM},
number = {3},
month = {March},
volume = {9},
title = {The next 700 programming languages},
year = {1966},
author = {P.J. Landin}
}
@techreport{luo-spec,
month = {January},
title = {Program Specification and Data Refinement in Type Theory},
year = {1993},
institution = {Department of Computer Science, University of Edinburgh},
author = {Zhaohui Luo}
}
@phdthesis{luo90,
school = {University of Edinburgh},
title = {An Extended Calculus Of Constructions},
year = {1990},
author = {Zhaohui Luo}
}
@techreport{lego-manual,
title = {\textsc{Lego} Proof Development System: User's Manual},
year = {1992},
institution = {Department of Computer Science, University of Edinburgh},
author = {Zhaohui Luo and Robert Pollack}
}
@inproceedings{alf,
title = {The {ALF} proof editor and its proof engine},
year = {1994},
booktitle = {Formal Proceeding of the 1993 Workshop on Types for Proofs and Programs},
author = {Lena Magnusson and Bengt N\"{o}rdstrom}
}
@misc{happy,
howpublished = {http://www.haskell.org/happy/},
title = {Happy User Guide},
year = {2001},
author = {Simon Marlow and Andy Gill}
}
@inproceedings{generic-haskell,
title = {Generic Haskell, Specifically},
author = {Dave Clarke and Andres L\"{o}h},
editor = {Jeremy Gibbons and Johan Jeuring},
booktitle = {Proceedings of the IFIP TC2 Working Conference on Generic Programming},
year = {2002},
publisher = {Kluwer Academic Publishers},
pages = {21--48}
}
@article{faking-it,
title = {Faking It -- Simulating Dependent Types in {Haskell}},
year = {2002},
author = {Conor McBride},
journal = {Journal of Functional Programming},
volume = {12},
number = {4+5},
pages = {375--392}
}
@misc{mcbride-inverting,
title = {Inverting Inductively Defined Relations in \textsc{Lego}},
year = {1996},
author = {Conor McBride}
}
@phdthesis{mcbride-thesis,
month = {May},
school = {University of Edinburgh},
title = {Dependently Typed Functional Programs and their proofs},
year = {2000},
author = {Conor McBride}
}
@article{mcbride-unification,
title = {First-Order Unification by Structural Recursion},
year = {2003},
author = {Conor McBride},
journal = {Journal of Functional Programming},
volume = {13},
number = {6},
pages = {1061--1075}
}
@misc{mckinna-pollack,
howpublished = {Kluwer Academic Publishers},
title = {Some Lambda Calculus and Type Theory formalized},
year = {1998},
author = {James McKinna and Robert Pollack}
}
@book{num-theory,
title = {An Introduction to the Theory of Numbers},
year = {1980},
publisher = {John Wiley and Sons},
author = {Ivan Niven and Herbert S. Zuckerman}
}
@book{prog-mltt,
title = {Programming in Martin-L\"{o}f's Type Theory -- An Introduction},
year = {1990},
publisher = {Oxford University Press},
author = {Bengt Nordstr\"{o}m and Kent Petersson and Jan M. Smith},
note = {Out of print. Available from http://www.cs.chalmers.se/Cs/Research/Logic}
}
@book{okasaki,
title = {Purely Functional Data Structures},
year = {1998},
publisher = {Cambridge University Press},
author = {Chris Okasaki}
}
@book{arith-systems,
title = {Computer Arithmetic Systems},
year = {1994},
publisher = {Prentice-Hall},
author = {Amos R. Omondi}
}
@book{pj-imp,
title = {The Implementation of Functional Programming Languages},
year = {1987},
publisher = {Prentice-Hall},
author = {Simon {Peyton Jones}}
}
@book{cp-bjc,
title = {Computational Numerical Methods},
year = {1986},
publisher = {John Wiley and Sons},
author = {C. Phillips and B. Cornelius}
}
@book{nag,
title = {The NAG Library: a beginner's guide},
year = {1986},
publisher = {Oxford : Clarendon Press},
author = {Jen Phillips}
}
@misc{believe,
month = {September},
title = {How to Believe a Machine-Checked Proof},
year = {1996},
author = {Robert Pollack}
}
@phdthesis{pollack94,
school = {University of Edinburgh},
title = {The Theory of LEGO -- A Proof Checker for the Extended Calculus of Constructions},
year = {1994},
author = {Robert Pollack}
}
@inproceedings{intel-bug,
series = {LNCS},
volume = {915},
title = {Anatomy of the Pentium Bug},
publisher = {Springer-Verlag},
year = {1995},
pages = {97--107},
author = {V.R. Pratt}
}
@book{maple,
title = {The Maple Handbook: Maple V Release 4},
year = {1996},
publisher = {Springer},
author = {Darren Redfern}
}
@book{crypto,
title = {Applied Cryptography: protocols, algorithms and source code in C.},
year = {1996},
publisher = {Wiley},
author = {Bruce Schneier}
}
@article{adts,
journal = {Mathematical Structures in Computer Science},
number = {2},
volume = {10},
title = {On lists and other abstract data types in the calculus of construction},
year = {2000},
pages = {261-276},
author = {Jonathan P. Seldin}
}
@article{seldin97,
journal = {Annals of Pure and Applied Logic},
number = {1},
month = {January},
volume = {83},
title = {On the proof theory of Coquand's calculus of constructions},
year = {1997},
pages = {23--101},
author = {Jonathan P. Seldin}
}
@article{wichmann,
journal = {The Computer Journal},
volume = {32},
title = {Towards a Formal Specification of Floating Point},
year = {1989},
pages = {432-436},
author = {B.A. Wichmann}
}
@book{mathematica,
title = {Mathematica : a system for doing mathematics by computer},
year = {1991},
publisher = {Addison Wesley},
author = {Stephen Wolfram}
}
@inproceedings{xi-imp,
author = "Hongwei Xi",
title = {{Imperative Programming with Dependent Types}},
booktitle = "Proceedings of 15th IEEE Symposium on Logic in Computer Science",
year = 2000,
month = "June",
address = "Santa Barbara",
pages = "375--387"
}
@phdthesis{xi-thesis,
month = {December},
school = {Department of Mathematical Sciences, Carnegie Mellon University},
title = {Dependent Types in Practical Programming},
year = {1998},
author = {Hongwei Xi}
}
@techreport{dtal,
author = {Hongwei Xi and Robert Harper},
title = {A Dependently Typed Assembly Language},
institution = {Computer Science and Engineering Department, Oregon Graduate Institute},
year = 1999,
number = {OGI-CSE-99-008},
month = {July},
}
@misc{bignum-cmp,
month = {February},
title = {Comparison of three public-domain multiprecision libraries: BigNum, Gmp and Pari},
year = {1998},
author = {Paul Zimmerman}
}
@book{perl,
title = {Programming Perl},
author = {Larry Wall and Tom Christiansen and Jon Orwant},
year = {2000},
edition = {3rd},
publisher = {O'Reilly}
}
@misc{python,
howpublished = {http://www.python.org/doc/current/tut/tut.html},
month = {April},
title = {Python Tutorial},
year = {2001},
author = {Guido van {Rossum} and Fred L. {Drake, Jr}}
}
@book{logic,
title = {The Language of First Order Logic},
year = {1992},
publisher = {CSLI Lecture Notes},
author = {Jon Barwise and John Etchemendy}
}
@book{haskell,
title = {Haskell -- The Craft of Functional Programming},
year = {1999},
publisher = {Addison Wesley},
author = {Simon Thompson}
}
@inproceedings{coq-hol,
title = {A Comparative Study of Coq and HOL},
year = {1997},
booktitle = {Theorem Proving in Higher Order Logics},
pages = {323-337},
author = {Vincent Zammit}
}
@misc{gay90,
month = {November},
title = {Correctly Rounded Binary-Decimal and Decimal-Binary Conversions},
year = {1990},
author = {David M. Gay},
note = {AT&T Bell Laboratories, Numerical Analysis Manuscript 90-10}
}
@article{hughes-matters,
journal = {Computer Journal},
number = {2},
volume = {32},
title = {Why Functional Programming Matters},
year = {1989},
pages = {98--107},
author = {J. Hughes}
}
@inproceedings{proofpointing,
title = {Proof by Pointing},
year = {1994},
booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer So},
pages = {141--160},
editor = {M. Hagiya and J. C. Mitchell},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {789},
address = {Sendai, Japan},
author = {Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry}
}
@misc{inductive-coq,
month = {December},
title = {Inductive Definitions in the System Coq -- Rules and Properties},
year = {1992},
author = {Christine Paulin-Mohring}
}
@misc{leiserson98,
month = {July},
title = {Using de Bruijn Sequences to Index a 1 in a Computer Word},
year = {1998},
author = {{Charles E. Leiserson} and {Harald Prokop} and {Keith H. Randall}}
}
@inproceedings{proofchecking,
title = {A two-level approach towards lean proof-checking},
year = {1996},
booktitle = {TYPES},
pages = {16--35},
author = {G. Barthe and M.P.J. Ruys and H.P. Barendregt}
}
@inproceedings{congruence,
title = {Congruence Types},
year = {1995},
booktitle = {CSL},
pages = {36--51},
author = {Gilles Barthe and Herman Geuvers}
}
@phdthesis{geuvers-thesis,
title = {Logic and Type Systems},
author = {Herman Geuvers},
year = 1993,
school = {Katholieke Universiteit Nijmegen}
}
@techreport{multiple-values,
title = {Multiple Values in {Standard ML}},
year = {1994},
number = {94-312},
institution = {LFCS, Dept of Computer Science, University of Edinburgh},
author = {Kevin Mitchell}
}
@inproceedings{oracle-checking,
month = {January},
title = {Oracle-Based Checking of Untrusted Software},
year = {2001},
booktitle = {Proceedings of the 28th ACM Symposium on Principles of Programming Languages},
pages = {142--154},
author = {{George C. Necula} and {S.P. Rahul}}
}
@article{adams93jfp,
journal = {Journal of Functional Programming},
number = {4},
volume = {3},
title = {Efficient Sets -- A Balancing Act},
year = {1993},
pages = {553--561},
author = {Stephen Adams}
}
@inproceedings{hughes-sized,
title = {Proving the Correctness of Reactive Systems Using Sized Types},
year = {1996},
booktitle = {Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programmin},
pages = {410--423},
author = {John Hughes and Lars Pareto and Amr Sabry}
}
@inproceedings{whittle99ml,
title = {An {ML} Editor Based on Proofs-As-Programs},
year = {1999},
booktitle = {Automated Software Engineering},
pages = {166--173},
author = {Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe}
}
@book{efp-typeinf,
title = {Elements of Functional Programming},
year = {1989},
publisher = {Addison-Wesley},
author = {Chris Reade},
series = {International Computer Science Series}
}
@incollection{ wadler-views,
author = "Philip Wadler",
title = "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction",
booktitle = "Proceedings, 14th Symposium on Principles of Programming Languages",
publisher = "Association for Computing Machinery",
editor = "Steve Munchnik",
pages = "307--312",
year = "1987",
url = "citeseer.nj.nec.com/wadler87views.html" }
@article{ coquand-checking,
author = "Thierry Coquand",
title = "An Algorithm for Type-Checking Dependent Types",
journal = "Science of Computer Programming",
volume = "26",
number = "1-3",
pages = "167-177",
year = "1996",
url = "citeseer.nj.nec.com/coquand96algorithm.html" }
@misc{coquand-pm,
author = "Thierry Coquand",
title = "Pattern Matching with Dependent Types",
year = "1992",
howpublished = "Available from \verb+http://www.cs.chalmers.se/~coquand/type.html+"
}
@misc{pollack-records,
month = {August},
title = {Dependently Typed Records for Representing Mathematical Structure},
year = {2000},
author = {Robert Pollack}
}
@article{checking-betarte,
journal = {Journal of Functional Programming},
number = {2},
month = {March},
volume = {10},
title = {Type checking dependent (record) types and subtyping},
year = {2000},
pages = {137--166},
author = {Gustavo Betarte}
}
@article{ gcode,
author = "Thomas Johnsson",
title = "Efficient Compilation of Lazy Evaluation",
booktitle = "Proceedings of the {ACM} {SIGPLAN}'84 Symposium on Compiler Con struction",
journal = "SIGPLAN Notices",
volume = "19",
number = "6",
month = "June",
publisher = "ACM Press",
pages = "58--69",
year = "1984",
url = "citeseer.nj.nec.com/johnsson84efficient.html" }
@misc{kamareddine01,
month = {February},
title = {Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems},
year = {2001},
author = {Fairouz Kamareddine}
}
@book{prooftheory,
title = {Basic Proof Theory},
year = {1996},
publisher = {Cambridge University Press},
author = {A.S. Troelstra and H. Schwichtenberg},
series = {Cambridge Tracts in Theoretical Computer Science}
}
@misc{nbe_staged,
title = {Integrating Normalization-by-Evaluation into a Staged Programming Language},
year = {1998},
author = {Tim Sheard}
}
@inproceedings{nbe2,
title = {Normalization by evaluation},
year = {1998},
author = {Ulrich Berger and Matthias Eberl and Helmut Schwichtenberg},
booktitle = {Prospects for Hardware Foundations 1998},
pages = {117--137},
series = {LNCS}
}
@misc{rtcg_jfp,
title = {Compiling for Run-time Code Generation},
year = {2000},
author = {Frederick Smith and Dan Grossman and Greg Morrisett and Luke Hornof and Trevor J},
note = {Under consideration for J. Functional Programming}
}
@phdthesis{fredsmith_thesis,
month = {January},
school = {Cornell University},
title = {Certified Run-time Code Generation},
year = {2002},
author = {Frederick Smith}
}
@inproceedings{xi_arraybounds,
author = "Hongwei Xi and Frank Pfenning",
title = {Eliminating Array Bound Checking through Dependent Types},
booktitle = "Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation",
year = 1998,
month = "June",
address = "Montreal",
pages = "249--257",
}
@inproceedings{xi_deadcode,
author = "Hongwei Xi",
title = {Dead Code Elimination through Dependent Types},
booktitle = "The First International Workshop on Practical Aspects of Declarative Languages",
year = 1999,
month = "January",
address = "San Antonio",
pages = "228--242"
}
@book{compilers,
title = {Compilers --- Principles, Techniques and Tools},
year = {1986},
publisher = {Addison-Wesley},
author = {Alfred Aho and Ravi Sethi and Jeffrey Ullman}
}
@inproceedings{nhc,
title = {Highlights from nhc: A space efficient {Haskell} Compiler},
year = {1995},
author = "Niklas R{\"o}jemo",
booktitle = "Functional Programming Languages and Computer Architecture",
pages = "282--292"
}
@misc{mlmatch,
title = {SML/NJ Match Compiler Notes},
year = {1992},
author = {William Aitken}
}
@misc{mlmatch_sestoft,
title = {ML pattern match compilation and partial evaluation},
year = {1992},
author = {Peter Sestoft}
}
@inproceedings{compiledstrongreduction,
title = {A Compiled Implementation of Strong Reduction},
year = {2002},
author = {Benjamin Gr\'{e}goire and Xavier Leroy},
booktitle = {Proc. 2002 International Conf. on Functional Programming (ICFP 2002)},
pages = {235--246}
}
@misc{tclhaskell,
howpublished = {http://www.dcs.gla.ac.uk/~meurig/TclHaskell/usermanual.html},
month = {August},
title = {TclHaskell - User Manual},
year = {1999},
author = {Meurig Sage}
}
@InProceedings{nbe-cat,
author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
title = "Categorical reconstruction of a reduction free
normalization proof",
year = "1995",
booktitle = "Category Theory and Computer Science",
editor = {David Pitt and David E. Rydeheard and Peter Johnstone},
series = {LNCS},
volume = {953},
pages = {182-199}
}
@inproceedings{presburgerEFSM,
title = {A Comparison of Presburger Engines for EFSM Reachability},
year = {1998},
booktitle = {Computer Aided Verification '98},
pages = {280--292},
author = {Thomas R. Shiple and James H. Kukula and Rajeev K. Ranjan}
}
@misc{typesafecast,
title = {Type-Safe Cast},
year = {2000},
author = {Stephanie Weirich}
}
@phdthesis{grobauer-thesis,
school = {University of Aarhus},
title = {Topics in Semantics Based Program Manipulation},
year = {2001},
author = {Bernd Grobauer}
}
@misc{monads-moggi,
title = {Computational Lambda Calculus and Monads},
year = {1989},
author = {Eugenio Moggi}
}
@article{gmp-proof,
title = {A proof of {GMP} square root},
year = {2002},
journal = {Journal of Automated Reasoning},
volume = {29},
pages = {225--252},
author = {Yves Bertot and Nicolas Magaud and Paul Zimmerman}
}
@article{F-tal,
journal = {ACM Transactions on Programming Languages and Systems},
number = {3},
month = {May},
volume = {21},
title = {From {System F} to Typed Assembly Language},
year = {1999},
pages = {528--569},
author = {Greg Morrisett and David Walker and Karl Crary and Neal Glew}
}
@techreport{nbe-rtcg,
month = {December},
title = {Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation},
year = {1997},
institution = {BRICS},
author = {Vincent Balat and Oliver Danvy}
}
@misc{yong-schemata,
howpublished = {http://www.dur.ac.uk/yong.luo/},
title = {A Methodology for Implementing Inductive Schemata},
year = {2002},
author = {Yong Luo and Zhaohui Luo}
}
@inproceedings{harper93,
title = {Explicit Polymorphism and CPS Conversion},
year = {1993},
booktitle = {20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {206--219},
publisher = {ACM Press, New York, NY, USA},
author = {Robert Harper and Mark Lillibridge}
}
@techreport{backends,
month = {November},
title = {Functional Back-Ends within the Lambda-Sigma Calculus},
year = {1996},
institution = {INRIA},
author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
}
@article{stg,
title = {Implementing lazy functional languages on stock hardware -- the {Spineless Tagless G-machine}},
year = {1992},
journal = {Journal of Functional Programming},
volume = {2},
number = {2},
pages = {127--202},
month = {April},
author = {Simon {Peyton Jones}}
}
@article{debruijn,
journal = {Indagationes Mathematicae},
volume = {34},
title = {Lambda calculus notation with nameless dummies},
year = {1972},
pages = {381--392},
author = {N.G. de Bruijn}
}
@book{assembly,
month = {January},
title = {PC Assembly Language},
year = {2002},
publisher = {http://www.drpaulcarter.com/},
author = {Paul A. Carter}
}
@inproceedings{poly99,
title = {Once Upon A Polymorphic Type},
year = {1999},
booktitle = {26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
publisher = {ACM},
author = {Keith Wansbrough and Simon {Peyton Jones}}
}
@misc{lazy_intro,
title = {Compiling Lazy Functional Languages: An introduction},
year = {1986},
author = {Thomas Johnsson}
}
@inproceedings{unboxed-fp,
month = {Sept},
title = {Unboxed Values as First Class Citizens in a Non-Strict Functional Language},
year = {1991},
author = {Simon {Peyton Jones} and John Launchbury},
booktitle = {Functional Programming Languages and Computer Architecture (FPCA'91)},
crossref = {fplca91},
pages = {636--666}
}
@inproceedings{abc-machine,
author = {Sjaak Smetsers and Eric N{\"{o}}cker and John {van Groningen} and Rinus Plasmeijer},
title = {Generating efficient code for lazy functional languages},
booktitle = {Functional programming Languages and Computer Architecture},
year = {1991},
pages = {592--617},
crossref = {fplca91}
}
@proceedings{fplca91,
title = {Functional programming Languages and Computer Architecture},
year = {1991},
volume = {523},
series = {LNCS},
publisher = {Springer-Verlag},
editor = {John Hughes}
}
@inproceedings{nbe,
title = {An inverse of the evaluation functional for typed $\lambda$-calculus},
year = {1991},
booktitle = {Proc. 1991 IEEE Symp. on Logic in Comp. Sci.},
pages = {203--211},
editor = {R. Vemuri},
author = {Ulrich Berger and Helmut Schwichtenberg}
}
@inproceedings{typed-closure,
title = {Typed Closure Conversion},
year = {1996},
booktitle = {Symposium on Principles of Programming Languages},
pages = {271--283},
author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper}
}
@misc{ghc-commentary,
howpublished = {http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/},
title = {The Glasgow Haskell Compiler (GHC) Commentary},
year = {2002},
author = {Manuel M. T. Chakravarty and Sigbjorn Finne and Simon Marlow and Simon {Peyton Jones} and Julian Seward and Reuben Thomas},
note = {Available from GHC CVS repository}
}
@inproceedings{lambdalift,
month = {September},
title = {Lambda Lifting: Transforming Programs to Recursive Equations},
year = {1985},
booktitle = {Functional Programming Languages and Computer Architecture},
pages = {190--203},
editor = {Jean-Pierre Jouannaud},
publisher = {Springer-Verlag},
author = {Thomas Johnsson}
}
@inproceedings{til,
title = {TIL: A Type-Directed Optimizing Compiler for ML},
year = {1996},
booktitle = {Proc. {ACM} {SIGPLAN} '96 Conference on Programming Language Design and Implementation},
pages = {181--192},
author = {D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee}
}
@phdthesis{shao94,
school = {Princeton University},
title = {Compiling Standard {ML} for Efficient Execution on Modern Machines},
year = {1994},
author = {Zhong Shao}
}
@inproceedings{gmachine,
month = {September},
title = {The {G-Machine}: A fast, graph-reduction evaluator},
year = {1985},
booktitle = {Functional Programming Languages and Computer Architecture},
pages = {400--413},
editor = {Jean-Pierre Jouannaud},
publisher = {Springer-Verlag},
author = {R.B. Kieburtz}
}
@inproceedings{strictness,
month = {September},
title = {Strictness Analysis - A practical approach},
year = {1985},
booktitle = {Functional Programming Languages and Computer Hardware},
pages = {35--49},
editor = {Jean-Pierre Jouannaud},
publisher = {Springer-Verlag},
author = {Chris Clack and Simon {Peyton Jones}}
}
@book{fl-impl,
title = {Implementing Functional Languages - A Tutorial},
year = {1992},
publisher = {Prentice Hall International},
author = {Simon {Peyton Jones} and David Lester}
}
@phdthesis{capretta-thesis,
school = {Katholieke Universiteit Nijmegen},
title = {Abstraction and Computation},
year = {2002},
author = {Venanzio Capretta}
}
@article{bird-pointer,
journal = {Journal of Functional Programming},
number = {3},
month = {May},
volume = {11},
title = {Unfolding Pointer Algorithms},
year = {2001},
pages = {347--358},
author = {Richard S. Bird}
}
@article{impl-tp,
journal = {Journal of Functional Programming},
number = {2},
month = {March},
volume = {9},
title = {Implementing Theorem Provers in a Purely Functional Style},
year = {1999},
pages = {147--166},
author = {Keith Hanna}
}
@article{shrink-lambda,
journal = {Journal of Functional Programming},
number = {5},
month = {September},
volume = {7},
title = {Shrinking Lambda Expressions in Linear Time},
year = {1997},
pages = {515--540},
author = {Andrew W. Appel and Trevor Jim}
}
@article{stack-tal,
journal = {Journal of Functional Programming},
number = {1},
month = {January},
volume = {12},
title = {Stack-based Typed Assembly Language},
year = {2002},
pages = {43--88},
author = {Greg Morrisset and Karl Crart and Neal Glew and David Walker}
}
@article{runtime-lamsig,
journal = {Journal of Functional Programming},
number = {2},
month = {March},
volume = {8},
title = {Functional Runtime Systems within the lambda-sigma Calculus},
year = {1998},
pages = {131--176},
author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
}
@article{busylazy,
journal = {Journal of Functional Programming},
number = {6},
month = {November},
volume = {11},
title = {How to look busy while being as lazy as ever: the Implementation of a lazy functional debugger},
year = {2001},
pages = {629--671},
author = {Henrik Nilsson}
}
@article{lazyveager,
journal = {Journal of Functional Programming},
number = {5},
month = {September},
volume = {7},
title = {More haste, less speed: lazy versus eager evaluation},
year = {1997},
pages = {541--547},
author = {Richard Bird and Geraint Jones and Oege {de Moor}}
}
@article{jvm-fp,
journal = {Journal of Functional Programming},
number = {6},
month = {November},
volume = {9},
title = {Compiling lazy functional programs for the Java Virtual Machine},
year = {1999},
pages = {579--603},
author = {David Wakeling}
}
@book{isabelle,
publisher = {Springer-Verlag},
series = {LNCS},
volume = {2283},
month = {March},
title = {Isabelle/HOL - A proof assistant for higher order logic},
year = {2002},
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}
}
@article{ghc-inliner,
journal = {Journal of Functional Programming},
number = {4},
month = {September},
volume = {12},
title = {Secrets of the {Glasgow Haskell Compiler} inliner},
year = {2002},
pages = {393--434},
author = {Simon {Peyton Jones} and Simon Marlow}
}
@article{dynamic-fp,
journal = {Journal of Functional Programming},
number = {1},
month = {January},
volume = {8},
title = {The dynamic compiliation of lazy functional programs},
year = {1998},
pages = {61--81},
author = {David Wakeling}
}
@misc{isabelle-ref,
month = {March},
title = {Isabelle Reference Manual},
year = {2002},
author = {Lawrence C. Paulson}
}
@article{debruijn-nested,
journal = {Journal of Functional Programming},
number = {1},
month = {January},
volume = {9},
title = {de Bruijn notation as a nested datatype},
year = {1999},
pages = {77--91},
author = {Richard S. Bird and Ross Paterson}
}
@article{perfect-trees,
journal = {Journal of Functional Programming},
number = {3},
month = {May},
volume = {10},
title = {Perfect trees and bit-reversal permutations},
year = {2000},
pages = {305--317},
author = {Ralf Hinze}
}
@phdthesis{paulin-extraction,
school = {Paris 7},
title = {Extraction de programmes dans le Calcul des Constructions},
year = {1989},
author = {Christine Paulin-Mohring}
}
@phdthesis{santos95,
school = {University of Glasgow},
title = {Compilation By Transformation In Non-Strict Functional Languages},
year = {1995},
author = {{Andr\'{e} Lu\'{i}s de Medeiros} Santos}
}
@book{cps,
title = {Compiling With Continuations},
year = {1992},
publisher = {Cambridge University Press},
author = {Andrew W. Appel}
}
@techreport{SKIM,
number = {31},
title = {The {SKIM} microprogrammer's guide},
year = {1983},
institution = {University of Cambridge},
author = {W.R. Stoye}
}
@misc{NORMA,
title = {An Overview of Burroughs {NORMA}},
year = {1985},
author = {H. Richards}
}
@book{ml,
title = {The Definition of Standard ML --- Revised},
year = {1997},
publisher = {MIT Press},
author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}
}
@misc{ml71,
title = {An intuitionistic theory of types},
year = {1971},
author = {Per Martin-L\"{o}f}
}
@phdthesis{girard-thesis,
school = {Universit\'{e} Paris VII},
title = {Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur},
year = {1972},
author = {Jean-Yves Girard}
}
@inproceedings{ml75,
title = {An intuitionistic theory of types: predicative part},
year = {1975},
booktitle = {Logic Colloquium '73},
editor = {H. Rose and J.C. Shepherdson},
publisher = {North-Holland},
author = {Per Martin-L\"{o}f}
}
@inproceedings{cpm90,
title = {Inductively defined types},
year = {1990},
author = {Thierry Coquand and Christine Paulin-Mohring},
series = {LNCS},
volume = {417},
publusher = {Springer-Verlag}
}
@phdthesis{fpcustom,
month = {May},
school = {Computer Lab, University of Cambridge},
title = {The Implementation of Functional Languages using Custom Hardware},
year = {1985},
author = {W.R. Stoye}
}
@phdthesis{hughesthesis,
month = {September},
school = {Programming Research Group, Oxford},
title = {The design and implementation of programming languages},
year = {1984},
author = {John Hughes}
}
@inproceedings{tim,
volume = {274},
title = {{TIM} -- A simple lazy abstract machine to execute supercombinators},
year = {1987},
booktitle = {Functional Programming Languages and Computer Architecture},
publisher = {Springer-Verlag},
author = {John Fairbairn and Stuart Wray},
pages = {34--45},
series = {LNCS}
}
@techreport{abc,
title = {The {ABC} machine -- A Sequential Stack-based Abstract Machine For Graph Rewriting},
year = {1990},
institution = {University of Nijmegen},
author = {P.W.M. Koopman and M.C.J.D. van {Eekelen} and E.G.J.M.H. Ncker and J.E.W. Smetsers and M.J. Plasmeijer}
}
@techreport{implicit,
title = {On Implicit Arguments},
year = {1994},
institution = {Faculty of Science, University of Tokyo},
author = {Masami Hagiya and Yozo Toda}
}
@book{semantics,
title = {Denotational Semantics},
year = {1986},
publisher = {Wm. C. Brown},
author = {David A. Schmidt}
}
@inproceedings{lazyml,
month = {August},
title = {A compiler for {Lazy} {ML}},
year = {1984},
booktitle = {Proceedings of the {ACM} Symposium on Lisp and Functional Programming},
pages = {218--227},
author = {Lennart Augustsson}
}
@inproceedings{nu-g,
title = {Parallel graph reduction with the $\langle\nu,G\rangle$-machine},
year = {1989},
booktitle = {Functional Programming Languages and Computer Architecture},
publisher = {ACM Press},
author = {Lennart Augustsson and Thomas Johnsson}
}
@book{k&r,
title = {The C programming language},
year = {1988},
publisher = {Prentice-Hall},
author = {Brian W. Kernighan and Dennis M. Ritchie}
}
@misc{c--garbage,
title = {C--: a portable assembly language that supports garbage collection},
year = {1999},
author = {Simon {Peyton Jones} and Norman Ramsey and Fermin Reig},
note = {Invited talk at PPDP'99}
}
@misc{epigram,
howpublished = {http://www.dur.ac.uk/CARG/epigram.html},
title = {Project Proposal: {Epigram}: Innovative Programming via Inductive Families},
year = {2002},
author = {Zhaohui Luo and James McKinna and Paul Callaghan and Conor McBride}
}
@misc{ghc-rewrite,
title = {Playing by the Rules: Rewriting as a practical optimisation technique in {GHC}},
year = {2001},
author = {Simon {Peyton Jones} and Andrew Tolmach and Tony Hoare}
}
@UNPUBLISHED{implicit-pollack,
AUTHOR = {Robert Pollack},
TITLE = {Implicit Syntax},
NOTE = {Informal Proceedings of First Workshop on
Logical Frameworks, Antibes},
YEAR = {1990},
MONTH = MAY
}
@article{transform-haskell,
journal = {Science of Computer Programming},
volume = {32},
title = {A transformation-based optimiser for {Haskell}},
year = {1998},
pages = {3--47},
author = {Simon {Peyton Jones} and Andr\'{e} L. M. Santos}
}
@inproceedings{knuth-bendix,
title = {Simple Word Problems in Universal Algebras},
year = {1970},
booktitle = {Computational Problems in Abstract Algebra},
pages = {263--298},
editor = {John Leech},
publisher = {Pergamon Press},
author = {Donald E. Knuth and Peter B. Bendix}
}
@inproceedings{phantomfun,
title = {Fun With Phantom Types},
author = {Ralf Hinze},
pages = {245--262},
year = {2003},
crossref = {funprogramming},
booktitle = {The Fun Of Programming},
publisher = {Palgrave}
}
@book{funprogramming,
month = {March},
title = {The Fun Of Programming},
year = {2003},
editor = {Jeremy Gibbons and Oege {de Moor}},
publisher = {Palgrave},
series = {Cornerstones of Computing}
}
@inproceedings{anderson-proof,
title = {Representing Proof Transformations For Program Optimization},
year = {1994},
booktitle = {International Conference On Automated Deduction},
publisher = {Springer Verlag},
author = {Penny Anderson}
}
@phdthesis{daria-thesis,
month = {April},
school = {Institute of Informatics, Warsaw University},
title = {Termination of Rewriting in the Calculus of Constructions},
year = {2003},
author = {Daria Walukiewicz-Chrzaszcz}
}
@inproceedings{change-data,
title = {Changing Data Structures In Type Theory: A Study Of Natural Numbers},
year = {2001},
booktitle = {Types For Proofs And Programs 2000},
pages = {181--196},
editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
publisher = {Springer},
author = {Nicolas Magaud and Yves Bertot}
}
@phdthesis{nico-thesis,
title = {Changement de Representation des donn\'{e}es dans le Calcul de Constructions},
author = {Nicolas Magaud},
year = {2003},
month = {October},
school = {Universit\'{e} de Nice - Sophia Antipolis}
}
@book{patterns,
title = {Design Patterns},
year = {1995},
publisher = {Addison Wesley},
author = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides}
}
@misc{ghchugs,
month = {August},
title = {The New {GHC}/{Hugs} Runtime System},
year = {1998},
author = {Simon Marlow and Simon {Peyton Jones}}
}
@misc{stgrevised,
month = {February},
title = {The {STG} runtime system (revised)},
year = {1999},
author = {Simon {Peyton Jones} and Simon Marlow and Alastair Reid},
howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
}
@inproceedings{optimistic,
month = {March},
title = {Optimistic Evaluation --- an adaptive evaluation strategy for non-strict programs},
year = {2003},
author = {Robert Ennals and Simon {Peyton Jones}},
booktitle = {International Conference on Functional Programming},
pages = {287--298}
}
@phdthesis{ennals-thesis,
title = {Adaptive Evaluation of Non-Strict Programs},
author = {Robert Ennals},
year = {2003},
month = {December},
school = {King's College, University of Cambridge}
}
@article{garbage,
journal = {ACM Computing Surveys},
number = {3},
volume = {13},
title = {Garbage Collection of Linked Data Structures},
year = {1981},
pages = {341--367},
author = {Jacques Cohen}
}
@article{baker-gc,
journal = {Communications of the ACM},
number = {4},
month = {April},
volume = {21},
title = {List Processing In Real Time On A Serial Computer},
year = {1978},
pages = {280--294},
author = {Henry G. {Baker Jr}}
}
@misc{bc-rec,
month = {February},
title = {Modelling General Recursion in Type Theory},
year = {2003},
note = {Under consideration for publication in Math. Struct. in Comp. Science. Draft, DCS, CTH --- INRIA, Sophia Antipolis, France},
author = {Ana Bove and Venanzio Capretta}
}
@misc{global-tag,
title = {Global Tagging Optimization by Type Inference},
year = {1992},
author = {Fritz Henglein}
}
@book{esr,
month = {October},
title = {The Cathedral And The Bazaar},
year = {1999},
publisher = {O'Reilly},
author = {Eric Raymond}
}
@book{manmonth,
title = {The Mythical Man-month: Essays on Software Engineering},
year = {1975},
publisher = {Addison Wesley},
author = {Frederick P. Brooks}
}
@inproceedings{evalpush,
title = {How to make a fast curry: push/enter vs eval/apply},
year = {2004},
author = {Simon Marlow and Simon {Peyton Jones}},
booktitle = {International Conference on Functional Programming, Snowbird},
pages = {4--15}
}
@phdthesis{boquist-thesis,
month = {April},
school = {Chalmers University of Technology},
title = {Code Optimisation Techniques for Lazy Functional Languages},
year = {1999},
author = {Urban Boquist}
}
@book{formal-spec,
title = {Formal Specification Of Programming Languages},
year = {1981},
publisher = {Prentice-Hall},
author = {Frank G. Pagan}
}
@inproceedings{elim-motive,
title = {Elimination With A Motive},
year = {2000},
booktitle = {Types for Proofs and Programs},
pages = {197--216},
editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
publisher = {Springer},
author = {Conor McBride}
}
@article{telescope,
journal = {Information and Computation},
number = {2},
month = {April},
volume = {91},
title = {Telescoping Mappings in Typed Lambda Calculus},
year = {1991},
pages = {189--204},
author = {N.G. de Bruijn}
}
@misc{typeintype,
title = {Typechecking is undecidable when 'type' is a type},
year = {1989},
author = {Mark B. Reinhold}
}
@misc{core,
month = {September},
title = {An External Representation for the {GHC} Core Language},
year = {2001},
author = {Andrew Tolmach and {The GHC Team}}
}
@article{deforestation,
journal = {Theoretical Computer Science},
volume = {73},
title = {Deforestation: Transforming programs to eliminate trees},
year = {1990},
pages = {231--248},
author = {Philip Wadler}
}
@misc{hep,
month = {July},
title = {Architecture of the {Haskell} Execution Platform},
year = {1999},
author = {Julian Seward and Simon Marlow and Andy Gill and Sigbjorn Finne and Simon {Peyton Jones} },
note = {Version 6},
howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
}
@mastersthesis{wahlstedt-thesis,
month = {October},
school = {Chalmers University Of Technology},
title = {Detecting Termination Using Size Change In Parameter Values},
year = {2000},
author = {David Wahlstedt}
}
@inproceedings{size-change,
title = {The size-change principle for program termination},
year = {2001},
booktitle = {Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
author = {Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. }
}
@article{ski-turner,
journal = {Software -- Practice and Experience},
volume = {9},
title = {A new implementation technique for applicative languages},
year = {1979},
pages = {31--49},
author = {David Turner}
}
@inproceedings{turner-strong,
number = {1022},
title = {Elementary Strong Functional Programming},
year = {1996},
booktitle = {First International Symposium on Functional Programming Languages in Education, Nijmegen, Netherlands, December 1995.},
pages = {1--13},
publisher = {Springer},
author = {David Turner},
series = {LNCS}
}
@misc{clean,
title = {The {Concurrent CLEAN} Language Report (draft)},
year = {2003},
author = {Rinus Plasmeijer and Marko van Eekelen},
howpublished = {Available from \verb+http://www.cs.kun.nl/~clean/+}
}
@article{burstall-struct,
journal = {Computer Journal},
number = {1},
volume = {12},
title = {Proving Properties of Programs By Structural Induction},
year = {1969},
pages = {41--48},
author = {Rod Burstall}
}
@incollection{ barendregt-types,
author = "Henk Barendregt",
title = "Lambda Calculi with Types",
booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky \& Gabbay \& Maibaum (Eds.)",
publisher = "Clarendon",
volume = "2",
year = "1992",
url = "citeseer.nj.nec.com/barendregt92lambda.html" }
@book{curry-feys,
title = {Combinatory Logic, volume 1},
year = {1958},
publisher = {North Holland},
author = {Haskell B. Curry and Robert Feys}
}
@phdthesis{bove-thesis,
month = {November},
school = {Chalmers University of Technology},
title = {General Recursion in Type Theory},
year = {2002},
author = {Ana Bove}
}
@inbook{ml-cm,
title = {Constructive Mathematics and Computer Programming},
year = {1985},
booktitle = {Mathematical Logic and Programming Languages},
publisher = {Prentice Hall},
author = {Per Martin-L\"{o}f}
}
@inproceedings{howard,
title = {The formulae-as-types notion of construction},
year = {1980},
booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
editor = {Jonathan P. Seldin and J. Roger Hindley},
publisher = {Academic Press},
author = {William A. Howard},
note = {A reprint of an unpublished manuscript from 1969}
}
@inproceedings{talx86,
title = {TALx86: A Realistic Typed Assembly Language},
year = {1999},
booktitle = {ACM SIGPLAN Workshop on Compiler Support for System Software},
pages = {25--35},
author = {Greg Morrisett and Karl Crary and Neal Glew and Dan Grossman and Richard Samuels and Frederick Smith and David Walker and Stephanie Weirich and Steve Zdancewic}
}
@inproceedings{bove-capretta,
volume = {2152},
title = {Nested General Recursion and Partiality in Type Theory},
year = {2001},
booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLS 2001},
pages = {121--135},
editor = {Richard J. Boulton and Paul B. Jackson},
publisher = {Springer-Verlag},
author = {Ana Bove and Venanzio Capretta},
series = {LNCS}
}
@misc{lvm,
month = {November},
title = {LVM, the lazy virtual machine},
year = {2002},
author = {Daan Leijen}
}
@misc{ocaml,
howpublished = {\verb+http://caml.inria.fr/ocaml/htmlman/+},
month = {August},
title = {The {Objective Caml} system release 3.06},
year = {2002},
author = {Xavier Leroy}
}
@misc{lambdagoto,
title = {Lambda : The Ultimate Goto},
year = {1977},
author = {Guy L. {Steele Jr}},
note = {MIT AI Memo 443}
}
@inproceedings{ liu-tail,
author = "Yanhong A. Liu and Scott D. Stoller",
title = "From Recursion to Iteration: What are the Optimizations?",
booktitle = "Partial Evaluation and Semantic-Based Program Manipulation",
pages = "73-82",
year = "2000",
url = "citeseer.nj.nec.com/liu00from.html" }
@inproceedings{aczel77,
title = {An Introduction To Inductive Definitions},
year = {1977},
booktitle = {Handbook of Mathematical Logic},
editor = {J. Barwise},
publisher = {North Holland},
author = {Peter Aczel}
}
@inproceedings{inductive-plastic,
volume = {1956},
title = {Implementation Techniques for Inductive Types in {Plastic}},
year = {1999},
booktitle = {Types for Proofs and Programs},
pages = {94--113},
editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith},
publisher = {Springer-Verlag},
author = {Paul Callaghan and Zhaohui Luo},
series = {LNCS}
}
@misc{graham,
howpublished = {Available from \verb+http://www.paulgraham.com/+},
month = {April},
title = {The Hundred Year Language},
year = {2003},
author = {Paul Graham},
note = {Keynote address at PyCon 2003}
}
@inproceedings{gimenez98,
volume = {1443},
title = {Structural Recursive Definitions in Type Theory},
year = {1998},
booktitle = {Proceedings of ICALP '98},
publisher = {Springer-Verlag},
author = {Eduardo Gim\'{e}nez},
series = {LNCS}
}
@article{quicksort,
journal = {Computer Journal},
number = {1},
volume = {5},
title = {Quicksort},
year = {1962},
pages = {10--15},
author = {C.A.R. Hoare}
}
@phdthesis{goguen-thesis,
school = {University of Edinburgh},
title = {A Typed Operational Semantics for Type Theory},
year = {1994},
author = {Healfdene Goguen}
}
@article{ph-universes,
journal = {Theoretical Computer Science},
number = {1},
volume = {89},
title = {Type Checking With Universes},
year = {1991},
pages = {107--136},
author = {Robert Harper and Randy Pollack}
}
@inproceedings{pm-compile,
month = {September},
title = {Compiling Pattern Matching},
year = {1985},
booktitle = {Functional Programming Languages and Computer Architecture},
pages = {368--381},
editor = {Jean-Pierre Jouannaud},
publisher = {Springer-Verlag},
author = {Lennart Augustsson}
}
@phdthesis{lena-thesis,
school = {Chalmers University of Technology, G\"{o}teborg},
title = {The implementation of {ALF} -- A Proof Editor based on {Martin-L\"{o}f}'s Monomorphic Type Theory with Explicit Substitutions},
year = {1994},
author = {Lena Magnusson}
}
@article{view-left,
journal = {Journal of Functional Programming},
number = {1},
volume = {14},
title = {The View From The Left},
year = {2004},
author = {Conor McBride and James McKinna},
pages = {69--111}
}
@inproceedings{not-a-number,
author = {Conor McBride and James McKinna},
title = {I am not a number, {I} am a free variable},
year = {2004},
booktitle = {Proceedings of the ACM SIGPLAN Haskell Workshop}
}
@misc{profiling,
title = {Time and Space Profiling for Non-Strict, Higher Order Functional Languages},
year = {1995},
author = {Patrick M. Sansom and Simon {Peyton Jones}}
}
@inbook{pattern-matching,
title = {The Implementation of Functional Programming Languages},
year = {1987},
booktitle = {The Implementation of Functional Programming Languages},
pages = {78--103},
editor = {Simon {Peyton Jones}},
chapter = {5},
publisher = {Prentice Hall},
author = {Philip Wadler},
crossref = {pj-imp}
}
@misc{tag-elim,
title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},
year = {2000},
author = {Walid Taha and Henning Makholm}
}
@inproceedings{extraction-coq,
title = {A New Extraction for {Coq}},
year = {2002},
booktitle = {Types for proofs and programs},
editor = {Herman Geuvers and Freek Wiedijk},
publisher = {Springer},
author = {Pierre Letouzey},
series = {LNCS}
}
@phdthesis{mcbride-snr-thesis,
school = {Queen's University of Belfast},
title = {Computer Aided Manipulation of Symbols},
year = {1970},
author = {Fred McBride}
}
@article{ho-strictness,
journal = {Science of Computer Programming},
volume = {7},
title = {Strictness analysis for higher-order functions},
year = {1986},
pages = {249--278},
author = { Geoffrey L. Burn and Chris Hankin and Samson Abramsky}
}
@phdthesis{mycroft-thesis,
school = {Dept Computer Science, University of Edinburgh},
title = {Abstract interpretation and optimising transformations for applicative programs},
year = {1981},
author = {A. Mycroft}
}
@inproceedings{bc-nested,
month = {September},
volume = {2152},
title = {Nested General Recursion and Partiality in Type Theory},
year = {2001},
booktitle = {Theorem Proving In Higher Order Logics: 14th International Conferences, TPHOLS 2001},
pages = {121--135},
publisher = {Springer--Verlag},
author = {Ana Bove and Venanzio Capretta},
series = {LNCS}
}
@techreport{bove-mutual,
month = {May},
title = {Mutual General Recursion in Type Theory},
year = {2002},
institution = {Department of Computing Science, Chalmers University of Technology},
author = {Ana Bove}
}
@article{berardi-pruning,
journal = {Journal of Logic and Computation},
number = {5},
volume = {6},
title = {Pruning Simply Typed Lambda Terms},
year = {1996},
pages = {663--681},
author = {Stefano Berardi}
}
@article{milner-tc,
journal = {Journal of Computer and System Science},
volume = {17},
title = {A Theory of Type Polymorphism in Programming},
year = {1978},
pages = {348--75},
author = {R. Milner}
}
@inproceedings{extt,
title = {Inductive Families Need Not Store Their Indices},
year = {2004},
booktitle = {Types for Proofs and Programs 2003},
author = {Edwin Brady and Conor McBride and James McKinna},
editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
publisher = {Springer},
volume = {3085},
pages = {115--129}
}
@book{luo94,
title = {Computation and Reasoning -- A Type Theory for Computer Science},
year = {1994},
publisher = {OUP},
author = {Zhaohui Luo},
series = {Intl. Series of Monographs on Comp. Sci.}
}
@article{backus78,
journal = {Communications of the ACM},
month = {August},
volume = {21},
title = {Can Programming Be Liberated From the {Von Neumann} Style?},
year = {1978},
pages = {280--294},
author = {John Backus}
}
@misc{henk,
month = {May},
title = {Henk: A Typed Intermediate Language},
year = {1997},
author = {Simon {Peyton Jones} and Erik Meijer}
}
@article{thunks,
journal = {Journal of Functional Programming},
number = {3},
month = {May},
volume = {7},
title = {Thunks and the $\lambda$-calculus},
year = {1997},
pages = {303--319},
author = {John Hatcliff and Olivier Danvy}
}
@inproceedings{grin-project,
author = "Urban Boquist and Thomas Johnsson",
title = "The {GRIN} Project: A Highly Optimising Back End for Lazy Functional Languages",
booktitle = "Implementation of Functional Languages",
pages = "58--84",
year = "1996",
url = "citeseer.ist.psu.edu/boquist96grin.html" }
@misc{boehm-gc,
howpublished = {\verb+http://www.hpl.hp.com/personal/Hans_Boehm/gc/+},
title = {A garbage collector for {C} and {C++}},
year = {2001},
author = {Hans-J. Boehm and Alan J. Demers and {Xerox Corporation Silicon Graphic} and {Hewlett-Packard Company}}
}
@misc{art-interpreter,
month = {May},
title = {The Art of the Interpreter or, the Modularity Complex (Parts Zero, One, and Two)},
year = {1978},
author = {Guy Lewis {Steele, Jr.} and Gerald Jay Sussman},
note = {MIT AI Lab. AI Lab Memo AIM-453}
}
@inproceedings{gimenez,
title = {Codifying Guarded Definitions With Recursive Schemes},
year = {1994},
booktitle = {Proceedings of TYPES 1994},
pages = {39--59},
author = {Eduardo Gim\'{e}nez}
}
@manual{ghc-manual,
title = {The Glasgow Haskell Compiler User's Guide, Version 6.0},
year = {2003},
author = {The {GHC Team}}
}
@article{rbtree,
journal = {Journal of Functional Programming},
number = {4},
month = {May},
volume = {9},
title = {Red-Black Trees In A Functional Setting},
year = {1999},
pages = {471--477},
author = {Chris Okasaki}
}
@inproceedings{dt-data,
author = "Hongwei Xi",
title = {{Dependently Typed Data Structures}},
booktitle = "Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99)",
year = 1999,
month = "September",
pages = "17--32",
address = "Paris",
}
@misc{krivine,
title = {On the Correctness and Efficiency of the {Krivine} Machine},
year = {2003},
month = {October},
author = {Mitchell Wand and Daniel P. Friedman},
howpublished = {Submitted for publication}
}
@inproceedings{nbe-filinski,
title = {Normalization by Evaluation for the Computational Lambda-Calculus},
year = {2001},
month = {May},
booktitle = {Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001},
author = {Andrzej Filinski},
pages = {151--165},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {2044}
}
@inproceedings{filinski-nbesem,
title = {A semantic account of type-directed partial evaluation},
year = {1999},
author = {Andrzej Filinski},
editor = {G. Nadathur},
booktitle = {International Conference on Principles and Practice of Declarative Programming},
volume = {1702},
series = {LNCS},
pages = {378--395},
publisher = {Springer-Verlag}
}
@article{secd,
title = {The mechanical evaluation of expressions},
author = {P.J. Landin},
year = {1964},
journal = {Computer Journal},
volume = {6},
pages = {308--320}
}
@misc{lispkit,
title = {The {LispKit} Manual},
author = {Peter Henderson and Geraint Jones and Simon Jones},
year = {1982},
howpublished = {Oxford University Computing Laboratory}
}
@inproceedings{wells-undecidable,
title = {Typability and Type Checking in the Second-order $\lambda$-calculus are equivalent and undecidable},
author = {J. Wells},
year = {1994},
month = {July},
booktitle = {Proc. 9th Ann. IEEE Symp. Logic Comput. Sci.}
}
@misc{patguards,
title = {Pattern Guards and Transformational Patterns},
author = {Martin Erwig and Simon {Peyton Jones}},
year = {2000},
howpublished = {Haskell Workshop}
}
@misc{alfa-manual,
title = {Alfa Users' Guide},
author = {Thomas Hallgren},
year = {2001},
howpublished = {Available from \verb+http://www.cs.chalmers.se/~hallgren/Alfa/+}
}
@inproceedings{nofib,
title = {The nofib Benchmark Suite of {Haskell} Programs},
author = {Will Partain},
year = {1992},
booktitle = {Functional Programming},
editor = {J. Launchbury and P.L. Sansom},
series = {Workshops in Computing},
publisher = {Springer Verlag}
}
@article{shape,
title = {Shape in Computing},
author = {Barry Jay},
journal = "{ACM} Computing Surveys",
year = "1996",
volume = "28",
number = "2",
pages = "355--357",
}
@misc{ffi,
title = {The {Haskell 98} Foreign Function Interface 1.0: An Addendum to the {Haskell 98} Report},
editor = {Manuel Chakravarty},
key = {FFI},
year = {2002},
month = {December},
howpublished = {Available from \verb+http://www.haskell.org/+}
}
@misc{perlxs,
title = {Perl {XS} Reference Manual},
author = {Dean Roehrich and {The Perl Porters}},
year = {1996},
howpublished = {\verb+http://www.perldoc.com/perl5.6/pod/perlxs.html+}
}
@misc{swig,
title = {{SWIG} : An Easy to Use Tool for Integrating Scripting Languages with {C} and {C++}},
author = {David M. Beazley},
year = {1996},
howpublished = {\verb+http://www.swig.org/papers/Tcl96/tcl96.html+}
}
@inproceedings{types-prog,
title = {Type Systems for Programming Languages},
booktitle = {Handbook of Theoretical Computer Science},
author = {John C. Mitchell},
pages = {365--458},
year = {1990},
crossref = {htcs}
}
@book{htcs,
title = {Handbook of Theoretical Computer Science},
editor = {J. van Leeuwen},
publisher = {Elsevier Science},
year = {1990}
}
@misc{r5rs,
title = {Revised$^5$ Report on the Algorithmic Language Scheme},
author = {Richard Kelsey and William Clinger and Jonathan Rees},
year = {1998},
month = {February},
howpublished = {Available from \verb+http://www.schemers.org/+}
}