Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

3847 lines (3374 sloc) 110.838 kB
@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 = {http://doi.acm.org/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},
ee = {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 = {http://doi.{ACM}.org/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 = {http://dx.doi.org/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 = {http://doi.{ACM}.org/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},
ee = {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 = {http://doi.{ACM}.org/10.1145/1863543.1863569},
publisher = {{ACM}},
address = {New York, NY, USA},
}
@inproceedings{levitation,
author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
title = {The gentle art of levitation},
booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
year = {2010},
isbn = {978-1-60558-794-3},
pages = {3--14},
location = {Baltimore, Maryland, USA},
doi = {http://doi.{ACM}.org/10.1145/1863543.1863547},
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 = {http://doi.{ACM}.org/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 = {http://doi.{ACM}.org/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 = {\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 = {\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
}
Jump to Line
Something went wrong with that request. Please try again.