@@ -0,0 +1,3836 @@
2+ author = {McBride, Conor and Paterson, Ross},
3+ title = {Applicative programming with effects},
4+ journal = {J. Funct. Program.},
12+ url = {http://portal.acm.org/citation.cfm?id=1348940.1348941},
13+ doi = {10.1017/S0956796807006326},
15+ publisher = {Cambridge University Press},
16+ address = {New York, NY, USA},
20+ author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam},
21+ title = {Lava: hardware design in {Haskell}},
22+ booktitle = {Proceedings of the third ACM SIGPLAN international conference on Functional programming},
25+ isbn = {1-58113-024-4},
26+ location = {Baltimore, Maryland, United States},
29+ url = {http://doi.acm.org/10.1145/289423.289440},
30+ doi = {http://doi.acm.org/10.1145/289423.289440},
33+ address = {New York, NY, USA},
36+@inproceedings{plpv11,
37+ author = {Edwin Brady},
38+ title = {Idris --- Systems programming meets full dependent types},
39+ booktitle = {Programming Languages meets Program Verification {(PLPV 2011)}},
42+ ee = {http://doi.acm.org/10.1145/1929529.1929536},
43+ bibsource = {DBLP, http://dblp.uni-trier.de}
46+@inproceedings{epicdraft,
47+ author = {Edwin Brady},
48+ title = {Epic --- a library for generating compilers},
50+ booktitle = {Draft Proceedings of {Trends in Functional Programming} ({TFP} '11)}
53+@inproceedings{ynot08,
54+ author = {Nanevski,, Aleksandar and Morrisett,, Greg and
55+ Shinnar,, Avraham and Govereau,, Paul and Birkedal,,
57+ title = {Ynot: reasoning with the awkward squad},
58+ booktitle = {{ICFP} '08: Proceeding of the 13th {ACM SIGPLAN}
59+ international conference on Functional programming},
61+ isbn = {978-1-59593-919-7},
63+ location = {Victoria, BC, Canada},
64+ doi = {http://doi.acm.org/10.1145/1411204.1411237},
66+ address = {New York, NY, USA},
70+ author = {Edwin Brady and Kevin Hammond},
71+ title = {Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols},
73+ journal = {Fundamenta Informaticae},
79+@inproceedings{devil-osdi00,
80+ author = {Fabrice M{\'e}rillon and
81+ Laurent R{\'e}veill{\`e}re and
85+ title = {Devil: An IDL for Hardware Programming},
86+ booktitle = {4th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2000)},
91+@INPROCEEDINGS{device-osdi08,
92+ author = {Dan Williams and Patrick Reynolds and Kevin Walsh and Emin Gün Sirer and Fred B. Schneider},
93+ title = {Device driver safety through a reference validation mechanism},
94+ booktitle = {8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)},
98+@inproceedings{sozeau-equations,
99+ author = {Matthieu Sozeau},
100+ title = {Equations: A Dependent Pattern-Matching Compiler},
101+ booktitle = {First International Conference on Interactive Theorem Proving (ITP 2010)},
104+ ee = {http://dx.doi.org/10.1007/978-3-642-14052-5_29},
105+ crossref = {DBLP:conf/itp/2010},
106+ bibsource = {DBLP, http://dblp.uni-trier.de}
110+@inproceedings{packet-type,
111+ author = "Peter J. McCann and Satish Chandra",
112+ title = "Packet Types: Abstract Specification of Network Protocol Messages",
114+ booktitle = "SIGCOMM '00",
118+@inproceedings{qs-types,
119+ author = {Eelis {van der Weegen} and James McKinna},
121+ title={A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq},
124+ series = {Lecture Notes in Computer Science},
125+ publisher = {Springer}
129+@inproceedings{totalparser,
130+ author = {Nils Anders Danielsson},
131+ title = {Total Parser Combinators},
132+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
134+ isbn = {978-1-60558-794-3},
136+ location = {Baltimore, Maryland, USA},
137+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},
138+ publisher = {{ACM}},
139+ address = {New York, NY, USA},
144+ title="{Internet Protocol}",
145+ series="Request for Comments",
147+ howpublished="RFC 791 (Standard)",
149+ organization="Internet Engineering Task Force",
152+ note="Updated by RFC 1349",
153+ url="http://www.ietf.org/rfc/rfc791.txt",
159+ title="{Internet Control Message Protocol}",
160+ series="Request for Comments",
162+ howpublished="RFC 792 (Standard)",
164+ organization="Internet Engineering Task Force",
167+ note="Updated by RFCs 950, 4884",
168+ url="http://www.ietf.org/rfc/rfc792.txt",
171+@INPROCEEDINGS{Dybjer-indrec,
172+ author = {Peter Dybjer and Anton Setzer},
173+ title = {A Finite Axiomatization of Inductive-Recursive Definitions},
174+ booktitle = {Tyed Lambda Calculi and Applications},
176+ series = {Lecture Notes in Computer Science},
179+ publisher = {Springer}
183+ author = {W. Richard Stevens},
184+ title = {{TCP/IP} Illustrated Volume 1: The Protocols},
186+ publisher = {Addison Wesley},
187+ isbn = {0-201-63346-9}
190+@inproceedings{coqtypeclasses,
191+ author = {Sozeau, Matthieu and Oury, Nicolas},
192+ title = {First-Class Type Classes},
193+ booktitle = {TPHOLs '08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics},
195+ isbn = {978-3-540-71065-3},
197+ location = {Montreal, P.Q., Canada},
198+ doi = {http://dx.doi.org/10.1007/978-3-540-71067-7_23},
199+ publisher = {Springer-Verlag},
200+ address = {Berlin, Heidelberg},
204+@inproceedings{kipling,
205+ author = {McBride, Conor},
206+ title = {Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation},
207+ booktitle = {WGP '10: Proceedings of the 6th {ACM} {SIGPLAN} workshop on Generic programming},
209+ isbn = {978-1-4503-0251-7},
211+ location = {Baltimore, Maryland, USA},
212+ doi = {http://doi.{ACM}.org/10.1145/1863495.1863497},
213+ publisher = {{ACM}},
214+ address = {New York, NY, USA},
217+@inproceedings{padsml,
218+ author = {Yitzhak Mandelbaum and
221+ Mary F. Fern{\'a}ndez and
223+ title = {{PADS/ML}: a functional data description language},
224+ booktitle = {POPL '07: Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on
225+ Principles of Programming Languages, POPL 2007, Nice, France,
226+ January 17-19, 2007},
229+ ee = {http://doi.{ACM}.org/10.1145/1190216.1190231},
230+ crossref = {DBLP:conf/popl/2007},
231+ bibsource = {DBLP, http://dblp.uni-trier.de}
234+@proceedings{DBLP:conf/popl/2007,
235+ editor = {Martin Hofmann and
236+ Matthias Felleisen},
237+ title = {Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on
238+ Principles of Programming Languages, POPL 2007, Nice, France,
239+ January 17-19, 2007},
241+ publisher = {{ACM}},
243+ isbn = {1-59593-575-4},
244+ bibsource = {DBLP, http://dblp.uni-trier.de}
247+@inproceedings{melange,
248+ author = {Madhavapeddy, Anil and Ho, Alex and Deegan, Tim and Scott, David and Sohan, Ripduman},
249+ title = {Melange: creating a "functional" internet},
250+ booktitle = {EuroSys '07: Proceedings of the 2nd {ACM} SIGOPS/EuroSys European Conference on Computer Systems 2007},
252+ isbn = {978-1-59593-636-3},
253+ location = {Lisbon, Portugal},
254+ doi = {http://doi.{ACM}.org/10.1145/1272996.1273009},
255+ publisher = {{ACM}},
256+ address = {New York, NY, USA},
261+@article{next700data,
262+ author = {Fisher, Kathleen and Mandelbaum, Yitzhak and Walker, David},
263+ title = {The next 700 data description languages},
264+ journal = {{SIGPLAN} Not.},
270+ doi = {http://doi.{ACM}.org/10.1145/1111320.1111039},
271+ publisher = {{ACM}},
272+ address = {New York, NY, USA},
276+@INPROCEEDINGS{xi-ats,
277+ author = {Hongwei Xi},
278+ title = {{Applied Type System} (extended abstract)},
279+ booktitle = {Types for Proofs and Programs 2003},
280+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
281+ publisher = {Springer},
282+ series = {Lecture Notes in Computer Science},
288+@inproceedings{powerpi,
289+ author = {Nicolas Oury and
291+ title = {The power of {Pi}},
292+ booktitle = {{ICFP} '08: Proceedings of the 13th {ACM} {SIGPLAN} International Conference
293+ on Functional Programming, {ICFP} 2008, Victoria, BC, Canada,
294+ September 20-28, 2008},
297+ ee = {http://doi.{ACM}.org/10.1145/1411204.1411213},
298+ crossref = {DBLP:conf/{ICFP}/2008},
299+ bibsource = {DBLP, http://dblp.uni-trier.de}
302+@proceedings{DBLP:conf/{ICFP}/2008,
303+ editor = {James Hook and
305+ title = {Proceeding of the 13th {ACM} {SIGPLAN} international conference
306+ on Functional programming, {ICFP} 2008, Victoria, BC, Canada,
307+ September 20-28, 2008},
308+ booktitle = {{ICFP}},
309+ publisher = {{ACM}},
311+ isbn = {978-1-59593-919-7},
312+ bibsource = {DBLP, http://dblp.uni-trier.de}
316+@inproceedings{security-types,
317+ author = {Morgenstern, Jamie and Licata, Daniel R.},
318+ title = {Security-typed programming within dependently typed programming},
319+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
321+ isbn = {978-1-60558-794-3},
323+ location = {Baltimore, Maryland, USA},
324+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863569},
325+ publisher = {{ACM}},
326+ address = {New York, NY, USA},
329+@inproceedings{levitation,
330+ author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
331+ title = {The gentle art of levitation},
332+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
334+ isbn = {978-1-60558-794-3},
336+ location = {Baltimore, Maryland, USA},
337+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863547},
338+ publisher = {{ACM}},
339+ address = {New York, NY, USA},
344+@INPROCEEDINGS{awkward,
345+ author = {Simon {Peyton Jones}},
346+ title = {Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in {Haskell}},
347+ booktitle = {Engineering theories of software construction},
352+@inproceedings{scrap-engine,
353+ author = {Brady, Edwin and Hammond, Kevin},
354+ title = {Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation},
355+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
357+ isbn = {978-1-60558-794-3},
359+ location = {Baltimore, Maryland, USA},
360+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},
361+ publisher = {{ACM}},
362+ address = {New York, NY, USA},
366+ author = {Chlipala, Adam},
367+ title = {Ur: statically-typed metaprogramming with type-level record computation},
368+ journal = {{SIGPLAN} Not.},
374+ doi = {http://doi.{ACM}.org/10.1145/1809028.1806612},
375+ publisher = {{ACM}},
376+ address = {New York, NY, USA},
381+@phdthesis{norell-thesis,
382+ author = {Ulf Norell},
383+ title = {Towards a practical programming language based on dependent type
385+ school = {Chalmers University of Technology},
387+ month = {September},
390+@inproceedings{open-type,
391+ author = {Schrijvers, Tom and Peyton Jones, Simon and Chakravarty, Manuel and Sulzmann, Martin},
392+ title = {Type checking with open type functions},
393+ booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},
396+ doi = {http://doi.{ACM}.org/10.1145/1411203.1411215},
397+ publisher = {{ACM}},
398+ address = {New York, NY, USA},
401+@inproceedings{ngna-dsl,
402+ title = {Domain Specific Languages ({DSL}s) for Network Protocols},
403+ author = {Saleem Bhatti and Edwin Brady and Kevin Hammond and James McKinna},
405+ booktitle = {International Workshop on Next Generation Network Architecture ({NGNA} 2009)}
408+@phdthesis{gill-thesis,
409+ title = {Cheap deforestation for non-strict functional languages},
411+ institution = {University of Glasgow},
417+ title = {Low Level Virtual Machine for {Glasgow Haskell Compiler}},
418+ author = {David Terei},
420+ howpublished = {Bachelor's Thesis, Computer Science and Engineering Dept., The University of New South Wales, Sydney, Australia}
424+ title = {{LLVM}: An Infrastructure for Multi-Stage Optimization},
425+ author = {Chris Lattner},
428+ institution = {Computer Science Dept., University of Illinois at Urbana-Champaign}
431+@inproceedings{gpu-arrays,
432+ title = {GPU Kernels as Data-Parallel Array Computations in Haskell},
433+ author = {Sean Lee and Manuel M. T. Chakravarty and Vinod Grover and Gabriele Keller.},
435+ booktitle = {Workshop on Exploiting Parallelism using GPUs and other Hardware-Assisted Methods (EPAHM 2009)}
439+ author = {Galois, Inc.},
442+ howpublished = {\url{http://cryptol.net/}}
445+@inproceedings{paradise-dsl,
446+ author = {Lennart Augustsson and Howard Mansell and Ganesh Sittampalam},
447+ title = {{Paradise: a two-stage DSL embedded in Haskell}},
448+ booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},
450+ publisher = {{ACM}},
455+ author = {Arie {van Deursen} and Paul Klint and Joost Visser},
456+ title = {Domain-Specific Languages --- an annotated bibliography},
458+ howpublished = {\url{http://homepages.cwi.nl/~arie/papers/dslbib/}}
461+@inproceedings{imperative-pe,
462+ author = {Debois, S{\o}ren},
463+ title = {Imperative program optimization by partial evaluation},
464+ booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
466+ isbn = {1-58113-835-0},
468+ location = {Verona, Italy},
469+ doi = {http://doi.{ACM}.org/10.1145/1014007.1014019},
470+ publisher = {{ACM}},
471+ address = {New York, NY, USA},
475+@inproceedings{offline-pe-termination,
476+ author = {Andersen, Peter Holst and Holst, Carsten Kehler},
477+ title = {Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language},
478+ booktitle = {Proc. SAS '96: Intl. Symp. on Static Analysis},
480+ isbn = {3-540-61739-6},
482+ publisher = {Springer},
483+ notaddress = {London, UK},
487+@inproceedings{stage-duplication,
488+ author = {Swadi, Kedar and Taha, Walid and Kiselyov, Oleg and Pasalic, Emir},
489+ title = {A monadic approach for avoiding code duplication when staging memoized functions},
490+ notbooktitle = {PEPM '06: Proceedings of the 2006 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
491+ booktitle = {Proc. PEPM '06:{ACM} Symp. on Partial Evaluation and Semantics-based Program Manipulation},
493+ isbn = {1-59593-196-1},
495+ location = {Charleston, South Carolina},
496+ doi = {http://doi.{ACM}.org/10.1145/1111542.1111570},
497+ notpublisher = {{ACM}},
498+ notaddress = {New York, NY, USA},
502+@inproceedings{concoqtion,
503+ author = {Fogarty, Seth and Pasalic, Emir and Siek, Jeremy and Taha, Walid},
504+ title = {Concoqtion: indexed types now!},
505+ booktitle = {PEPM '07: Proceedings of the 2007 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
507+ isbn = {978-1-59593-620-2},
509+ location = {Nice, France},
510+ doi = {http://doi.{ACM}.org/10.1145/1244381.1244400},
511+ publisher = {{ACM}},
512+ address = {New York, NY, USA},
515+@inproceedings{metahaskell,
516+ author = "Tim Sheard and Simon {Peyton Jones}",
517+ title = "Template metaprogramming for {Haskell}",
518+ booktitle = "{ACM} Haskell Workshop",
522+ noteditor = "Manuel M. T. Chakravarty",
523+ notpublisher = "{ACM} Press"
526+@misc{shark-profiler,
527+ title = {Optimizing your application with {Shark 4}},
529+ howpublished = {\url{http://developer.apple.com/tools/sharkoptimize.html}}
533+ title = {The Computer Language Benchmark Game},
535+ howpublished = {\url{http://shootout.alioth.debian.org/}}
539+ author = {Yoshihiko Futamura},
541+ title = "Partial Evaluation of Computation Process --– An Approach to a Compiler-Compiler",
542+ journal = {Systems, Comps., Controls},
549+ title = {Partial Evaluation and Automatic Program Generation},
550+ author = {N.D. Jones and C.K. Gomard and P. Sestoft},
552+ publisher = {Prentice Hall International}
555+@inproceedings{pantheon,
556+ author = {Sean Seefried and Manuel Chakravarty and Gabriele Keller},
557+ title = {Optimising Embedded {DSLs} using {Template Haskell}},
559+ booktitle = {{Proc. GPCE~'04: Conf. Generative Prog. and Component Eng.}},
560+ publisher = {Springer},
565+ author = {Elliott, Conal and Finne, Sigbj\orn and De Moor, Oege},
566+ title = {Compiling embedded languages},
567+ journal = {J. Funct. Program.},
573+ doi = {http://dx.doi.org/10.1017/S0956796802004574},
574+ publisher = {Cambridge University Press},
575+ address = {New York, NY, USA},
579+@inproceedings{russell,
580+ author = {Sozeau, Matthieu},
581+ title = {Program-ing finger trees in Coq},
582+ booktitle = {{ICFP} '07: Proceedings of the 12th {ACM} {SIGPLAN} international conference on Functional programming},
584+ isbn = {978-1-59593-815-2},
586+ location = {Freiburg, Germany},
587+ doi = {http://doi.{ACM}.org/10.1145/1291151.1291156},
588+ publisher = {{ACM}},
589+ address = {New York, NY, USA},
592+@inproceedings{turner-total,
593+ author = {D. A. Turner},
594+ title = {Elementary Strong Functional Programming},
596+ booktitle = "First International Symposium on Functional Programming Languages in Education",
597+ publisher = {Springer},
603+@incollection{free-theorems,
604+ author = "P. Wadler",
605+ title = "Theorems for Free!",
606+ booktitle = "{Proc. 4th Int.\ Conf.\ on Funct.\ Prog.\ Languages and Computer Arch., {FPCA}'89, London, {UK}, 11--13 Sept 1989}",
607+ publisher = "{ACM} Press",
608+ address = "New York",
611+ url = "citeseer.ist.psu.edu/wadler89theorems.html"
614+@inproceedings{TrulyConcurrent,
615+ author = {Naiyong Jin and Jifeng He},
616+ title = {Towards A Truly Concurrent Model for Processes Sharing Resources},
617+ booktitle = {Proc. 3rd {IEEE} International Conf. on Soft. Eng. and Formal Methods},
619+ isbn = {0-7695-2435-4},
621+ doi = {http://dx.doi.org/10.1109/SEFM.2005.50},
622+ publisher = {{IEEE} Computer Society},
623+ address = {Washington, DC, USA},
627+ note = {Omitted to preserve anonymity, contact PC chair for details}
631+ note = {Omitted to preserve anonymity, contact PC chair for details}
635+ note = {Omitted to preserve anonymity, contact PC chair for details}
638+@inproceedings{HaskellIO,
639+ author = {Simon L. {Peyton Jones} and Philip Wadler},
640+ title = {Imperative functional programming},
641+ booktitle = {Proc. 20th {ACM} Symposium on Principles of programming languages},
643+ isbn = {0-89791-560-7},
645+ location = {Charleston, South Carolina, United States},
646+ doi = {http://doi.{ACM}.org/10.1145/158511.158524},
647+ publisher = {{ACM}},
648+ address = {New York, NY, USA},
651+@article{CorrectnessConstruction,
653+title = "{Correctness by Construction: Better can also be Cheaper}",
654+journal = "{CrossTalk: the Journal of Defense Software Engineering}",
662+@INPROCEEDINGS{hj:popl03,
663+ AUTHOR = {M. Hofmann and S. Jost},
664+ TITLE = {Static Prediction of Heap Space Usage for First-Order Function
666+booktitle = "Proc. {POPL 2003 --- 2003 {ACM} Symp. on Principles of Programming La
671+ ORGANIZATION = {{ACM}}
675+@article{kobayashi-lock,
676+ author = {Naoki Kobayashi},
677+ title = {A type system for lock-free processes},
678+ journal = {Inf. Comput.},
684+ doi = {http://dx.doi.org/10.1016/S0890-5401(02)93171-8},
685+ publisher = {Academic Press, Inc.},
686+ address = {Duluth, MN, USA},
689+@techreport{linear-alias,
690+ title = {Linear types for aliased resources},
691+ author = {Chris Hawblitzel},
693+ institution = {Microsoft Research},
694+ number = {MSR-TR-2005-141}
697+@article{kobayashi-esop,
698+ title = {Type-Based Analysis of Deadlock fora Concurrent Calculus with Interrupts},
699+ author = {Kohei Suenaga and Naoki Kobayashi},
704+@inproceedings{res-c,
705+ title = {A Path Sensitive Type System for Resource Usage Verification of C Like Languages},
706+ author = {Hyun-Goo Kang and Youil Kim and Taisook Han and Hwansoo Han},
708+ publisher = {Springer-Verlag},
709+ booktitle = {Programming Languages and Systems},
716+ title = {Lightweight static resources: Sexy types for embedded and systems programming},
717+ author = {Oleg Kiselyov and Chung-Chieh Shan},
722+@inproceedings{scoped-res,
723+ title = {Resource Usage Analysis Via Scoped Methods},
724+ author = {Gang Tan and Xinming Ou and David Walker},
725+ booktitle = {Foundations of Object-Oriented Languages},
729+@article{igarashi-res,
730+ author = {Igarashi, Atsushi and Kobayashi, Naoki},
731+ title = {Resource usage analysis},
732+ journal = {ACM Trans. Program. Lang. Syst.},
740+ url = {http://doi.acm.org/10.1145/1057387.1057390},
741+ doi = {http://doi.acm.org/10.1145/1057387.1057390},
744+ address = {New York, NY, USA},
745+ keywords = {Resource usage, type inference},
748+@phdthesis{monitoring,
749+ title = {Policy Enforcement via Program Monitoring},
750+ author = {Jarred Adam Ligatti},
755+@inproceedings{sec-policy,
756+ title = {A Type System for Expressive Security Policies},
757+ author = {David Walker},
758+ booktitle = {Twenty-Seventh {ACM} {SIGPLAN} Symposium on Principles of Programming Languages},
762+@inproceedings{res-dfa,
763+ author = {K. Marriott and P.J. Stuckey and M. Sulzmann},
764+ title = {Resource Usage Verification},
766+ booktitle = {In Proc. of First Asian Symposium, APLAS 2003},
768+ publisher = {Springer-Verlag}
771+@incollection{ hancock-interactive,
772+ author = "Peter Hancock and Anton Setzer",
773+ title = "Interactive Programs in Dependent Type Theory",
774+ booktitle = "Proc.\ of 14th Ann.\ Conf.\ of {EACSL}, {CSL}'00, Fischbau, Germany, 21--26 Aug 2000",
776+ publisher = "Springer-Verlag",
778+ editor = "P. Clote and H. Schwichtenberg",
781+ url = "citeseer.ist.psu.edu/hancock00interactive.html" }
783+@inproceedings{popeea-resources,
784+ author = {Corneliu Popeea and Wei-Ngan Chin},
785+ title = {A type system for resource protocol verification and its correctness proof},
786+ booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
788+ isbn = {1-58113-835-0},
790+ location = {Verona, Italy},
791+ doi = {http://doi.{ACM}.org/10.1145/1014007.1014021},
792+ publisher = {{ACM} Press},
793+ address = {New York, NY, USA},
796+@inproceedings{sheard-langfuture,
797+ author = {Tim Sheard},
798+ title = "Languages of the future",
799+ booktitle = "{ACM} Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA'04)",
804+ author = {Edwin Brady},
805+ title = {{Ivor}, a proof engine},
807+ publisher = {Springer-Verlag},
809+ booktitle = {Implementation and Application of Functional Languages 2006}
813+ author = {Bruno Barras and Benjamin Werner},
815+ title = {{Coq} in {Coq}}
819+ author = {Paul Hudak},
820+ title = {Building Domain-Specific Embedded Languages},
823+ journal = {{ACM} Computing Surveys},
828+@inproceedings{concon,
829+ author = {Conor McBride and Healfdene Goguen and James McKinna},
830+ title = {Some Constructions On Constructors},
832+ booktitle = {TYPES 2004},
833+ publisher = {Springer},
838+@InProceedings{Hume-GPCE,
839+author = {K. Hammond and G.J. Michaelson},
840+title = {{Hume: a Domain-Specific Language for Real-Time Embedded Systems}},
841+booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'03)}},
842+publisher = {Springer-Verlag},
843+series = {Lecture Notes in Computer Science},
847+@inproceedings{lcf-milner,
848+ author = {Robin Milner},
849+ title = {{LCF}: A Way of Doing Proofs with a Machine},
850+ booktitle = {Mathematical Foundations of Computer Science 1978},
858+@inproceedings{epireloaded,
859+ title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},
860+ author = {James Chapman and Thorsten Altenkirch and Conor McBride},
862+ booktitle = {Trends in Functional Programming 2005},
866+@TECHREPORT{why-tool,
867+ AUTHOR = {J.-C. Filli\^atre},
868+ TITLE = {{Why: a multi-language multi-prover verification tool}},
869+ INSTITUTION = {{LRI, Universit\'e Paris Sud}},
870+ TYPE = {{Research Report}},
874+ URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
877+@misc{ large-extraction,
878+ author = "Lu\'iz Cruz-Filipe and Bas Spitters",
879+ title = "Program Extraction from Large Proof Developments",
881+ url = "citeseer.ist.psu.edu/cruz-filipe03program.html" }
884+ author = "Herman Geuvers and Freek Wiedijk and Jan Zwanenburg",
885+ title = "A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals",
886+ booktitle = "{TYPES 2000}",
889+ url = "citeseer.ist.psu.edu/geuvers01constructive.html" }
891+@article{mckinna-expr,
892+ title = {A type-correct, stack-safe, provably correct, expression compiler in {Epigram}},
893+ author = {James McKinna and Joel Wright},
895+ journal = {Journal of Functional Programming},
900+ title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",
901+ author = "William Pugh",
902+ journal = "Communication of the {ACM}",
908+ author = "Georges Gonthier",
909+ title = "A computer-checked proof of the {Four Colour Theorem}",
911+ howpublished = {\url{http://research.microsoft.com/~gonthier/4colproof.pdf}}}
913+@inproceedings{sparkle,
914+ author = "Maarten {de Mol} and Marko {van Eekelen} and Rinus Plasmeijer",
915+ title = "Theorem Proving for Functional Programmers",
916+ url = "citeseer.ist.psu.edu/654423.html",
917+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2002)},
918+ publisher = {Springer},
926+ author = {Catarina Coquand},
927+ howpublished= {\url{http://agda.sourceforge.net/}},
932+ title = {Cover Translator},
933+ howpublished = {\url{http://coverproject.org/CoverTranslator/}}
937+ title = {Parsec, a fast combinator parser},
938+ author = {Daan Leijen},
940+ howpublished = {\url{http://www.cs.uu.nl/~daan/parsec.html}}
943+@inproceedings{dtpmsp-gpce,
944+ author = {Edwin Brady and Kevin Hammond},
945+ title = {A Verified Staged Interpreter is a Verified Compiler},
946+ booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'06)}},
951+ title = {Haddock: A {Haskell} Documentation Tool},
952+ howpublished = {\url{http://www.haskell.org/haddock/}}
955+@inproceedings{offshoring,
956+ title = {Implicitly Heterogeneous Multi-Stage Programming},
957+ author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},
958+ booktitle = {Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005)},
959+ publisher = {Springer},
966+ title = {Stop thinking about bottoms when writing programs},
967+ author = {Thorsten Altenkirch},
969+ note = {Talk at BCTCS 2006}
973+ title = {Partiality is an Effect},
974+ author = {Tarmo Uustalu},
976+ note = {Talk at Dagstuhl workshop on Dependently Typed Progamming}
979+@inproceedings{McKinnaPOPL06,
980+ author = {James McKinna},
981+ title = {Why dependent types matter},
982+ booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2006)},
986+ doi = {http://doi.{ACM}.org/10.1145/1111320.1111038},
990+@inproceedings{leroy-compiler,
991+ title = {Formal Certification of a Compiler Back-end},
992+ author = {Xavier Leroy},
994+ booktitle = {Principles of Programming Languages 2006},
996+ publisher = {{ACM} Press}
999+@inproceedings{hutton-exceptions,
1000+ title = {Compiling Exceptions Correctly},
1002+ author = {Graham Hutton and Joel Wright},
1003+ booktitle = {Mathematics of Program Construction},
1004+ publisher = {Springer},
1009+@inproceedings{tagless-staged,
1010+ title = {Tagless Staged Interpreters for Typed Languages},
1012+ booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},
1013+ author = {Emir Pa\v{s}al\'{i}c and Walid Taha and Tim Sheard},
1014+ publisher = {{ACM}}
1017+@inproceedings{env-classifiers,
1018+ title = {Environment Classifiers},
1020+ author = {Walid Taha},
1021+ booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2003)},
1025+@inproceedings{dsl-msp,
1026+ title = {{DSL} Implementation in {MetaOCaml}, {Template Haskell}, {and C++}},
1027+ booktitle = {Domain Specific Program Genearation 2004},
1028+ author = {Krzysztof Czarnecki and John O'Donnell and J\"{o}rg Striegnitz and Walid Taha},
1029+ publisher = {Springer},
1036+ author = {Tim Sheard and James Hook and Nathan Linger},
1037+ title = {{GADTs} + Extensible Kinds = Dependent Programming},
1039+ misc = {Submitted to {ICFP} '05}
1042+@INPROCEEDINGS{dt-framework,
1043+ TITLE = {A Dependently Typed Framework for Static Analysis of Program Execution Costs},
1045+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
1046+ AUTHOR = {Edwin Brady and Kevin Hammond},
1050+ PUBLISHER = {Springer}
1053+@INPROCEEDINGS{step-counting,
1054+ TITLE = {Accurate Step Counting},
1056+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
1057+ AUTHOR = {Catherine Hope and Graham Hutton},
1058+ PUBLISHER = {Springer}
1062+ author = {Walid Taha},
1063+ title = {{A Gentle Introduction to Multi-stage Programming}},
1065+ note = {Available from \url{http://www.cs.rice.edu/~taha}},
1066+ notnote = {Available from \url{http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf}}
1069+@misc{mckinnabrady-phase,
1070+ title = {Phase Distinctions in the Compilation of {Epigram}},
1072+ author = {James McKinna and Edwin Brady},
1076+@phdthesis{ brady-thesis,
1077+ author = {Edwin Brady},
1078+ title = {Practical Implementation of a Dependently Typed Functional Programming Language},
1080+ school = {University of Durham}
1083+@phdthesis{ taha-thesis,
1084+ author = {Walid Taha},
1085+ title = {Multi-stage Programming: Its Theory and Applications},
1087+ school = {Oregon Graduate Inst. of Science and Technology}
1090+@phdthesis{ pasalic-thesis,
1091+ author = {Emir Pa\v{s}al\'{i}c},
1092+ title = {The Role of Type-Equality in Meta-programming},
1094+ school = {OGI School of Science and Engineering}
1098+ author = {Thorsten Altenkirch and Conor McBride and James McKinna},
1099+ title = {Why Dependent Types Matter},
1104+@inproceedings { wadler-listless,
1105+ author = {Philip Wadler},
1106+ title = {Listlessness is better than laziness: {Lazy} evaluation and garbage collection at compile-time},
1107+ booktitle = {Proceedings of the 1984 {ACM} Symposium on LISP and functional programming},
1112+@techreport { gofer-impl,
1113+ author = {Mark P. Jones},
1114+ title = {The implementation of the Gofer functional programming system},
1117+ number = {YALEU/DCS/RR-1030},
1118+ institution = {Yale University}
1121+@techreport { pm-opt1,
1122+ author = {Kevin Scott and Norman Ramsey},
1123+ title = {When do match-compilation heuristics matter?},
1126+ number = {CS-2000-13},
1127+ institution = {Department of Computer Science, University of Virginia}
1130+@inproceedings{ pm-opt2,
1131+ author = "Fabrice Le Fessant and Luc Maranget",
1132+ title = "Optimizing Pattern Matching",
1133+ booktitle = "International Conference on Functional Programming",
1136+ url = "citeseer.ist.psu.edu/lefessant01optimizing.html" }
1138+@incollection{con-engine,
1139+ author = {G\'{e}rard Huet},
1140+ title = {The constructive engine},
1141+ booktitle = {A Perspective in Theoreticak Computer Science},
1142+ publisher = {World Scientific Publishing},
1144+ editor = {R. Narasimhan},
1145+ note = {Commemorative Volume for Gift Siromoney},
1149+@inproceedings{gadts,
1150+ title = {Simple unification-based type inference for {GADTs}},
1151+ author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
1153+ booktitle = {Proc. 2006 International Conf. on Functional Programming ({ICFP} 2006)}
1157+ author = {Simon {Peyton Jones} and Geoffrey Washburn and Stephanie Weirich},
1158+ title = {Wobbly types: type inference for generalised algebraic data types},
1160+ note = {Submitted to POPL 2005}
1164+ author = {Conor McBride},
1165+ title = {Epigram: Practical Programming with Dependent Types},
1167+ howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
1171+ author = {Per Martin-L\"{o}f},
1172+ title = "Intuitionistic Type Theory",
1174+ publisher = "Bibliopolis"
1177+@article{modular-fulllazy,
1178+ title = {A Modular Fully Lazy Lambda Lifter in {Haskell}},
1179+ author = {Simon {Peyton Jones} and David Lester},
1182+ journal = {Software Practice and Experience},
1188+@article{ghani-jay95,
1189+ author = {Barry Jay and Neil Ghani},
1190+ title = {The Virtues of Eta-Expansion},
1191+ journal = {Journal of Functional Programming},
1199+ author = {Lennart Augustsson},
1200+ title = {n+k patterns},
1202+ howpublished = {Message to the haskell mailing list, Mon, 17 May 93}
1205+@article{ danvy98functional,
1206+ author = "Olivier Danvy",
1207+ title = "Functional Unparsing",
1208+ journal = "Journal of Functional Programming",
1213+ url = "citeseer.ist.psu.edu/danvy98functional.html" }
1215+@inproceedings{SeveriPoll94,
1216+ author = {Paula Severi and Erik Poll},
1217+ booktitle = {Logical Foundations of Computing Science, LFCS'94},
1218+ editor = {A. Nerode and Yu. V. Matiyasevich},
1220+ pages = {316--328},
1221+ publisher = {Springer},
1223+ title = {{P}ure {T}ype {S}ystems with {D}efinitions},
1227+@inproceedings{coinductive,
1228+ title = {An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol},
1229+ booktitle = {Proceedings of the 1995 Workshop on Types for Proofs and Programs},
1234+ publisher = {Springer-Verlag},
1235+ author = {Eduardo Gim\'{e}nez}
1239+ author = "Joe Armstrong and Robert Virding and Claes Wikstr{\"o}m and Mike Williams",
1240+ title = "Concurrent Programming in Erlang",
1241+ edition = "Second",
1242+ publisher = "Prentice-Hall",
1244+ url = "citeseer.ist.psu.edu/armstrong93concurrent.html"
1247+@PhdThesis{alti:phd93,
1248+ author = "Thorsten Altenkirch",
1249+ title = "Constructions, Inductive Types and Strong Normalization",
1250+ school = "University of Edinburgh",
1252+ month = "November",
1255+@inproceedings{coq-modules,
1256+ author = "Jacek Chrzaszcz",
1257+ title = "Modules in {Coq} Are and Will Be Correct",
1259+ booktitle = {Types for Proofs and Programs 2003},
1260+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
1261+ publisher = {Springer},
1265+@inproceedings{comp-polymorphism,
1266+ author = "Robert Harper and Greg Morrisett",
1267+ title = "Compiling Polymorphism Using Intensional Type Analysis",
1269+ booktitle = "Proceedings of the 22nd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programming languages",
1270+ pages = "130 -- 141"
1273+@misc{runtime-loader,
1274+ author = "Andre Pang",
1275+ title = "{GHC} Runtime Loading",
1277+ howpublished = {Available from \verb+http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading+}
1280+@article{mccarthy-lisp,
1281+ author = "John McCarthy",
1282+ title = "Recursive Functions of Symbolic Expressions and Their Computation By Machine",
1284+ journal = "Communications of the {ACM}",
1291+ author = " David R. Musser and Atul Saini and Gillmer J. Derge",
1292+ title= "The {STL} Tutorial and Reference Guide: {C++} Programming with the Standard Template Library",
1294+ publisher = "Addison Wesley"
1297+@misc{ phase-distinction,
1298+ author = "Luca Cardelli",
1299+ title = "Phase Distinctions in Type Theory",
1300+ howpublished = "Manuscript",
1302+ url = "citeseer.ist.psu.edu/cardelli88phase.html" }
1304+@book {pierce-types,
1305+ author = "Benjamin C. Pierce",
1306+ title = "Type and Programming Languages",
1308+ publisher = "MIT Press"
1312+ Author = "Thierry Coquand and G\'{e}rard Huet",
1313+ title = "The calculus of constructions",
1315+ journal = "Information and Computation",
1320+@article{ miller91jlc,
1321+ Author = "Dale Miller",
1322+ Title = "A Logic Programming Language with Lambda-Abstraction,
1323+ Function Variables, and Simple Unification",
1324+ Journal = "Journal of Logic and Computation",
1329+ URL = "citeseer.ist.psu.edu/miller91logic.html",
1330+ URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" }
1332+@article{miller-unity,
1333+ author = "Dale Miller",
1334+ title = "Unification Under a Mixed Prefix",
1335+ journal = "Journal of Symbolic Computation",
1337+ pages = "321--358",
1341+@inproceedings{ cynthia,
1342+ author = "Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe",
1343+ title = "An {ML} Editor Based on Proofs-As-Programs",
1344+ booktitle = "Automated Software Engineering",
1347+ url = "citeseer.ist.psu.edu/whittle99ml.html" }
1351+ title={The Humble Programmer},
1352+ author={Edsger Dijkstra},
1354+ note={Turing Award Lecture, EWD 340}
1358+ title={Specifications for the {IBM} Mathematical FORmula TRANslating System, {FORTRAN}},
1359+ author={{IBM Applied Science Division}},
1365+@inproceedings{quickcheck,
1366+ title = {{QuickCheck}: A Lightweight Tool For Random Testing Of {Haskell} Programs},
1367+ author = {Koen Claessen and John Hughes},
1369+ booktitle = {International Conference on Functional Programming}
1372+@inproceedings{currylam,
1373+ title = {Functionality in Combinatory Logic},
1374+ author = {Haskell Curry},
1376+ booktitle = {Proc. Nat. Acad. Sci, USA},
1381+@article{churchsimplelam1,
1382+ title = {A set of postulates for the foundation of logic},
1383+ author = {Alonzo Church},
1385+ journal = {Annals of Mathematics},
1391+@article{churchsimplelam2,
1392+ title = {A set of postulates for the foundation of logic},
1393+ author = {Alonzo Church},
1395+ journal = {Annals of Mathematics},
1402+ title = {A Formulation of the Simple Theory of Types},
1403+ author = {Alonzo Church},
1405+ journal = {Journal of Symbolic Logic},
1411+ title = {Concepts in Programming Languages},
1412+ author = {John C. Mitchell},
1414+ publisher = {Cambridge University Press}
1417+@inproceedings{harrison-hol99,
1418+ title = {A Machine-Checked Theory of Floating Point Arithmetic},
1420+ booktitle = {Theorem Proving in Higher Order Logics: 12th International Conference, TP},
1421+ pages = {113--130},
1422+ author = {John Harrison},
1427+ title = {C--: A portable assembly language},
1429+ booktitle = {Workshop on Implementing Functional Languages, St Andrews},
1430+ author = {Simon {Peyton Jones} and Thomas Nordin and Dino Oliva},
1431+ crossref = {func-imp97}
1434+@proceedings{func-imp97,
1435+ title = {Workshop on Implementing Functional Languages, St Andrews},
1437+ editor = {C Clack},
1438+ publisher = {Springer-Verlag}
1443+ title = {Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99},
1445+ editor = {Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and Christine Paul},
1446+ publisher = {Springer-Verlag},
1447+ address = {Nice, France},
1452+ title = {Mathematical Logic and Programming Languages},
1454+ editor = {C.A.R. Hoare and J.C. Shepherdson},
1455+ publisher = {Prentice-Hall}
1459+ title = {Selected Papers on Automath},
1461+ editor = {S. Abramsky and J. Barwise and K. Fine and H.J. Keisler and A.S. Troelstr},
1462+ publisher = {North-Holland}
1466+ howpublished = {http://www.mersenne.org/prime.htm},
1467+ title = {Great Internet Mersenne Prime Search}
1470+@misc{haskell-report,
1471+ title = {Haskell 98 Language and Libraries --- The Revised Report},
1473+ month = {December},
1474+ author = {Simon {Peyton Jones} and others},
1475+ howpublished = {Available from \verb+http://www.haskell.org/+}
1478+@inproceedings{cayenne-{ICFP},
1479+ author = "Lennart Augustsson",
1480+ title = "Cayenne - a Language with Dependent Types",
1481+ booktitle = "Proc. 1998 International Conf. on Functional Programming ({ICFP} '98)",
1482+ pages = "239--250",
1484+ url = "citeseer.nj.nec.com/augustsson98cayenne.html"
1488+@misc{equality-cayenne,
1489+ howpublished = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
1490+ title = {Equality Proofs in Cayenne},
1492+ author = {Lennart Augustsson}
1495+@misc{interp-cayenne,
1496+ title = {An exercise in dependent types: A well-typed interpreter},
1498+ author = {Lennart Augustsson and Magnus Carlsson}
1501+@inproceedings{balaa00fixpoint,
1502+ title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
1504+ booktitle = {Theorem Proving in Higher Order Logics},
1506+ author = {Antonia Balaa and Yves Bertot}
1509+@inproceedings{isabelle-maple,
1510+ title = {Theorems and algorithms: An interface between Isabelle and Maple},
1512+ booktitle = {International Symposium on Symbolic and Algebraic Computation},
1513+ author = {Ballarin, C. and Homann, K., and Calmet, J.}
1516+@book{barendregt-num,
1517+ title = {The Lambda Calculus, Its Syntax and Semantics},
1519+ publisher = {North-Holland},
1520+ author = {Henk Barendregt}
1524+ title = {Recreations in the Theory of Numbers},
1526+ publisher = {Dover},
1527+ author = {Albert H. Beiler}
1530+@article{multidigit,
1531+ journal = {Advances in Applied Mathematics},
1532+ title = {Multidigit Multiplication for Mathematicians},
1534+ author = {Daniel J. Bernstein}
1537+@article{buhler-fox,
1538+ journal = {{ACM} Crossroads 2.1.},
1539+ month = {September},
1540+ title = {The Fox project: A language-structured approach to networking software.},
1542+ author = {Buhler, J.},
1543+ note = {Available at http://www.{ACM}.org/crossroads/xrds2-1/foxnet.html}
1546+@techreport{burstall91,
1547+ title = {Computer Assisted Proof for Mathematics: an Introduction Using the \textsc{Lego} Proof System},
1549+ institution = {University of Edinburgh},
1550+ author = {Rod Burstall}
1554+ title = {An Implementation of {LF} with Coercive Subtyping and Universes},
1555+ author = {Paul Callaghan and Zhaohui Luo},
1556+ journal = {Journal of Automated Reasoning},
1564+ title = {Coercive subtyping},
1565+ author = {Zhaohui Luo},
1566+ journal = {J. Logic Comput.},
1573+@inproceedings{calmet-homann,
1574+ title = {Classification of communication and cooperation mechanisms for logical and symbolic computation systems},
1576+ booktitle = {Proceedings of the First International Workshop 'Frontiers of Combining S},
1578+ publisher = {Kluwer},
1579+ author = {J. Calmet and K. Homann}
1582+@techreport{comm-proofs,
1583+ title = {On Communicating Proofs in Interactive Mathematical Documents},
1585+ institution = {Eindhoven University of Technology},
1586+ author = {Olga Caprotti and Martijn Oostdijk}
1590+ title = {How to formally and efficiently prove Prime(2999)},
1592+ author = {Olga Caprotti and Martijn Oostdijk},
1593+ journal = {Symbolic Computation and Automated Reasoning},
1598+ title = {The Calculi of Lambda-Conversion},
1600+ publisher = {Princeton University Press},
1601+ author = {Alonzo Church}
1605+ title = {Implementing Mathematics with the NuPrl Proof Development System},
1607+ publisher = {Prentice-Hall},
1609+ author = {Constable, Robert L. and others}
1613+ title = {On Numbers and Games},
1615+ publisher = {Academic Press},
1616+ author = {J.H. Conway}
1620+ howpublished = {\verb+http://coq.inria.fr/+},
1621+ title = {The {Coq} Proof Assistant --- Reference Manual},
1623+ author = {{Coq Development Team}}
1628+ title = {Type Theory and Programming},
1630+ author = {Thierry Coquand and Bengt Nordstr\"{o}m and Jan M. Smith and Bj\"{o}rn von Sydow}
1634+ title = {The Functional Approach to Programming},
1636+ publisher = {Cambridge University Press},
1637+ author = {Guy Cousineau and Michel Mauny}
1641+ howpublished = {http://www2.hursley.ibm.com/decimal/},
1643+ title = {Standard Decimal Arithmetic Specification},
1645+ author = {Mike Cowlishaw},
1646+ note = {\copyright IBM Corporation 2001}
1650+ title = {Elements of Intuitionism},
1653+ publisher = {Oxford: Clarendon},
1654+ author = {Michael A.E. Dummet}
1658+ title = {Inductive Families},
1660+ author = {Peter Dybjer},
1661+ journal = {Formal Aspects Of Computing},
1667+ howpublished = {http://www.octave.org/},
1668+ month = {February},
1669+ title = {GNU Octave -- A high-level interactive language for numerical computations},
1671+ author = {John W. Eaton}
1675+ title = {Computing methods for scientists and engineers},
1677+ publisher = {Oxford : Clarendon Press},
1678+ author = {L. Fox and D.F. Mayers}
1682+ howpublished = {http://www.gnu.org/software/guile/guile.html},
1683+ title = {Guile -- Project GNU's extension language},
1685+ author = {{Free Software Foundation}}
1689+ journal = {Journal of Functional Programming},
1692+ title = {Do we need dependent types?},
1695+ author = {Daniel Fridlender and Mia Indrika}
1698+@book{primes-programming,
1699+ title = {Primes and Programming -- An Introduction to Number Theory with Computing},
1701+ publisher = {Cambridge University Press},
1702+ author = {Peter Giblin}
1707+ title = {A Tutorial on Recursive Types in \textsc{Coq}},
1709+ author = {Eduardo Gim\'{e}nez}
1712+@article{goldberg91,
1713+ journal = {{ACM} Computing Surveys},
1716+ title = {What every computer scientist should know about floating point arithmetic},
1719+ author = {D. Goldberg}
1722+@article{binary-lambda,
1723+ journal = {Journal of Functional Programming},
1726+ title = {An adequate and efficient left associated binary numeral system in the $\lambda$-calculus},
1728+ author = {Mayer Goldberg}
1732+ title = {Introduction to HOL},
1734+ publisher = {Cambridge University Press},
1735+ author = {M. Gordon and T. Melham}
1739+ howpublished = {Available from \verb+http://www.swox.com/gmp/manual/+},
1740+ title = {The {GNU Multiple Precision} Arithmetic Library 4.1.3 --- Manual},
1742+ author = {Torbj\"{o}rn Granlund and others}
1745+@article{harrison-fmsd94,
1746+ journal = {Formal Methods in System Design},
1748+ title = {Constructing the Real Numbers in {HOL}},
1751+ author = {John Harrison}
1754+@book{harrison-thesis,
1755+ title = {Theorem Proving with the Real Numbers},
1757+ publisher = {Springer-Verlag},
1758+ author = {John Harrison}
1761+@techreport{hol-maple,
1762+ title = {Reasing about the Reals: the marriage of HOL and Maple},
1764+ institution = {University of Cambridge Computer Laboratory},
1765+ author = {John Harrison and Laurent Th\'{e}ry}
1769+ howpublished = {http://pauillac.inria.fr/coq},
1770+ title = {The \textsc{Coq} Proof Assistant - A Tutorial},
1771+ author = {G\'{e}rard Huet and Gilles Kahn and Christine Paulin-Mohring}
1774+@misc{restr-haskell,
1775+ howpublished = {http://citeseer.nj.nec.com/253599.html},
1776+ month = {September},
1777+ title = {Restricted Data Types in Haskell},
1779+ author = {John Hughes}
1783+ howpublished = {http://www2.hursley.ibm.com/decimalj/decimald.html},
1784+ month = {September},
1785+ title = {Decimal Arithmetic for Java -- a Proposal},
1787+ author = {{IBM Corporation}}
1791+ title = {{IEEE} Standard for Binary Floating Point Arithmetic},
1793+ author = {{IEEE Standard 754}}
1797+ title = {IEEE Standard for Radix-Independent Floating-Point Arithmetic},
1799+ author = {{IEEE Standard 854}}
1802+@inproceedings{jon91,
1803+ title = {Completing the Rational and Metric Spaces in \textsc{Lego}},
1805+ booktitle = {Proceedings of the Second Workshop on Logical Frameworks},
1806+ author = {Claire Jones}
1809+@misc{ typinghaskell,
1810+ author = "Mark Jones",
1811+ title = "Typing {Haskell} in {Haskell}",
1812+ howpublished = "In Haskell Workshop, September 1999.",
1814+ url = "citeseer.ist.psu.edu/article/jones99typing.html" }
1817+ journal = {Soviet Physics-Doklady},
1819+ title = {Multiplication of multidigit numbers by automata},
1821+ pages = {595--596},
1822+ author = {A. Karatsuba and Y. Ofman}
1827+ title = {The Art of Computer Programming - Seminumerical Algorithms},
1829+ publisher = {Addison Wesley},
1830+ author = {Donald E. Knuth}
1834+ journal = {Communications of the {ACM}},
1838+ title = {The next 700 programming languages},
1840+ author = {P.J. Landin}
1843+@techreport{luo-spec,
1845+ title = {Program Specification and Data Refinement in Type Theory},
1847+ institution = {Department of Computer Science, University of Edinburgh},
1848+ author = {Zhaohui Luo}
1852+ school = {University of Edinburgh},
1853+ title = {An Extended Calculus Of Constructions},
1855+ author = {Zhaohui Luo}
1858+@techreport{lego-manual,
1859+ title = {\textsc{Lego} Proof Development System: User's Manual},
1861+ institution = {Department of Computer Science, University of Edinburgh},
1862+ author = {Zhaohui Luo and Robert Pollack}
1866+ title = {The {ALF} proof editor and its proof engine},
1868+ booktitle = {Formal Proceeding of the 1993 Workshop on Types for Proofs and Programs},
1869+ author = {Lena Magnusson and Bengt N\"{o}rdstrom}
1873+ howpublished = {http://www.haskell.org/happy/},
1874+ title = {Happy User Guide},
1876+ author = {Simon Marlow and Andy Gill}
1879+@inproceedings{generic-haskell,
1880+ title = {Generic Haskell, Specifically},
1881+ author = {Dave Clarke and Andres L\"{o}h},
1882+ editor = {Jeremy Gibbons and Johan Jeuring},
1883+ booktitle = {Proceedings of the IFIP TC2 Working Conference on Generic Programming},
1885+ publisher = {Kluwer Academic Publishers},
1890+ title = {Faking It -- Simulating Dependent Types in {Haskell}},
1892+ author = {Conor McBride},
1893+ journal = {Journal of Functional Programming},
1899+@misc{mcbride-inverting,
1900+ title = {Inverting Inductively Defined Relations in \textsc{Lego}},
1902+ author = {Conor McBride}
1905+@phdthesis{mcbride-thesis,
1907+ school = {University of Edinburgh},
1908+ title = {Dependently Typed Functional Programs and their proofs},
1910+ author = {Conor McBride}
1913+@article{mcbride-unification,
1914+ title = {First-Order Unification by Structural Recursion},
1916+ author = {Conor McBride},
1917+ journal = {Journal of Functional Programming},
1920+ pages = {1061--1075}
1923+@misc{mckinna-pollack,
1924+ howpublished = {Kluwer Academic Publishers},
1925+ title = {Some Lambda Calculus and Type Theory formalized},
1927+ author = {James McKinna and Robert Pollack}
1931+ title = {An Introduction to the Theory of Numbers},
1933+ publisher = {John Wiley and Sons},
1934+ author = {Ivan Niven and Herbert S. Zuckerman}
1938+ title = {Programming in Martin-L\"{o}f's Type Theory -- An Introduction},
1940+ publisher = {Oxford University Press},
1941+ author = {Bengt Nordstr\"{o}m and Kent Petersson and Jan M. Smith},
1942+ note = {Out of print. Available from http://www.cs.chalmers.se/Cs/Research/Logic}
1946+ title = {Purely Functional Data Structures},
1948+ publisher = {Cambridge University Press},
1949+ author = {Chris Okasaki}
1952+@book{arith-systems,
1953+ title = {Computer Arithmetic Systems},
1955+ publisher = {Prentice-Hall},
1956+ author = {Amos R. Omondi}
1960+ title = {The Implementation of Functional Programming Languages},
1962+ publisher = {Prentice-Hall},
1963+ author = {Simon {Peyton Jones}}
1967+ title = {Computational Numerical Methods},
1969+ publisher = {John Wiley and Sons},
1970+ author = {C. Phillips and B. Cornelius}
1974+ title = {The NAG Library: a beginner's guide},
1976+ publisher = {Oxford : Clarendon Press},
1977+ author = {Jen Phillips}
1981+ month = {September},
1982+ title = {How to Believe a Machine-Checked Proof},
1984+ author = {Robert Pollack}
1987+@phdthesis{pollack94,
1988+ school = {University of Edinburgh},
1989+ title = {The Theory of LEGO -- A Proof Checker for the Extended Calculus of Constructions},
1991+ author = {Robert Pollack}
1994+@inproceedings{intel-bug,
1997+ title = {Anatomy of the Pentium Bug},
1998+ publisher = {Springer-Verlag},
2001+ author = {V.R. Pratt}
2005+ title = {The Maple Handbook: Maple V Release 4},
2007+ publisher = {Springer},
2008+ author = {Darren Redfern}
2012+ title = {Applied Cryptography: protocols, algorithms and source code in C.},
2014+ publisher = {Wiley},
2015+ author = {Bruce Schneier}
2019+ journal = {Mathematical Structures in Computer Science},
2022+ title = {On lists and other abstract data types in the calculus of construction},
2025+ author = {Jonathan P. Seldin}
2029+ journal = {Annals of Pure and Applied Logic},
2033+ title = {On the proof theory of Coquand's calculus of constructions},
2036+ author = {Jonathan P. Seldin}
2040+ journal = {The Computer Journal},
2042+ title = {Towards a Formal Specification of Floating Point},
2045+ author = {B.A. Wichmann}
2049+ title = {Mathematica : a system for doing mathematics by computer},
2051+ publisher = {Addison Wesley},
2052+ author = {Stephen Wolfram}
2055+@inproceedings{xi-imp,
2056+author = "Hongwei Xi",
2057+title = {{Imperative Programming with Dependent Types}},
2058+booktitle = "Proceedings of 15th {IEEE} Symposium on Logic in Computer Science",
2061+address = "Santa Barbara",
2065+@phdthesis{xi-thesis,
2066+ month = {December},
2067+ school = {Department of Mathematical Sciences, Carnegie Mellon University},
2068+ title = {Dependent Types in Practical Programming},
2070+ author = {Hongwei Xi}
2075+author = {Hongwei Xi and Robert Harper},
2076+title = {A Dependently Typed Assembly Language},
2077+institution = {Computer Science and Engineering Department, Oregon Graduate Institute},
2079+number = {OGI-CSE-99-008},
2084+ month = {February},
2085+ title = {Comparison of three public-domain multiprecision libraries: BigNum, Gmp and Pari},
2087+ author = {Paul Zimmerman}
2091+ title = {Programming Perl},
2092+ author = {Larry Wall and Tom Christiansen and Jon Orwant},
2095+ publisher = {O'Reilly}
2099+ howpublished = {http://www.python.org/doc/current/tut/tut.html},
2101+ title = {Python Tutorial},
2103+ author = {Guido van {Rossum} and Fred L. {Drake, Jr}}
2107+ title = {The Language of First Order Logic},
2109+ publisher = {CSLI Lecture Notes},
2110+ author = {Jon Barwise and John Etchemendy}
2114+ title = {Haskell -- The Craft of Functional Programming},
2116+ publisher = {Addison Wesley},
2117+ author = {Simon Thompson}
2120+@inproceedings{coq-hol,
2121+ title = {A Comparative Study of Coq and HOL},
2123+ booktitle = {Theorem Proving in Higher Order Logics},
2125+ author = {Vincent Zammit}
2129+ month = {November},
2130+ title = {Correctly Rounded Binary-Decimal and Decimal-Binary Conversions},
2132+ author = {David M. Gay},
2133+ note = {AT&T Bell Laboratories, Numerical Analysis Manuscript 90-10}
2136+@article{hughes-matters,
2137+ journal = {Computer Journal},
2140+ title = {Why Functional Programming Matters},
2143+ author = {J. Hughes}
2146+@inproceedings{proofpointing,
2147+ title = {Proof by Pointing},
2149+ booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer So},
2150+ pages = {141--160},
2151+ editor = {M. Hagiya and J. C. Mitchell},
2152+ publisher = {Springer-Verlag},
2155+ address = {Sendai, Japan},
2156+ author = {Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry}
2159+@misc{inductive-coq,
2160+ month = {December},
2161+ title = {Inductive Definitions in the System Coq -- Rules and Properties},
2163+ author = {Christine Paulin-Mohring}
2168+ title = {Using de Bruijn Sequences to Index a 1 in a Computer Word},
2170+ author = {{Charles E. Leiserson} and {Harald Prokop} and {Keith H. Randall}}
2173+@inproceedings{proofchecking,
2174+ title = {A two-level approach towards lean proof-checking},
2176+ booktitle = {TYPES},
2178+ author = {G. Barthe and M.P.J. Ruys and H.P. Barendregt}
2181+@inproceedings{congruence,
2182+ title = {Congruence Types},
2186+ author = {Gilles Barthe and Herman Geuvers}
2189+@phdthesis{geuvers-thesis,
2190+ title = {Logic and Type Systems},
2191+ author = {Herman Geuvers},
2193+ school = {Katholieke Universiteit Nijmegen}
2196+@techreport{multiple-values,
2197+ title = {Multiple Values in {Standard ML}},
2200+ institution = {LFCS, Dept of Computer Science, University of Edinburgh},
2201+ author = {Kevin Mitchell}
2204+@inproceedings{oracle-checking,
2206+ title = {Oracle-Based Checking of Untrusted Software},
2208+ booktitle = {Proceedings of the 28th {ACM} Symposium on Principles of Programming Languages},
2209+ pages = {142--154},
2210+ author = {{George C. Necula} and {S.P. Rahul}}
2213+@article{adams93jfp,
2214+ journal = {Journal of Functional Programming},
2217+ title = {Efficient Sets -- A Balancing Act},
2219+ pages = {553--561},
2220+ author = {Stephen Adams}
2223+@inproceedings{hughes-sized,
2224+ title = {Proving the Correctness of Reactive Systems Using Sized Types},
2226+ booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programmin},
2227+ pages = {410--423},
2228+ author = {John Hughes and Lars Pareto and Amr Sabry}
2231+@inproceedings{whittle99ml,
2232+ title = {An {ML} Editor Based on Proofs-As-Programs},
2234+ booktitle = {Automated Software Engineering},
2235+ pages = {166--173},
2236+ author = {Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe}
2240+ title = {Elements of Functional Programming},
2242+ publisher = {Addison-Wesley},
2243+ author = {Chris Reade},
2244+ series = {International Computer Science Series}
2247+@incollection{ wadler-views,
2248+ author = "Philip Wadler",
2249+ title = "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction",
2250+ booktitle = "Proceedings, 14th Symposium on Principles of Programming Languages",
2251+ publisher = "Association for Computing Machinery",
2252+ editor = "Steve Munchnik",
2253+ pages = "307--312",
2255+ url = "citeseer.nj.nec.com/wadler87views.html" }
2257+@article{ coquand-checking,
2258+ author = "Thierry Coquand",
2259+ title = "An Algorithm for Type-Checking Dependent Types",
2260+ journal = "Science of Computer Programming",
2265+ url = "citeseer.nj.nec.com/coquand96algorithm.html" }
2268+ author = "Thierry Coquand",
2269+ title = "Pattern Matching with Dependent Types",
2271+ howpublished = "Available from \verb+http://www.cs.chalmers.se/~coquand/type.html+"
2274+@misc{pollack-records,
2276+ title = {Dependently Typed Records for Representing Mathematical Structure},
2278+ author = {Robert Pollack}
2281+@article{checking-betarte,
2282+ journal = {Journal of Functional Programming},
2286+ title = {Type checking dependent (record) types and subtyping},
2288+ pages = {137--166},
2289+ author = {Gustavo Betarte}
2294+ author = "Thomas Johnsson",
2295+ title = "Efficient Compilation of Lazy Evaluation",
2296+ booktitle = "Proceedings of the {{ACM}} {{SIGPLAN}}'84 Symposium on Compiler Con struction",
2297+ journal = "{SIGPLAN} Notices",
2301+ publisher = "{ACM} Press",
2304+ url = "citeseer.nj.nec.com/johnsson84efficient.html" }
2306+@misc{kamareddine01,
2307+ month = {February},
2308+ title = {Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems},
2310+ author = {Fairouz Kamareddine}
2314+ title = {Basic Proof Theory},
2316+ publisher = {Cambridge University Press},
2317+ author = {A.S. Troelstra and H. Schwichtenberg},
2318+ series = {Cambridge Tracts in Theoretical Computer Science}
2322+ title = {Integrating Normalization-by-Evaluation into a Staged Programming Language},
2324+ author = {Tim Sheard}
2327+@inproceedings{nbe2,
2328+ title = {Normalization by evaluation},
2330+ author = {Ulrich Berger and Matthias Eberl and Helmut Schwichtenberg},
2331+ booktitle = {Prospects for Hardware Foundations 1998},
2332+ pages = {117--137},
2339+ title = {Compiling for Run-time Code Generation},
2341+ author = {Frederick Smith and Dan Grossman and Greg Morrisett and Luke Hornof and Trevor J},
2342+ note = {Under consideration for J. Functional Programming}
2345+@phdthesis{fredsmith_thesis,
2347+ school = {Cornell University},
2348+ title = {Certified Run-time Code Generation},
2350+ author = {Frederick Smith}
2353+@inproceedings{xi_arraybounds,
2354+author = "Hongwei Xi and Frank Pfenning",
2355+title = {Eliminating Array Bound Checking through Dependent Types},
2356+booktitle = "Proceedings of {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation",
2359+address = "Montreal",
2363+@inproceedings{xi_deadcode,
2364+author = "Hongwei Xi",
2365+title = {Dead Code Elimination through Dependent Types},
2366+booktitle = "The First International Workshop on Practical Aspects of Declarative Languages",
2369+address = "San Antonio",
2374+ title = {Compilers --- Principles, Techniques and Tools},
2376+ publisher = {Addison-Wesley},
2377+ author = {Alfred Aho and Ravi Sethi and Jeffrey Ullman}
2381+ title = {Highlights from nhc: A space efficient {Haskell} Compiler},
2383+ author = "Niklas R{\"o}jemo",
2384+ booktitle = "Functional Programming Languages and Computer Architecture",
2390+ title = {SML/NJ Match Compiler Notes},
2392+ author = {William Aitken}
2395+@misc{mlmatch_sestoft,
2396+ title = {ML pattern match compilation and partial evaluation},
2398+ author = {Peter Sestoft}
2401+@inproceedings{compiledstrongreduction,
2402+ title = {A Compiled Implementation of Strong Reduction},
2404+ author = {Benjamin Gr\'{e}goire and Xavier Leroy},
2405+ booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},
2410+ howpublished = {http://www.dcs.gla.ac.uk/~meurig/TclHaskell/usermanual.html},
2412+ title = {TclHaskell - User Manual},
2414+ author = {Meurig Sage}
2418+@InProceedings{nbe-cat,
2419+ author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
2420+ title = "Categorical reconstruction of a reduction free
2421+ normalization proof",
2423+ booktitle = "Category Theory and Computer Science",
2424+ editor = {David Pitt and David E. Rydeheard and Peter Johnstone},
2430+@inproceedings{presburgerEFSM,
2431+ title = {A Comparison of Presburger Engines for EFSM Reachability},
2433+ booktitle = {Computer Aided Verification '98},
2434+ pages = {280--292},
2435+ author = {Thomas R. Shiple and James H. Kukula and Rajeev K. Ranjan}
2439+ title = {Type-Safe Cast},
2441+ author = {Stephanie Weirich}
2444+@phdthesis{grobauer-thesis,
2445+ school = {University of Aarhus},
2446+ title = {Topics in Semantics Based Program Manipulation},
2448+ author = {Bernd Grobauer}
2452+ title = {Computational Lambda Calculus and Monads},
2454+ author = {Eugenio Moggi}
2458+ title = {A proof of {GMP} square root},
2460+ journal = {Journal of Automated Reasoning},
2462+ pages = {225--252},
2463+ author = {Yves Bertot and Nicolas Magaud and Paul Zimmerman}
2467+ journal = {{ACM} Transactions on Programming Languages and Systems},
2471+ title = {From {System F} to Typed Assembly Language},
2473+ pages = {528--569},
2474+ author = {Greg Morrisett and David Walker and Karl Crary and Neal Glew}
2477+@techreport{nbe-rtcg,
2478+ month = {December},
2479+ title = {Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation},
2481+ institution = {BRICS},
2482+ author = {Vincent Balat and Oliver Danvy}
2485+@misc{yong-schemata,
2486+ howpublished = {http://www.dur.ac.uk/yong.luo/},
2487+ title = {A Methodology for Implementing Inductive Schemata},
2489+ author = {Yong Luo and Zhaohui Luo}
2492+@inproceedings{harper93,
2493+ title = {Explicit Polymorphism and CPS Conversion},
2495+ booktitle = {20th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
2496+ pages = {206--219},
2497+ publisher = {{ACM} Press, New York, NY, USA},
2498+ author = {Robert Harper and Mark Lillibridge}
2501+@techreport{backends,
2502+ month = {November},
2503+ title = {Functional Back-Ends within the Lambda-Sigma Calculus},
2505+ institution = {INRIA},
2506+ author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
2510+ title = {Implementing lazy functional languages on stock hardware -- the {Spineless Tagless G-machine}},
2512+ journal = {Journal of Functional Programming},
2515+ pages = {127--202},
2517+ author = {Simon {Peyton Jones}}
2521+ journal = {Indagationes Mathematicae},
2523+ title = {Lambda calculus notation with nameless dummies},
2525+ pages = {381--392},
2526+ author = {N.G. de Bruijn}
2531+ title = {PC Assembly Language},
2533+ publisher = {http://www.drpaulcarter.com/},
2534+ author = {Paul A. Carter}
2537+@inproceedings{poly99,
2538+ title = {Once Upon A Polymorphic Type},
2540+ booktitle = {26th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
2541+ publisher = {{ACM}},
2542+ author = {Keith Wansbrough and Simon {Peyton Jones}}
2546+ title = {Compiling Lazy Functional Languages: An introduction},
2548+ author = {Thomas Johnsson}
2551+@inproceedings{unboxed-fp,
2553+ title = {Unboxed Values as First Class Citizens in a Non-Strict Functional Language},
2555+ author = {Simon {Peyton Jones} and John Launchbury},
2556+ booktitle = {Functional Programming Languages and Computer Architecture (FPCA'91)},
2557+ crossref = {fplca91},
2561+@inproceedings{abc-machine,
2562+ author = {Sjaak Smetsers and Eric N{\"{o}}cker and John {van Groningen} and Rinus Plasmeijer},
2563+ title = {Generating efficient code for lazy functional languages},
2564+ booktitle = {Functional programming Languages and Computer Architecture},
2566+ pages = {592--617},
2567+ crossref = {fplca91}
2570+@proceedings{fplca91,
2571+ title = {Functional programming Languages and Computer Architecture},
2575+ publisher = {Springer-Verlag},
2576+ editor = {John Hughes}
2582+ title = {An inverse of the evaluation functional for typed $\lambda$-calculus},
2584+ booktitle = {Proc. 1991 {IEEE} Symp. on Logic in Comp. Sci.},
2585+ pages = {203--211},
2586+ editor = {R. Vemuri},
2587+ author = {Ulrich Berger and Helmut Schwichtenberg}
2590+@inproceedings{typed-closure,
2591+ title = {Typed Closure Conversion},
2593+ booktitle = {Symposium on Principles of Programming Languages},
2594+ pages = {271--283},
2595+ author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper}
2598+@misc{ghc-commentary,
2599+ howpublished = {http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/},
2600+ title = {The Glasgow Haskell Compiler (GHC) Commentary},
2602+ author = {Manuel M. T. Chakravarty and Sigbjorn Finne and Simon Marlow and Simon {Peyton Jones} and Julian Seward and Reuben Thomas},
2603+ note = {Available from GHC CVS repository}
2606+@inproceedings{lambdalift,
2607+ month = {September},
2608+ title = {Lambda Lifting: Transforming Programs to Recursive Equations},
2610+ booktitle = {Functional Programming Languages and Computer Architecture},
2611+ pages = {190--203},
2612+ editor = {Jean-Pierre Jouannaud},
2613+ publisher = {Springer-Verlag},
2614+ author = {Thomas Johnsson}
2618+ title = {TIL: A Type-Directed Optimizing Compiler for ML},
2620+ booktitle = {Proc. {{ACM}} {{SIGPLAN}} '96 Conference on Programming Language Design and Implementation},
2621+ pages = {181--192},
2622+ author = {D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee}
2626+ school = {Princeton University},
2627+ title = {Compiling Standard {ML} for Efficient Execution on Modern Machines},
2629+ author = {Zhong Shao}
2632+@inproceedings{gmachine,
2633+ month = {September},
2634+ title = {The {G-Machine}: A fast, graph-reduction evaluator},
2636+ booktitle = {Functional Programming Languages and Computer Architecture},
2637+ pages = {400--413},
2638+ editor = {Jean-Pierre Jouannaud},
2639+ publisher = {Springer-Verlag},
2640+ author = {R.B. Kieburtz}
2643+@inproceedings{strictness,
2644+ month = {September},
2645+ title = {Strictness Analysis - A practical approach},
2647+ booktitle = {Functional Programming Languages and Computer Hardware},
2649+ editor = {Jean-Pierre Jouannaud},
2650+ publisher = {Springer-Verlag},
2651+ author = {Chris Clack and Simon {Peyton Jones}}
2655+ title = {Implementing Functional Languages - A Tutorial},
2657+ publisher = {Prentice Hall International},
2658+ author = {Simon {Peyton Jones} and David Lester}
2661+@phdthesis{capretta-thesis,
2662+ school = {Katholieke Universiteit Nijmegen},
2663+ title = {Abstraction and Computation},
2665+ author = {Venanzio Capretta}
2668+@article{bird-pointer,
2669+ journal = {Journal of Functional Programming},
2673+ title = {Unfolding Pointer Algorithms},
2675+ pages = {347--358},
2676+ author = {Richard S. Bird}
2680+ journal = {Journal of Functional Programming},
2684+ title = {Implementing Theorem Provers in a Purely Functional Style},
2686+ pages = {147--166},
2687+ author = {Keith Hanna}
2690+@article{shrink-lambda,
2691+ journal = {Journal of Functional Programming},
2693+ month = {September},
2695+ title = {Shrinking Lambda Expressions in Linear Time},
2697+ pages = {515--540},
2698+ author = {Andrew W. Appel and Trevor Jim}
2702+ journal = {Journal of Functional Programming},
2706+ title = {Stack-based Typed Assembly Language},
2709+ author = {Greg Morrisset and Karl Crart and Neal Glew and David Walker}
2712+@article{runtime-lamsig,
2713+ journal = {Journal of Functional Programming},
2717+ title = {Functional Runtime Systems within the lambda-sigma Calculus},
2719+ pages = {131--176},
2720+ author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
2724+ journal = {Journal of Functional Programming},
2726+ month = {November},
2728+ title = {How to look busy while being as lazy as ever: the Implementation of a lazy functional debugger},
2730+ pages = {629--671},
2731+ author = {Henrik Nilsson}
2734+@article{lazyveager,
2735+ journal = {Journal of Functional Programming},
2737+ month = {September},
2739+ title = {More haste, less speed: lazy versus eager evaluation},
2741+ pages = {541--547},
2742+ author = {Richard Bird and Geraint Jones and Oege {de Moor}}
2746+ journal = {Journal of Functional Programming},
2748+ month = {November},
2750+ title = {Compiling lazy functional programs for the Java Virtual Machine},
2752+ pages = {579--603},
2753+ author = {David Wakeling}
2757+ publisher = {Springer-Verlag},
2761+ title = {Isabelle/HOL - A proof assistant for higher order logic},
2763+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}
2766+@article{ghc-inliner,
2767+ journal = {Journal of Functional Programming},
2769+ month = {September},
2771+ title = {Secrets of the {Glasgow Haskell Compiler} inliner},
2773+ pages = {393--434},
2774+ author = {Simon {Peyton Jones} and Simon Marlow}
2777+@article{dynamic-fp,
2778+ journal = {Journal of Functional Programming},
2782+ title = {The dynamic compiliation of lazy functional programs},
2785+ author = {David Wakeling}
2790+ title = {Isabelle Reference Manual},
2792+ author = {Lawrence C. Paulson}
2795+@article{debruijn-nested,
2796+ journal = {Journal of Functional Programming},
2800+ title = {de Bruijn notation as a nested datatype},
2803+ author = {Richard S. Bird and Ross Paterson}
2806+@article{perfect-trees,
2807+ journal = {Journal of Functional Programming},
2811+ title = {Perfect trees and bit-reversal permutations},
2813+ pages = {305--317},
2814+ author = {Ralf Hinze}
2817+@phdthesis{paulin-extraction,
2818+ school = {Paris 7},
2819+ title = {Extraction de programmes dans le Calcul des Constructions},
2821+ author = {Christine Paulin-Mohring}
2824+@phdthesis{santos95,
2825+ school = {University of Glasgow},
2826+ title = {Compilation By Transformation In Non-Strict Functional Languages},
2828+ author = {{Andr\'{e} Lu\'{i}s de Medeiros} Santos}
2832+ title = {Compiling With Continuations},
2834+ publisher = {Cambridge University Press},
2835+ author = {Andrew W. Appel}
2840+ title = {The {SKIM} microprogrammer's guide},
2842+ institution = {University of Cambridge},
2843+ author = {W.R. Stoye}
2847+ title = {An Overview of Burroughs {NORMA}},
2849+ author = {H. Richards}
2853+ title = {The Definition of Standard ML --- Revised},
2855+ publisher = {MIT Press},
2856+ author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}
2860+ title = {An intuitionistic theory of types},
2862+ author = {Per Martin-L\"{o}f}
2865+@phdthesis{girard-thesis,
2866+ school = {Universit\'{e} Paris VII},
2867+ title = {Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur},
2869+ author = {Jean-Yves Girard}
2872+@inproceedings{ml75,
2873+ title = {An intuitionistic theory of types: predicative part},
2875+ booktitle = {Logic Colloquium '73},
2876+ editor = {H. Rose and J.C. Shepherdson},
2877+ publisher = {North-Holland},
2878+ author = {Per Martin-L\"{o}f}
2881+@inproceedings{cpm90,
2882+ title = {Inductively defined types},
2884+ author = {Thierry Coquand and Christine Paulin-Mohring},
2887+ publusher = {Springer-Verlag}
2890+@phdthesis{fpcustom,
2892+ school = {Computer Lab, University of Cambridge},
2893+ title = {The Implementation of Functional Languages using Custom Hardware},
2895+ author = {W.R. Stoye}
2898+@phdthesis{hughesthesis,
2899+ month = {September},
2900+ school = {Programming Research Group, Oxford},
2901+ title = {The design and implementation of programming languages},
2903+ author = {John Hughes}
2908+ title = {{TIM} -- A simple lazy abstract machine to execute supercombinators},
2910+ booktitle = {Functional Programming Languages and Computer Architecture},
2911+ publisher = {Springer-Verlag},
2912+ author = {John Fairbairn and Stuart Wray},
2918+ title = {The {ABC} machine -- A Sequential Stack-based Abstract Machine For Graph Rewriting},
2920+ institution = {University of Nijmegen},
2921+ 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}
2924+@techreport{implicit,
2925+ title = {On Implicit Arguments},
2927+ institution = {Faculty of Science, University of Tokyo},
2928+ author = {Masami Hagiya and Yozo Toda}
2932+ title = {Denotational Semantics},
2934+ publisher = {Wm. C. Brown},
2935+ author = {David A. Schmidt}
2938+@inproceedings{lazyml,
2940+ title = {A compiler for {Lazy} {ML}},
2942+ booktitle = {Proceedings of the {{ACM}} Symposium on Lisp and Functional Programming},
2943+ pages = {218--227},
2944+ author = {Lennart Augustsson}
2947+@inproceedings{nu-g,
2948+ title = {Parallel graph reduction with the $\langle\nu,G\rangle$-machine},
2950+ booktitle = {Functional Programming Languages and Computer Architecture},
2951+ publisher = {{ACM} Press},
2952+ author = {Lennart Augustsson and Thomas Johnsson}
2956+ title = {The C programming language},
2958+ publisher = {Prentice-Hall},
2959+ author = {Brian W. Kernighan and Dennis M. Ritchie}
2963+ title = {C--: a portable assembly language that supports garbage collection},
2965+ author = {Simon {Peyton Jones} and Norman Ramsey and Fermin Reig},
2966+ note = {Invited talk at PPDP'99}
2970+ howpublished = {http://www.dur.ac.uk/CARG/epigram.html},
2971+ title = {Project Proposal: {Epigram}: Innovative Programming via Inductive Families},
2973+ author = {Zhaohui Luo and James McKinna and Paul Callaghan and Conor McBride}
2977+ title = {Playing by the Rules: Rewriting as a practical optimisation technique in {GHC}},
2979+ author = {Simon {Peyton Jones} and Andrew Tolmach and Tony Hoare}
2982+@UNPUBLISHED{implicit-pollack,
2983+ AUTHOR = {Robert Pollack},
2984+ TITLE = {Implicit Syntax},
2985+ NOTE = {Informal Proceedings of First Workshop on
2986+ Logical Frameworks, Antibes},
2992+@article{transform-haskell,
2993+ journal = {Science of Computer Programming},
2995+ title = {A transformation-based optimiser for {Haskell}},
2998+ author = {Simon {Peyton Jones} and Andr\'{e} L. M. Santos}
3001+@inproceedings{knuth-bendix,
3002+ title = {Simple Word Problems in Universal Algebras},
3004+ booktitle = {Computational Problems in Abstract Algebra},
3005+ pages = {263--298},
3006+ editor = {John Leech},
3007+ publisher = {Pergamon Press},
3008+ author = {Donald E. Knuth and Peter B. Bendix}
3011+@inproceedings{phantomfun,
3012+ title = {Fun With Phantom Types},
3013+ author = {Ralf Hinze},
3014+ pages = {245--262},
3016+ crossref = {funprogramming},
3017+ booktitle = {The Fun Of Programming},
3018+ publisher = {Palgrave}
3021+@book{funprogramming,
3023+ title = {The Fun Of Programming},
3025+ editor = {Jeremy Gibbons and Oege {de Moor}},
3026+ publisher = {Palgrave},
3027+ series = {Cornerstones of Computing}
3030+@inproceedings{anderson-proof,
3031+ title = {Representing Proof Transformations For Program Optimization},
3033+ booktitle = {International Conference On Automated Deduction},
3034+ publisher = {Springer Verlag},
3035+ author = {Penny Anderson}
3038+@phdthesis{daria-thesis,
3040+ school = {Institute of Informatics, Warsaw University},
3041+ title = {Termination of Rewriting in the Calculus of Constructions},
3043+ author = {Daria Walukiewicz-Chrzaszcz}
3046+@inproceedings{change-data,
3047+ title = {Changing Data Structures In Type Theory: A Study Of Natural Numbers},
3049+ booktitle = {Types For Proofs And Programs 2000},
3050+ pages = {181--196},
3051+ editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
3052+ publisher = {Springer},
3053+ author = {Nicolas Magaud and Yves Bertot}
3056+@phdthesis{nico-thesis,
3057+ title = {Changement de Representation des donn\'{e}es dans le Calcul de Constructions},
3058+ author = {Nicolas Magaud},
3061+ school = {Universit\'{e} de Nice - Sophia Antipolis}
3066+ title = {Design Patterns},
3068+ publisher = {Addison Wesley},
3069+ author = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides}
3074+ title = {The New {GHC}/{Hugs} Runtime System},
3076+ author = {Simon Marlow and Simon {Peyton Jones}}
3080+ month = {February},
3081+ title = {The {STG} runtime system (revised)},
3083+ author = {Simon {Peyton Jones} and Simon Marlow and Alastair Reid},
3084+ howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
3087+@inproceedings{optimistic,
3089+ title = {Optimistic Evaluation --- an adaptive evaluation strategy for non-strict programs},
3091+ author = {Robert Ennals and Simon {Peyton Jones}},
3092+ booktitle = {International Conference on Functional Programming},
3096+@phdthesis{ennals-thesis,
3097+ title = {Adaptive Evaluation of Non-Strict Programs},
3098+ author = {Robert Ennals},
3100+ month = {December},
3101+ school = {King's College, University of Cambridge}
3105+ journal = {{ACM} Computing Surveys},
3108+ title = {Garbage Collection of Linked Data Structures},
3110+ pages = {341--367},
3111+ author = {Jacques Cohen}
3115+ journal = {Communications of the {ACM}},
3119+ title = {List Processing In Real Time On A Serial Computer},
3121+ pages = {280--294},
3122+ author = {Henry G. {Baker Jr}}
3126+ month = {February},
3127+ title = {Modelling General Recursion in Type Theory},
3129+ note = {Under consideration for publication in Math. Struct. in Comp. Science. Draft, DCS, CTH --- INRIA, Sophia Antipolis, France},
3130+ author = {Ana Bove and Venanzio Capretta}
3134+ title = {Global Tagging Optimization by Type Inference},
3136+ author = {Fritz Henglein}
3141+ title = {The Cathedral And The Bazaar},
3143+ publisher = {O'Reilly},
3144+ author = {Eric Raymond}
3148+ title = {The Mythical Man-month: Essays on Software Engineering},
3150+ publisher = {Addison Wesley},
3151+ author = {Frederick P. Brooks}
3154+@inproceedings{evalpush,
3155+ title = {How to make a fast curry: push/enter vs eval/apply},
3157+ author = {Simon Marlow and Simon {Peyton Jones}},
3158+ booktitle = {International Conference on Functional Programming, Snowbird},
3162+@phdthesis{boquist-thesis,
3164+ school = {Chalmers University of Technology},
3165+ title = {Code Optimisation Techniques for Lazy Functional Languages},
3167+ author = {Urban Boquist}
3171+ title = {Formal Specification Of Programming Languages},
3173+ publisher = {Prentice-Hall},
3174+ author = {Frank G. Pagan}
3177+@inproceedings{elim-motive,
3178+ title = {Elimination With A Motive},
3180+ booktitle = {Types for Proofs and Programs},
3181+ pages = {197--216},
3182+ editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
3183+ publisher = {Springer},
3184+ author = {Conor McBride}
3188+ journal = {Information and Computation},
3192+ title = {Telescoping Mappings in Typed Lambda Calculus},
3194+ pages = {189--204},
3195+ author = {N.G. de Bruijn}
3199+ title = {Typechecking is undecidable when 'type' is a type},
3201+ author = {Mark B. Reinhold}
3205+ month = {September},
3206+ title = {An External Representation for the {GHC} Core Language},
3208+ author = {Andrew Tolmach and {The GHC Team}}
3211+@article{deforestation,
3212+ journal = {Theoretical Computer Science},
3214+ title = {Deforestation: Transforming programs to eliminate trees},
3216+ pages = {231--248},
3217+ author = {Philip Wadler}
3222+ title = {Architecture of the {Haskell} Execution Platform},
3224+ author = {Julian Seward and Simon Marlow and Andy Gill and Sigbjorn Finne and Simon {Peyton Jones} },
3225+ note = {Version 6},
3226+ howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
3229+@mastersthesis{wahlstedt-thesis,
3231+ school = {Chalmers University Of Technology},
3232+ title = {Detecting Termination Using Size Change In Parameter Values},
3234+ author = {David Wahlstedt}
3237+@inproceedings{size-change,
3238+ title = {The size-change principle for program termination},
3240+ booktitle = {Proceedings of the 28th Annual {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
3241+ author = {Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. }
3244+@article{ski-turner,
3245+ journal = {Software -- Practice and Experience},
3247+ title = {A new implementation technique for applicative languages},
3250+ author = {David Turner}
3253+@inproceedings{turner-strong,
3255+ title = {Elementary Strong Functional Programming},
3257+ booktitle = {First International Symposium on Functional Programming Languages in Education, Nijmegen, Netherlands, December 1995.},
3259+ publisher = {Springer},
3260+ author = {David Turner},
3265+ title = {The {Concurrent CLEAN} Language Report (draft)},
3267+ author = {Rinus Plasmeijer and Marko van Eekelen},
3268+ howpublished = {Available from \verb+http://www.cs.kun.nl/~clean/+}
3271+@article{burstall-struct,
3272+ journal = {Computer Journal},
3275+ title = {Proving Properties of Programs By Structural Induction},
3278+ author = {Rod Burstall}
3281+@incollection{ barendregt-types,
3282+ author = "Henk Barendregt",
3283+ title = "Lambda Calculi with Types",
3284+ booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky \& Gabbay \& Maibaum (Eds.)",
3285+ publisher = "Clarendon",
3288+ url = "citeseer.nj.nec.com/barendregt92lambda.html" }
3291+ title = {Combinatory Logic, volume 1},
3293+ publisher = {North Holland},
3294+ author = {Haskell B. Curry and Robert Feys}
3297+@phdthesis{bove-thesis,
3298+ month = {November},
3299+ school = {Chalmers University of Technology},
3300+ title = {General Recursion in Type Theory},
3302+ author = {Ana Bove}
3306+ title = {Constructive Mathematics and Computer Programming},
3308+ booktitle = {Mathematical Logic and Programming Languages},
3309+ publisher = {Prentice Hall},
3310+ author = {Per Martin-L\"{o}f}
3313+@inproceedings{howard,
3314+ title = {The formulae-as-types notion of construction},
3316+ booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
3317+ editor = {Jonathan P. Seldin and J. Roger Hindley},
3318+ publisher = {Academic Press},
3319+ author = {William A. Howard},
3320+ note = {A reprint of an unpublished manuscript from 1969}
3323+@inproceedings{talx86,
3324+ title = {TALx86: A Realistic Typed Assembly Language},
3326+ booktitle = {{ACM} {SIGPLAN} Workshop on Compiler Support for System Software},
3328+ 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}
3331+@inproceedings{bove-capretta,
3333+ title = {Nested General Recursion and Partiality in Type Theory},
3335+ booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLS 2001},
3336+ pages = {121--135},
3337+ editor = {Richard J. Boulton and Paul B. Jackson},
3338+ publisher = {Springer-Verlag},
3339+ author = {Ana Bove and Venanzio Capretta},
3344+ month = {November},
3345+ title = {LVM, the lazy virtual machine},
3347+ author = {Daan Leijen}
3351+ howpublished = {\verb+http://caml.inria.fr/ocaml/htmlman/+},
3353+ title = {The {Objective Caml} system release 3.06},
3355+ author = {Xavier Leroy}
3359+ title = {Lambda : The Ultimate Goto},
3361+ author = {Guy L. {Steele Jr}},
3362+ note = {MIT AI Memo 443}
3365+@inproceedings{ liu-tail,
3366+ author = "Yanhong A. Liu and Scott D. Stoller",
3367+ title = "From Recursion to Iteration: What are the Optimizations?",
3368+ booktitle = "Partial Evaluation and Semantic-Based Program Manipulation",
3371+ url = "citeseer.nj.nec.com/liu00from.html" }
3373+@inproceedings{aczel77,
3374+ title = {An Introduction To Inductive Definitions},
3376+ booktitle = {Handbook of Mathematical Logic},
3377+ editor = {J. Barwise},
3378+ publisher = {North Holland},
3379+ author = {Peter Aczel}
3382+@inproceedings{inductive-plastic,
3384+ title = {Implementation Techniques for Inductive Types in {Plastic}},
3386+ booktitle = {Types for Proofs and Programs},
3388+ editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith},
3389+ publisher = {Springer-Verlag},
3390+ author = {Paul Callaghan and Zhaohui Luo},
3395+ howpublished = {Available from \verb+http://www.paulgraham.com/+},
3397+ title = {The Hundred Year Language},
3399+ author = {Paul Graham},
3400+ note = {Keynote address at PyCon 2003}
3403+@inproceedings{gimenez98,
3405+ title = {Structural Recursive Definitions in Type Theory},
3407+ booktitle = {Proceedings of ICALP '98},
3408+ publisher = {Springer-Verlag},
3409+ author = {Eduardo Gim\'{e}nez},
3414+ journal = {Computer Journal},
3417+ title = {Quicksort},
3420+ author = {C.A.R. Hoare}
3423+@phdthesis{goguen-thesis,
3424+ school = {University of Edinburgh},
3425+ title = {A Typed Operational Semantics for Type Theory},
3427+ author = {Healfdene Goguen}
3430+@article{ph-universes,
3431+ journal = {Theoretical Computer Science},
3434+ title = {Type Checking With Universes},
3436+ pages = {107--136},
3437+ author = {Robert Harper and Randy Pollack}
3440+@inproceedings{pm-compile,
3441+ month = {September},
3442+ title = {Compiling Pattern Matching},
3444+ booktitle = {Functional Programming Languages and Computer Architecture},
3445+ pages = {368--381},
3446+ editor = {Jean-Pierre Jouannaud},
3447+ publisher = {Springer-Verlag},
3448+ author = {Lennart Augustsson}
3451+@phdthesis{lena-thesis,
3452+ school = {Chalmers University of Technology, G\"{o}teborg},
3453+ title = {The implementation of {ALF} -- A Proof Editor based on {Martin-L\"{o}f}'s Monomorphic Type Theory with Explicit Substitutions},
3455+ author = {Lena Magnusson}
3459+ journal = {Journal of Functional Programming},
3462+ title = {The View From The Left},
3464+ author = {Conor McBride and James McKinna},
3468+@inproceedings{not-a-number,
3469+ author = {Conor McBride and James McKinna},
3470+ title = {I am not a number, {I} am a free variable},
3472+ booktitle = {Proceedings of the {ACM} {SIGPLAN} Haskell Workshop}
3477+ title = {Time and Space Profiling for Non-Strict, Higher Order Functional Languages},
3479+ author = {Patrick M. Sansom and Simon {Peyton Jones}}
3482+@inbook{pattern-matching,
3483+ title = {The Implementation of Functional Programming Languages},
3485+ booktitle = {The Implementation of Functional Programming Languages},
3487+ editor = {Simon {Peyton Jones}},
3489+ publisher = {Prentice Hall},
3490+ author = {Philip Wadler},
3491+ crossref = {pj-imp}
3494+@article{pe-problems,
3495+ author = {Jones, N. D.},
3496+ title = {Challenging problems in partial evaluation and mixed computation},
3497+ journal = {New Gen. Comput.},
3501+ issn = {0288-3635},
3502+ pages = {291--302},
3503+ doi = {http://dx.doi.org/10.1007/BF03037143},
3504+ publisher = {Ohmsha},
3505+ address = {Tokyo, Japan, Japan},
3508+@inproceedings{tag-elim,
3509+ title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},
3511+ booktitle = {Subtyping and Dependent Types in Programming, APPSEM Workshop},
3512+ author = {Walid Taha and Henning Makholm}
3515+@inproceedings{extraction-coq,
3516+ title = {A New Extraction for {Coq}},
3518+ booktitle = {Types for proofs and programs},
3519+ editor = {Herman Geuvers and Freek Wiedijk},
3520+ publisher = {Springer},
3521+ author = {Pierre Letouzey},
3525+@phdthesis{mcbride-snr-thesis,
3526+ school = {Queen's University of Belfast},
3527+ title = {Computer Aided Manipulation of Symbols},
3529+ author = {Fred McBride}
3532+@article{ho-strictness,
3533+ journal = {Science of Computer Programming},
3535+ title = {Strictness analysis for higher-order functions},
3537+ pages = {249--278},
3538+ author = { Geoffrey L. Burn and Chris Hankin and Samson Abramsky}
3541+@phdthesis{mycroft-thesis,
3542+ school = {Dept Computer Science, University of Edinburgh},
3543+ title = {Abstract interpretation and optimising transformations for applicative programs},
3545+ author = {A. Mycroft}
3548+@inproceedings{bc-nested,
3549+ month = {September},
3551+ title = {Nested General Recursion and Partiality in Type Theory},
3553+ booktitle = {Theorem Proving In Higher Order Logics: 14th International Conferences, TPHOLS 2001},
3554+ pages = {121--135},
3555+ publisher = {Springer--Verlag},
3556+ author = {Ana Bove and Venanzio Capretta},
3560+@techreport{bove-mutual,
3562+ title = {Mutual General Recursion in Type Theory},
3564+ institution = {Department of Computing Science, Chalmers University of Technology},
3565+ author = {Ana Bove}
3568+@article{berardi-pruning,
3569+ journal = {Journal of Logic and Computation},
3572+ title = {Pruning Simply Typed Lambda Terms},
3574+ pages = {663--681},
3575+ author = {Stefano Berardi}
3579+ journal = {Journal of Computer and System Science},
3581+ title = {A Theory of Type Polymorphism in Programming},
3584+ author = {R. Milner}
3587+@inproceedings{extt,
3588+ title = {Inductive Families Need Not Store Their Indices},
3590+ booktitle = {Types for Proofs and Programs 2003},
3591+ author = {Edwin Brady and Conor McBride and James McKinna},
3592+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
3593+ series = {Lecture Notes in Computer Science},
3594+ publisher = {Springer},
3600+ title = {Computation and Reasoning -- A Type Theory for Computer Science},
3603+ author = {Zhaohui Luo},
3604+ series = {Intl. Series of Monographs on Comp. Sci.}
3608+ journal = {Communications of the {ACM}},
3611+ title = {Can Programming Be Liberated From the {Von Neumann} Style?},
3613+ pages = {280--294},
3614+ author = {John Backus}
3619+ title = {Henk: A Typed Intermediate Language},
3621+ author = {Simon {Peyton Jones} and Erik Meijer}
3625+ journal = {Journal of Functional Programming},
3629+ title = {Thunks and the $\lambda$-calculus},
3631+ pages = {303--319},
3632+ author = {John Hatcliff and Olivier Danvy}
3635+@inproceedings{grin-project,
3636+ author = "Urban Boquist and Thomas Johnsson",
3637+ title = "The {GRIN} Project: A Highly Optimising Back End for Lazy Functional Languages",
3638+ booktitle = "Implementation of Functional Languages",
3641+ url = "citeseer.ist.psu.edu/boquist96grin.html" }
3644+ nothowpublished = {\url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}},
3645+ title = {A garbage collector for {C} and {C++}},
3647+ author = {Hans-J. Boehm and Alan J. Demers and {Xerox Corporation Silicon Graphic} and {Hewlett-Packard Company}}
3650+@misc{art-interpreter,
3652+ title = {The Art of the Interpreter or, the Modularity Complex (Parts Zero, One, and Two)},
3654+ author = {Guy Lewis {Steele, Jr.} and Gerald Jay Sussman},
3655+ note = {MIT AI Lab. AI Lab Memo AIM-453}
3658+@inproceedings{gimenez,
3659+ title = {Codifying Guarded Definitions With Recursive Schemes},
3661+ booktitle = {Proceedings of TYPES 1994},
3663+ author = {Eduardo Gim\'{e}nez}
3667+ title = {The Glasgow Haskell Compiler User's Guide, Version 6.0},
3669+ author = {The {GHC Team}}
3673+ journal = {Journal of Functional Programming},
3677+ title = {Red-Black Trees In A Functional Setting},
3679+ pages = {471--477},
3680+ author = {Chris Okasaki}
3683+@inproceedings{dt-data,
3684+author = "Hongwei Xi",
3685+title = {{Dependently Typed Data Structures}},
3686+booktitle = "Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99)",
3688+month = "September",
3694+ title = {On the Correctness and Efficiency of the {Krivine} Machine},
3697+ author = {Mitchell Wand and Daniel P. Friedman},
3698+ howpublished = {Submitted for publication}
3701+@inproceedings{nbe-filinski,
3702+ title = {Normalization by Evaluation for the Computational Lambda-Calculus},
3705+ booktitle = {Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001},
3706+ author = {Andrzej Filinski},
3707+ pages = {151--165},
3708+ publisher = {Springer-Verlag},
3713+@inproceedings{filinski-nbesem,
3714+ title = {A semantic account of type-directed partial evaluation},
3716+ author = {Andrzej Filinski},
3717+ editor = {G. Nadathur},
3718+ booktitle = {International Conference on Principles and Practice of Declarative Programming},
3721+ pages = {378--395},
3722+ publisher = {Springer-Verlag}
3726+ title = {The mechanical evaluation of expressions},
3727+ author = {P.J. Landin},
3729+ journal = {Computer Journal},
3735+ title = {The {LispKit} Manual},
3736+ author = {Peter Henderson and Geraint Jones and Simon Jones},
3738+ howpublished = {Oxford University Computing Laboratory}
3741+@inproceedings{wells-undecidable,
3742+ title = {Typability and Type Checking in the Second-order $\lambda$-calculus are equivalent and undecidable},
3743+ author = {J. Wells},
3746+ booktitle = {Proc. 9th Ann. {IEEE} Symp. Logic Comput. Sci.}
3750+ title = {Pattern Guards and Transformational Patterns},
3751+ author = {Martin Erwig and Simon {Peyton Jones}},
3753+ howpublished = {Haskell Workshop}
3757+ title = {Alfa Users' Guide},
3758+ author = {Thomas Hallgren},
3760+ howpublished = {Available from \verb+http://www.cs.chalmers.se/~hallgren/Alfa/+}
3763+@inproceedings{nofib,
3764+ title = {The nofib Benchmark Suite of {Haskell} Programs},
3765+ author = {Will Partain},
3767+ booktitle = {Functional Programming},
3768+ editor = {J. Launchbury and P.L. Sansom},
3769+ series = {Workshops in Computing},
3770+ publisher = {Springer Verlag}
3774+ title = {Shape in Computing},
3775+ author = {Barry Jay},
3776+ journal = "{{ACM}} Computing Surveys",
3780+ pages = "355--357",
3784+ title = {The {Haskell 98} Foreign Function Interface 1.0: An Addendum to the {Haskell 98} Report},
3785+ editor = {Manuel Chakravarty},
3788+ month = {December},
3789+ howpublished = {Available from \verb+http://www.haskell.org/+}
3793+ title = {Perl {XS} Reference Manual},
3794+ author = {Dean Roehrich and {The Perl Porters}},
3796+ howpublished = {\verb+http://www.perldoc.com/perl5.6/pod/perlxs.html+}
3800+ title = {{SWIG} : An Easy to Use Tool for Integrating Scripting Languages with {C} and {C++}},
3801+ author = {David M. Beazley},
3803+ howpublished = {\verb+http://www.swig.org/papers/Tcl96/tcl96.html+}
3806+@inproceedings{types-prog,
3807+ title = {Type Systems for Programming Languages},
3808+ booktitle = {Handbook of Theoretical Computer Science},
3809+ author = {John C. Mitchell},
3810+ pages = {365--458},
3816+ title = {Handbook of Theoretical Computer Science},
3817+ editor = {J. van Leeuwen},
3818+ publisher = {Elsevier Science},
3823+ title = {Revised$^5$ Report on the Algorithmic Language Scheme},
3824+ author = {Richard Kelsey and William Clinger and Jonathan Rees},
3826+ month = {February},
3827+ howpublished = {Available from \verb+http://www.schemers.org/+}
3831+ title = {Update on today's {Gmail} Outage},
3832+ author = {{Official Gmail Blog}},
3833+ howpublished = {\url{http://gmailblog.blogspot.com/2009/02/update-on-todays-gmail-outage.html}},
3834+ note = {Retrieved 26th February 2009},