@@ -0,0 +1,3846 @@
1+@article{lambdapi,
2+ author = {Andres L\"{o}h and Conor McBride and Wouter Swierstra},
3+ title = {A tutorial implementation of a dependently typed lambda calculus},
4+ year = 2010,
5+ journal = {Fundamenta Informaticae},
6+ volume = 102,
7+ number = 2
8+}
9+
10+@article{idioms,
11+ author = {McBride, Conor and Paterson, Ross},
12+ title = {Applicative programming with effects},
13+ journal = {J. Funct. Program.},
14+ volume = {18},
15+ issue = {1},
16+ month = {January},
17+ year = {2008},
18+ issn = {0956-7968},
19+ pages = {1--13},
20+ numpages = {13},
21+ url = {http://portal.acm.org/citation.cfm?id=1348940.1348941},
22+ doi = {10.1017/S0956796807006326},
23+ acmid = {1348941},
24+ publisher = {Cambridge University Press},
25+ address = {New York, NY, USA},
26+}
27+
28+@inproceedings{lava,
29+ author = {Bjesse, Per and Claessen, Koen and Sheeran, Mary and Singh, Satnam},
30+ title = {Lava: hardware design in {Haskell}},
31+ booktitle = {Proceedings of the third ACM SIGPLAN international conference on Functional programming},
32+ series = {ICFP '98},
33+ year = {1998},
34+ isbn = {1-58113-024-4},
35+ location = {Baltimore, Maryland, United States},
36+ pages = {174--184},
37+ numpages = {11},
38+ url = {http://doi.acm.org/10.1145/289423.289440},
39+ doi = {http://doi.acm.org/10.1145/289423.289440},
40+ acmid = {289440},
41+ publisher = {ACM},
42+ address = {New York, NY, USA},
43+}
44+
45+@inproceedings{plpv11,
46+ author = {Edwin Brady},
47+ title = {Idris --- Systems programming meets full dependent types},
48+ booktitle = {Programming Languages meets Program Verification {(PLPV 2011)}},
49+ year = {2011},
50+ pages = {43--54},
51+ ee = {http://doi.acm.org/10.1145/1929529.1929536},
52+ bibsource = {DBLP, http://dblp.uni-trier.de}
53+}
54+
55+@inproceedings{epic-tfp,
56+ author = {Edwin Brady},
57+ title = {Epic --- a library for generating compilers},
58+ year = 2011,
59+ booktitle = {{Trends in Functional Programming} ({TFP} '11)},
60+ note = {To appear}
61+}
62+
63+@inproceedings{ynot08,
64+ author = {Nanevski,, Aleksandar and Morrisett,, Greg and
65+ Shinnar,, Avraham and Govereau,, Paul and Birkedal,,
66+ Lars},
67+ title = {Ynot: reasoning with the awkward squad},
68+ booktitle = {{ICFP} '08: Proceeding of the 13th {ACM SIGPLAN}
69+ international conference on Functional programming},
70+ year = {2008},
71+ isbn = {978-1-59593-919-7},
72+ pages = {229--240},
73+ location = {Victoria, BC, Canada},
74+ doi = {http://doi.acm.org/10.1145/1411204.1411237},
75+ publisher = {ACM},
76+ address = {New York, NY, USA},
77+}
78+
79+@article{cbconc-fi,
80+ author = {Edwin Brady and Kevin Hammond},
81+ title = {Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage Protocols},
82+ year = 2010,
83+ journal = {Fundamenta Informaticae},
84+ volume = 102,
85+ number = 2,
86+ pages = {145--176}
87+}
88+
89+@inproceedings{devil-osdi00,
90+ author = {Fabrice M{\'e}rillon and
91+ Laurent R{\'e}veill{\`e}re and
92+ Charles Consel and
93+ Renaud Marlet and
94+ Gilles Muller},
95+ title = {Devil: An IDL for Hardware Programming},
96+ booktitle = {4th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2000)},
97+ year = {2000}
98+}
99+
100+
101+@INPROCEEDINGS{device-osdi08,
102+ author = {Dan Williams and Patrick Reynolds and Kevin Walsh and Emin Gün Sirer and Fred B. Schneider},
103+ title = {Device driver safety through a reference validation mechanism},
104+ booktitle = {8th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008)},
105+ year = {2008}
106+}
107+
108+@inproceedings{sozeau-equations,
109+ author = {Matthieu Sozeau},
110+ title = {Equations: A Dependent Pattern-Matching Compiler},
111+ booktitle = {First International Conference on Interactive Theorem Proving (ITP 2010)},
112+ year = {2010},
113+ pages = {419--434},
114+ ee = {http://dx.doi.org/10.1007/978-3-642-14052-5_29},
115+ crossref = {DBLP:conf/itp/2010},
116+ bibsource = {DBLP, http://dblp.uni-trier.de}
117+}
118+
119+
120+@inproceedings{packet-type,
121+ author = "Peter J. McCann and Satish Chandra",
122+ title = "Packet Types: Abstract Specification of Network Protocol Messages",
123+ year = 2000,
124+ booktitle = "SIGCOMM '00",
125+ publisher = {{ACM}}
126+}
127+
128+@inproceedings{qs-types,
129+ author = {Eelis {van der Weegen} and James McKinna},
130+
131+ title={A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq},
132+ year={2009},
133+ pages={256--271},
134+ series = {Lecture Notes in Computer Science},
135+ publisher = {Springer}
136+
137+}
138+
139+@inproceedings{totalparser,
140+ author = {Nils Anders Danielsson},
141+ title = {Total Parser Combinators},
142+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
143+ year = {2010},
144+ isbn = {978-1-60558-794-3},
145+ pages = {285--296},
146+ location = {Baltimore, Maryland, USA},
147+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},
148+ publisher = {{ACM}},
149+ address = {New York, NY, USA},
150+ }
151+
152+@misc{rfc791,
153+ author="J. Postel",
154+ title="{Internet Protocol}",
155+ series="Request for Comments",
156+ number="791",
157+ howpublished="RFC 791 (Standard)",
158+ publisher="IETF",
159+ organization="Internet Engineering Task Force",
160+ year=1981,
161+ month=sep,
162+ note="Updated by RFC 1349",
163+ url="http://www.ietf.org/rfc/rfc791.txt",
164+}
165+
166+
167+@misc{rfc792,
168+ author="J. Postel",
169+ title="{Internet Control Message Protocol}",
170+ series="Request for Comments",
171+ number="792",
172+ howpublished="RFC 792 (Standard)",
173+ publisher="IETF",
174+ organization="Internet Engineering Task Force",
175+ year=1981,
176+ month=sep,
177+ note="Updated by RFCs 950, 4884",
178+ url="http://www.ietf.org/rfc/rfc792.txt",
179+}
180+
181+@INPROCEEDINGS{Dybjer-indrec,
182+ author = {Peter Dybjer and Anton Setzer},
183+ title = {A Finite Axiomatization of Inductive-Recursive Definitions},
184+ booktitle = {Tyed Lambda Calculi and Applications},
185+ volume = {1581},
186+ series = {Lecture Notes in Computer Science},
187+ year = {1998},
188+ pages = {129--146},
189+ publisher = {Springer}
190+}
191+
192+@book{stevenstcpip,
193+ author = {W. Richard Stevens},
194+ title = {{TCP/IP} Illustrated Volume 1: The Protocols},
195+ year = 1994,
196+ publisher = {Addison Wesley},
197+ isbn = {0-201-63346-9}
198+}
199+
200+@inproceedings{coqtypeclasses,
201+ author = {Sozeau, Matthieu and Oury, Nicolas},
202+ title = {First-Class Type Classes},
203+ booktitle = {TPHOLs '08: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics},
204+ year = {2008},
205+ isbn = {978-3-540-71065-3},
206+ pages = {278--293},
207+ location = {Montreal, P.Q., Canada},
208+ doi = {http://dx.doi.org/10.1007/978-3-540-71067-7_23},
209+ publisher = {Springer-Verlag},
210+ address = {Berlin, Heidelberg},
211+ }
212+
213+
214+@inproceedings{kipling,
215+ author = {McBride, Conor},
216+ title = {Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation},
217+ booktitle = {WGP '10: Proceedings of the 6th {ACM} {SIGPLAN} workshop on Generic programming},
218+ year = {2010},
219+ isbn = {978-1-4503-0251-7},
220+ pages = {1--12},
221+ location = {Baltimore, Maryland, USA},
222+ doi = {http://doi.{ACM}.org/10.1145/1863495.1863497},
223+ publisher = {{ACM}},
224+ address = {New York, NY, USA},
225+ }
226+
227+@inproceedings{padsml,
228+ author = {Yitzhak Mandelbaum and
229+ Kathleen Fisher and
230+ David Walker and
231+ Mary F. Fern{\'a}ndez and
232+ Artem Gleyzer},
233+ title = {{PADS/ML}: a functional data description language},
234+ booktitle = {POPL '07: Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on
235+ Principles of Programming Languages, POPL 2007, Nice, France,
236+ January 17-19, 2007},
237+ year = {2007},
238+ pages = {77-83},
239+ ee = {http://doi.{ACM}.org/10.1145/1190216.1190231},
240+ crossref = {DBLP:conf/popl/2007},
241+ bibsource = {DBLP, http://dblp.uni-trier.de}
242+}
243+
244+@proceedings{DBLP:conf/popl/2007,
245+ editor = {Martin Hofmann and
246+ Matthias Felleisen},
247+ title = {Proceedings of the 34th {ACM} {SIGPLAN}-SIGACT Symposium on
248+ Principles of Programming Languages, POPL 2007, Nice, France,
249+ January 17-19, 2007},
250+ booktitle = {POPL},
251+ publisher = {{ACM}},
252+ year = {2007},
253+ isbn = {1-59593-575-4},
254+ bibsource = {DBLP, http://dblp.uni-trier.de}
255+}
256+
257+@inproceedings{melange,
258+ author = {Madhavapeddy, Anil and Ho, Alex and Deegan, Tim and Scott, David and Sohan, Ripduman},
259+ title = {Melange: creating a "functional" internet},
260+ booktitle = {EuroSys '07: Proceedings of the 2nd {ACM} SIGOPS/EuroSys European Conference on Computer Systems 2007},
261+ year = {2007},
262+ isbn = {978-1-59593-636-3},
263+ location = {Lisbon, Portugal},
264+ doi = {http://doi.{ACM}.org/10.1145/1272996.1273009},
265+ publisher = {{ACM}},
266+ address = {New York, NY, USA},
267+ }
268+
269+
270+
271+@article{next700data,
272+ author = {Fisher, Kathleen and Mandelbaum, Yitzhak and Walker, David},
273+ title = {The next 700 data description languages},
274+ journal = {{SIGPLAN} Not.},
275+ volume = {41},
276+ number = {1},
277+ year = {2006},
278+ issn = {0362-1340},
279+ pages = {2--15},
280+ doi = {http://doi.{ACM}.org/10.1145/1111320.1111039},
281+ publisher = {{ACM}},
282+ address = {New York, NY, USA},
283+ }
284+
285+
286+@INPROCEEDINGS{xi-ats,
287+ author = {Hongwei Xi},
288+ title = {{Applied Type System} (extended abstract)},
289+ booktitle = {Types for Proofs and Programs 2003},
290+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
291+ publisher = {Springer},
292+ series = {Lecture Notes in Computer Science},
293+ volume = {3085},
294+ year = {2004},
295+ pages = {394--408}
296+}
297+
298+@inproceedings{powerpi,
299+ author = {Nicolas Oury and
300+ Wouter Swierstra},
301+ title = {The power of {Pi}},
302+ booktitle = {{ICFP} '08: Proceedings of the 13th {ACM} {SIGPLAN} International Conference
303+ on Functional Programming, {ICFP} 2008, Victoria, BC, Canada,
304+ September 20-28, 2008},
305+ year = {2008},
306+ pages = {39--50},
307+ ee = {http://doi.{ACM}.org/10.1145/1411204.1411213},
308+ crossref = {DBLP:conf/{ICFP}/2008},
309+ bibsource = {DBLP, http://dblp.uni-trier.de}
310+}
311+
312+@proceedings{DBLP:conf/{ICFP}/2008,
313+ editor = {James Hook and
314+ Peter Thiemann},
315+ title = {Proceeding of the 13th {ACM} {SIGPLAN} international conference
316+ on Functional programming, {ICFP} 2008, Victoria, BC, Canada,
317+ September 20-28, 2008},
318+ booktitle = {{ICFP}},
319+ publisher = {{ACM}},
320+ year = {2008},
321+ isbn = {978-1-59593-919-7},
322+ bibsource = {DBLP, http://dblp.uni-trier.de}
323+}
324+
325+
326+@inproceedings{security-types,
327+ author = {Morgenstern, Jamie and Licata, Daniel R.},
328+ title = {Security-typed programming within dependently typed programming},
329+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
330+ year = {2010},
331+ isbn = {978-1-60558-794-3},
332+ pages = {169--180},
333+ location = {Baltimore, Maryland, USA},
334+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863569},
335+ publisher = {{ACM}},
336+ address = {New York, NY, USA},
337+ }
338+
339+@inproceedings{levitation,
340+ author = {Chapman, James and Dagand, Pierre-\'{E}variste and McBride, Conor and Morris, Peter},
341+ title = {The gentle art of levitation},
342+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
343+ year = {2010},
344+ isbn = {978-1-60558-794-3},
345+ pages = {3--14},
346+ location = {Baltimore, Maryland, USA},
347+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863547},
348+ publisher = {{ACM}},
349+ address = {New York, NY, USA},
350+ }
351+
352+
353+
354+@INPROCEEDINGS{awkward,
355+ author = {Simon {Peyton Jones}},
356+ title = {Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in {Haskell}},
357+ booktitle = {Engineering theories of software construction},
358+ year = {2001},
359+ pages = {47--96}
360+}
361+
362+@inproceedings{scrap-engine,
363+ author = {Brady, Edwin and Hammond, Kevin},
364+ title = {Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation},
365+ booktitle = {{ICFP} '10: Proceedings of the 15th {ACM} {SIGPLAN} International Conference on Functional Programming},
366+ year = {2010},
367+ isbn = {978-1-60558-794-3},
368+ pages = {297--308},
369+ location = {Baltimore, Maryland, USA},
370+ doi = {http://doi.{ACM}.org/10.1145/1863543.1863587},
371+ publisher = {{ACM}},
372+ address = {New York, NY, USA},
373+ }
374+
375+@article{urweb,
376+ author = {Chlipala, Adam},
377+ title = {Ur: statically-typed metaprogramming with type-level record computation},
378+ journal = {{SIGPLAN} Not.},
379+ volume = {45},
380+ number = {6},
381+ year = {2010},
382+ issn = {0362-1340},
383+ pages = {122--133},
384+ doi = {http://doi.{ACM}.org/10.1145/1809028.1806612},
385+ publisher = {{ACM}},
386+ address = {New York, NY, USA},
387+ }
388+
389+
390+
391+@phdthesis{norell-thesis,
392+ author = {Ulf Norell},
393+ title = {Towards a practical programming language based on dependent type
394+ theory},
395+ school = {Chalmers University of Technology},
396+ year = 2007,
397+ month = {September},
398+}
399+
400+@inproceedings{open-type,
401+ author = {Schrijvers, Tom and Peyton Jones, Simon and Chakravarty, Manuel and Sulzmann, Martin},
402+ title = {Type checking with open type functions},
403+ booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},
404+ year = {2008},
405+ pages = {51--62},
406+ doi = {http://doi.{ACM}.org/10.1145/1411203.1411215},
407+ publisher = {{ACM}},
408+ address = {New York, NY, USA},
409+ }
410+
411+@inproceedings{ngna-dsl,
412+ title = {Domain Specific Languages ({DSL}s) for Network Protocols},
413+ author = {Saleem Bhatti and Edwin Brady and Kevin Hammond and James McKinna},
414+ year = {2009},
415+ booktitle = {International Workshop on Next Generation Network Architecture ({NGNA} 2009)}
416+}
417+
418+@phdthesis{gill-thesis,
419+ title = {Cheap deforestation for non-strict functional languages},
420+ author = {A Gill},
421+ institution = {University of Glasgow},
422+ month = {January},
423+ year = 1996
424+}
425+
426+@misc{llvm-haskell,
427+ title = {Low Level Virtual Machine for {Glasgow Haskell Compiler}},
428+ author = {David Terei},
429+ year = 2009,
430+ howpublished = {Bachelor's Thesis, Computer Science and Engineering Dept., The University of New South Wales, Sydney, Australia}
431+}
432+
433+@mastersthesis{llvm,
434+ title = {{LLVM}: An Infrastructure for Multi-Stage Optimization},
435+ author = {Chris Lattner},
436+ year = 2002,
437+ month = {December},
438+ institution = {Computer Science Dept., University of Illinois at Urbana-Champaign}
439+}
440+
441+@inproceedings{gpu-arrays,
442+ title = {GPU Kernels as Data-Parallel Array Computations in Haskell},
443+ author = {Sean Lee and Manuel M. T. Chakravarty and Vinod Grover and Gabriele Keller.},
444+ year = 2009,
445+ booktitle = {Workshop on Exploiting Parallelism using GPUs and other Hardware-Assisted Methods (EPAHM 2009)}
446+}
447+
448+@misc{cryptol,
449+ author = {Galois, Inc.},
450+ title = {Cryptol},
451+ year = {2009},
452+ howpublished = {\url{http://cryptol.net/}}
453+}
454+
455+@inproceedings{paradise-dsl,
456+ author = {Lennart Augustsson and Howard Mansell and Ganesh Sittampalam},
457+ title = {{Paradise: a two-stage DSL embedded in Haskell}},
458+ booktitle = {International Conf. on Functional Programming ({ICFP} 2008)},
459+ year = {2008},
460+ publisher = {{ACM}},
461+ pages = {225--228}
462+ }
463+
464+@misc{dsl-bib,
465+ author = {Arie {van Deursen} and Paul Klint and Joost Visser},
466+ title = {Domain-Specific Languages --- an annotated bibliography},
467+ year = 2000,
468+ howpublished = {\url{http://homepages.cwi.nl/~arie/papers/dslbib/}}
469+}
470+
471+@inproceedings{imperative-pe,
472+ author = {Debois, S{\o}ren},
473+ title = {Imperative program optimization by partial evaluation},
474+ booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
475+ year = {2004},
476+ isbn = {1-58113-835-0},
477+ pages = {113--122},
478+ location = {Verona, Italy},
479+ doi = {http://doi.{ACM}.org/10.1145/1014007.1014019},
480+ publisher = {{ACM}},
481+ address = {New York, NY, USA},
482+ }
483+
484+
485+@inproceedings{offline-pe-termination,
486+ author = {Andersen, Peter Holst and Holst, Carsten Kehler},
487+ title = {Termination Analysis for Offline Partial Evaluation of a Higher Order Functional Language},
488+ booktitle = {Proc. SAS '96: Intl. Symp. on Static Analysis},
489+ year = {1996},
490+ isbn = {3-540-61739-6},
491+ pages = {67--82},
492+ publisher = {Springer},
493+ notaddress = {London, UK},
494+ }
495+
496+
497+@inproceedings{stage-duplication,
498+ author = {Swadi, Kedar and Taha, Walid and Kiselyov, Oleg and Pasalic, Emir},
499+ title = {A monadic approach for avoiding code duplication when staging memoized functions},
500+ notbooktitle = {PEPM '06: Proceedings of the 2006 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
501+ booktitle = {Proc. PEPM '06:{ACM} Symp. on Partial Evaluation and Semantics-based Program Manipulation},
502+ year = {2006},
503+ isbn = {1-59593-196-1},
504+ pages = {160--169},
505+ location = {Charleston, South Carolina},
506+ doi = {http://doi.{ACM}.org/10.1145/1111542.1111570},
507+ notpublisher = {{ACM}},
508+ notaddress = {New York, NY, USA},
509+ }
510+
511+
512+@inproceedings{concoqtion,
513+ author = {Fogarty, Seth and Pasalic, Emir and Siek, Jeremy and Taha, Walid},
514+ title = {Concoqtion: indexed types now!},
515+ booktitle = {PEPM '07: Proceedings of the 2007 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
516+ year = {2007},
517+ isbn = {978-1-59593-620-2},
518+ pages = {112--121},
519+ location = {Nice, France},
520+ doi = {http://doi.{ACM}.org/10.1145/1244381.1244400},
521+ publisher = {{ACM}},
522+ address = {New York, NY, USA},
523+ }
524+
525+@inproceedings{metahaskell,
526+ author = "Tim Sheard and Simon {Peyton Jones}",
527+ title = "Template metaprogramming for {Haskell}",
528+ booktitle = "{ACM} Haskell Workshop",
529+ year = 2002,
530+ month = oct,
531+ pages = "1-16",
532+ noteditor = "Manuel M. T. Chakravarty",
533+ notpublisher = "{ACM} Press"
534+}
535+
536+@misc{shark-profiler,
537+ title = {Optimizing your application with {Shark 4}},
538+ year = 2009,
539+ howpublished = {\url{http://developer.apple.com/tools/sharkoptimize.html}}
540+}
541+
542+@misc{shootout,
543+ title = {The Computer Language Benchmark Game},
544+ year = {2009},
545+ howpublished = {\url{http://shootout.alioth.debian.org/}}
546+}
547+
548+@article{futamura,
549+ author = {Yoshihiko Futamura},
550+ year = 1971,
551+ title = "Partial Evaluation of Computation Process --– An Approach to a Compiler-Compiler",
552+ journal = {Systems, Comps., Controls},
553+ volume = 2,
554+ number = 5,
555+ pages = {45-–50}
556+}
557+
558+@book{pebook,
559+ title = {Partial Evaluation and Automatic Program Generation},
560+ author = {N.D. Jones and C.K. Gomard and P. Sestoft},
561+ year = 1993,
562+ publisher = {Prentice Hall International}
563+}
564+
565+@inproceedings{pantheon,
566+ author = {Sean Seefried and Manuel Chakravarty and Gabriele Keller},
567+ title = {Optimising Embedded {DSLs} using {Template Haskell}},
568+ year = {2004},
569+ booktitle = {{Proc. GPCE~'04: Conf. Generative Prog. and Component Eng.}},
570+ publisher = {Springer},
571+ series = {LNCS}
572+}
573+
574+@article{pan,
575+ author = {Elliott, Conal and Finne, Sigbj\orn and De Moor, Oege},
576+ title = {Compiling embedded languages},
577+ journal = {J. Funct. Program.},
578+ volume = {13},
579+ number = {3},
580+ year = {2003},
581+ issn = {0956-7968},
582+ pages = {455--481},
583+ doi = {http://dx.doi.org/10.1017/S0956796802004574},
584+ publisher = {Cambridge University Press},
585+ address = {New York, NY, USA},
586+ }
587+
588+
589+@inproceedings{russell,
590+ author = {Sozeau, Matthieu},
591+ title = {Program-ing finger trees in Coq},
592+ booktitle = {{ICFP} '07: Proceedings of the 12th {ACM} {SIGPLAN} international conference on Functional programming},
593+ year = {2007},
594+ isbn = {978-1-59593-815-2},
595+ pages = {13--24},
596+ location = {Freiburg, Germany},
597+ doi = {http://doi.{ACM}.org/10.1145/1291151.1291156},
598+ publisher = {{ACM}},
599+ address = {New York, NY, USA},
600+ }
601+
602+@inproceedings{turner-total,
603+ author = {D. A. Turner},
604+ title = {Elementary Strong Functional Programming},
605+ year = 1995,
606+ booktitle = "First International Symposium on Functional Programming Languages in Education",
607+ publisher = {Springer},
608+ series = {LNCS},
609+ volume = {1022},
610+ pages = {1--13}
611+}
612+
613+@incollection{free-theorems,
614+ author = "P. Wadler",
615+ title = "Theorems for Free!",
616+ booktitle = "{Proc. 4th Int.\ Conf.\ on Funct.\ Prog.\ Languages and Computer Arch., {FPCA}'89, London, {UK}, 11--13 Sept 1989}",
617+ publisher = "{ACM} Press",
618+ address = "New York",
619+ pages = "347--359",
620+ year = "1989",
621+ url = "citeseer.ist.psu.edu/wadler89theorems.html"
622+}
623+
624+@inproceedings{TrulyConcurrent,
625+ author = {Naiyong Jin and Jifeng He},
626+ title = {Towards A Truly Concurrent Model for Processes Sharing Resources},
627+ booktitle = {Proc. 3rd {IEEE} International Conf. on Soft. Eng. and Formal Methods},
628+ year = {2005},
629+ isbn = {0-7695-2435-4},
630+ pages = {231--239},
631+ doi = {http://dx.doi.org/10.1109/SEFM.2005.50},
632+ publisher = {{IEEE} Computer Society},
633+ address = {Washington, DC, USA},
634+ }
635+
636+@misc{GPCE2006,
637+ note = {Omitted to preserve anonymity, contact PC chair for details}
638+}
639+
640+@misc{IFL2006,
641+ note = {Omitted to preserve anonymity, contact PC chair for details}
642+}
643+
644+@misc{ivor-anon,
645+ note = {Omitted to preserve anonymity, contact PC chair for details}
646+}
647+
648+@inproceedings{HaskellIO,
649+ author = {Simon L. {Peyton Jones} and Philip Wadler},
650+ title = {Imperative functional programming},
651+ booktitle = {Proc. 20th {ACM} Symposium on Principles of programming languages},
652+ year = {1993},
653+ isbn = {0-89791-560-7},
654+ pages = {71--84},
655+ location = {Charleston, South Carolina, United States},
656+ doi = {http://doi.{ACM}.org/10.1145/158511.158524},
657+ publisher = {{ACM}},
658+ address = {New York, NY, USA},
659+ }
660+
661+@article{CorrectnessConstruction,
662+author = "P. Amey",
663+title = "{Correctness by Construction: Better can also be Cheaper}",
664+journal = "{CrossTalk: the Journal of Defense Software Engineering}",
665+month = mar,
666+year = 2002,
667+pages = "24--28"
668+}
669+
670+
671+
672+@INPROCEEDINGS{hj:popl03,
673+ AUTHOR = {M. Hofmann and S. Jost},
674+ TITLE = {Static Prediction of Heap Space Usage for First-Order Function
675+al Programs},
676+booktitle = "Proc. {POPL 2003 --- 2003 {ACM} Symp. on Principles of Programming La
677+nguages}",
678+ KEY = {HJ_POPL03},
679+ PAGES = {185--197},
680+ YEAR = {2003},
681+ ORGANIZATION = {{ACM}}
682+}
683+
684+
685+@article{kobayashi-lock,
686+ author = {Naoki Kobayashi},
687+ title = {A type system for lock-free processes},
688+ journal = {Inf. Comput.},
689+ volume = {177},
690+ number = {2},
691+ year = {2002},
692+ issn = {0890-5401},
693+ pages = {122--159},
694+ doi = {http://dx.doi.org/10.1016/S0890-5401(02)93171-8},
695+ publisher = {Academic Press, Inc.},
696+ address = {Duluth, MN, USA},
697+ }
698+
699+@techreport{linear-alias,
700+ title = {Linear types for aliased resources},
701+ author = {Chris Hawblitzel},
702+ year = {2005},
703+ institution = {Microsoft Research},
704+ number = {MSR-TR-2005-141}
705+}
706+
707+@article{kobayashi-esop,
708+ title = {Type-Based Analysis of Deadlock fora Concurrent Calculus with Interrupts},
709+ author = {Kohei Suenaga and Naoki Kobayashi},
710+ year = {2007},
711+ booktitle = {ESOP}
712+}
713+
714+@inproceedings{res-c,
715+ title = {A Path Sensitive Type System for Resource Usage Verification of C Like Languages},
716+ author = {Hyun-Goo Kang and Youil Kim and Taisook Han and Hwansoo Han},
717+ year = 2005,
718+ publisher = {Springer-Verlag},
719+ booktitle = {Programming Languages and Systems},
720+ pages = {264--280},
721+ series = {LNCS},
722+ volume = {3780}
723+}
724+
725+@miscs{lsr,
726+ title = {Lightweight static resources: Sexy types for embedded and systems programming},
727+ author = {Oleg Kiselyov and Chung-Chieh Shan},
728+ year = 2007,
729+ note = {Draft}
730+}
731+
732+@inproceedings{scoped-res,
733+ title = {Resource Usage Analysis Via Scoped Methods},
734+ author = {Gang Tan and Xinming Ou and David Walker},
735+ booktitle = {Foundations of Object-Oriented Languages},
736+ year = {2003}
737+}
738+
739+@article{igarashi-res,
740+ author = {Igarashi, Atsushi and Kobayashi, Naoki},
741+ title = {Resource usage analysis},
742+ journal = {ACM Trans. Program. Lang. Syst.},
743+ volume = {27},
744+ issue = {2},
745+ month = {March},
746+ year = {2005},
747+ issn = {0164-0925},
748+ pages = {264--313},
749+ numpages = {50},
750+ url = {http://doi.acm.org/10.1145/1057387.1057390},
751+ doi = {http://doi.acm.org/10.1145/1057387.1057390},
752+ acmid = {1057390},
753+ publisher = {ACM},
754+ address = {New York, NY, USA},
755+ keywords = {Resource usage, type inference},
756+}
757+
758+@phdthesis{monitoring,
759+ title = {Policy Enforcement via Program Monitoring},
760+ author = {Jarred Adam Ligatti},
761+ year = 2006,
762+ month = {May}
763+}
764+
765+@inproceedings{sec-policy,
766+ title = {A Type System for Expressive Security Policies},
767+ author = {David Walker},
768+ booktitle = {Twenty-Seventh {ACM} {SIGPLAN} Symposium on Principles of Programming Languages},
769+ pages = {254--267},
770+ year = 2000}
771+
772+@inproceedings{res-dfa,
773+ author = {K. Marriott and P.J. Stuckey and M. Sulzmann},
774+ title = {Resource Usage Verification},
775+ year = 2003,
776+ booktitle = {In Proc. of First Asian Symposium, APLAS 2003},
777+ pages = {212--229},
778+ publisher = {Springer-Verlag}
779+}
780+
781+@incollection{ hancock-interactive,
782+ author = "Peter Hancock and Anton Setzer",
783+ title = "Interactive Programs in Dependent Type Theory",
784+ booktitle = "Proc.\ of 14th Ann.\ Conf.\ of {EACSL}, {CSL}'00, Fischbau, Germany, 21--26 Aug 2000",
785+ volume = "1862",
786+ publisher = "Springer-Verlag",
787+ address = "Berlin",
788+ editor = "P. Clote and H. Schwichtenberg",
789+ pages = "317--331",
790+ year = "2000",
791+ url = "citeseer.ist.psu.edu/hancock00interactive.html" }
792+
793+@inproceedings{popeea-resources,
794+ author = {Corneliu Popeea and Wei-Ngan Chin},
795+ title = {A type system for resource protocol verification and its correctness proof},
796+ booktitle = {PEPM '04: Proceedings of the 2004 {ACM} {SIGPLAN} symposium on Partial evaluation and semantics-based program manipulation},
797+ year = {2004},
798+ isbn = {1-58113-835-0},
799+ pages = {135--146},
800+ location = {Verona, Italy},
801+ doi = {http://doi.{ACM}.org/10.1145/1014007.1014021},
802+ publisher = {{ACM} Press},
803+ address = {New York, NY, USA},
804+ }
805+
806+@inproceedings{sheard-langfuture,
807+ author = {Tim Sheard},
808+ title = "Languages of the future",
809+ booktitle = "{ACM} Conference on Object Orientated Programming Systems, Languages and Applicatioons (OOPSLA'04)",
810+ year = "2004"
811+}
812+
813+@inproceedings{ivor,
814+ author = {Edwin Brady},
815+ title = {{Ivor}, a proof engine},
816+ year = {2007},
817+ publisher = {Springer-Verlag},
818+ series = {LNCS},
819+ booktitle = {Implementation and Application of Functional Languages 2006}
820+}
821+
822+@misc{coq-in-coq,
823+ author = {Bruno Barras and Benjamin Werner},
824+ year = 1997,
825+ title = {{Coq} in {Coq}}
826+}
827+
828+@article{hudak-edsl,
829+ author = {Paul Hudak},
830+ title = {Building Domain-Specific Embedded Languages},
831+ year = {1996},
832+ month = {December},
833+ journal = {{ACM} Computing Surveys},
834+ volume = {28A},
835+ number = {4}
836+}
837+
838+@inproceedings{concon,
839+ author = {Conor McBride and Healfdene Goguen and James McKinna},
840+ title = {Some Constructions On Constructors},
841+ year = 2005,
842+ booktitle = {TYPES 2004},
843+ publisher = {Springer},
844+ series = {LNCS},
845+ volume = {3839}
846+}
847+
848+@InProceedings{Hume-GPCE,
849+author = {K. Hammond and G.J. Michaelson},
850+title = {{Hume: a Domain-Specific Language for Real-Time Embedded Systems}},
851+booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'03)}},
852+publisher = {Springer-Verlag},
853+series = {Lecture Notes in Computer Science},
854+year = {2003},
855+}
856+
857+@inproceedings{lcf-milner,
858+ author = {Robin Milner},
859+ title = {{LCF}: A Way of Doing Proofs with a Machine},
860+ booktitle = {Mathematical Foundations of Computer Science 1978},
861+ pages = {146-159},
862+ year = 1979,
863+ series = {LNCS},
864+ volume = {64}
865+}
866+
867+
868+@inproceedings{epireloaded,
869+ title = {Epigram Reloaded: A Standalone Typechecker for {ETT}},
870+ author = {James Chapman and Thorsten Altenkirch and Conor McBride},
871+ year = 2006,
872+ booktitle = {Trends in Functional Programming 2005},
873+ note = {To appear}
874+}
875+
876+@TECHREPORT{why-tool,
877+ AUTHOR = {J.-C. Filli\^atre},
878+ TITLE = {{Why: a multi-language multi-prover verification tool}},
879+ INSTITUTION = {{LRI, Universit\'e Paris Sud}},
880+ TYPE = {{Research Report}},
881+ NUMBER = {1366},
882+ MONTH = {March},
883+ YEAR = 2003,
884+ URL = {http://www.lri.fr/~filliatr/ftp/publis/why-tool.ps.gz}
885+}
886+
887+@misc{ large-extraction,
888+ author = "Lu\'iz Cruz-Filipe and Bas Spitters",
889+ title = "Program Extraction from Large Proof Developments",
890+ year = 2003,
891+ url = "citeseer.ist.psu.edu/cruz-filipe03program.html" }
892+
893+@inproceedings{ fta,
894+ author = "Herman Geuvers and Freek Wiedijk and Jan Zwanenburg",
895+ title = "A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals",
896+ booktitle = "{TYPES 2000}",
897+ pages = "96--111",
898+ year = "2000",
899+ url = "citeseer.ist.psu.edu/geuvers01constructive.html" }
900+
901+@article{mckinna-expr,
902+ title = {A type-correct, stack-safe, provably correct, expression compiler in {Epigram}},
903+ author = {James McKinna and Joel Wright},
904+ year = 2007,
905+ journal = {Journal of Functional Programming},
906+ note = {To appear}
907+}
908+
909+@article{pugh-omega,
910+ title = "The {Omega} {Test}: a fast and practical integer programming algorithm for dependence analysis",
911+ author = "William Pugh",
912+ journal = "Communication of the {ACM}",
913+ year = 1992,
914+ pages = {102--114}
915+}
916+
917+@misc{four-colour,
918+ author = "Georges Gonthier",
919+ title = "A computer-checked proof of the {Four Colour Theorem}",
920+ year = 2005,
921+ howpublished = {\url{http://research.microsoft.com/~gonthier/4colproof.pdf}}}
922+
923+@inproceedings{sparkle,
924+ author = "Maarten {de Mol} and Marko {van Eekelen} and Rinus Plasmeijer",
925+ title = "Theorem Proving for Functional Programmers",
926+ url = "citeseer.ist.psu.edu/654423.html",
927+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2002)},
928+ publisher = {Springer},
929+ series = {LNCS},
930+ volume = {2312},
931+ year = 2002
932+ }
933+
934+@misc{agda,
935+ title = {Agda},
936+ author = {Catarina Coquand},
937+ howpublished= {\url{http://agda.sourceforge.net/}},
938+ year = 2005
939+}
940+
941+@misc{cover,
942+ title = {Cover Translator},
943+ howpublished = {\url{http://coverproject.org/CoverTranslator/}}
944+}
945+
946+@misc{parsec,
947+ title = {Parsec, a fast combinator parser},
948+ author = {Daan Leijen},
949+ year = {2001},
950+ howpublished = {\url{http://www.cs.uu.nl/~daan/parsec.html}}
951+}
952+
953+@inproceedings{dtpmsp-gpce,
954+ author = {Edwin Brady and Kevin Hammond},
955+ title = {A Verified Staged Interpreter is a Verified Compiler},
956+ booktitle = {{Proc. Conf. Generative Programming and Component Engineering (GPCE~'06)}},
957+ year = 2006
958+}
959+
960+@misc{haddock,
961+ title = {Haddock: A {Haskell} Documentation Tool},
962+ howpublished = {\url{http://www.haskell.org/haddock/}}
963+}
964+
965+@inproceedings{offshoring,
966+ title = {Implicitly Heterogeneous Multi-Stage Programming},
967+ author = {Jason Eckhardt and Roumen Kaibachev and Emir Pa\v{s}al\'{i}c and Kedar Swadi and Walid Taha},
968+ booktitle = {Proc. 2005 Conf. on Generative Programming and Component Engineering (GPCE 2005)},
969+ publisher = {Springer},
970+ series = {LNCS},
971+ volume = {3676},
972+ year = 2005
973+}
974+
975+@misc{alti-partial,
976+ title = {Stop thinking about bottoms when writing programs},
977+ author = {Thorsten Altenkirch},
978+ year = 2006,
979+ note = {Talk at BCTCS 2006}
980+}
981+
982+@misc{tarmo-partial,
983+ title = {Partiality is an Effect},
984+ author = {Tarmo Uustalu},
985+ year = 2004,
986+ note = {Talk at Dagstuhl workshop on Dependently Typed Progamming}
987+}
988+
989+@inproceedings{McKinnaPOPL06,
990+ author = {James McKinna},
991+ title = {Why dependent types matter},
992+ booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2006)},
993+ year = {2006},
994+ issn = {0362-1340},
995+ pages = {1--1},
996+ doi = {http://doi.{ACM}.org/10.1145/1111320.1111038},
997+}
998+
999+
1000+@inproceedings{leroy-compiler,
1001+ title = {Formal Certification of a Compiler Back-end},
1002+ author = {Xavier Leroy},
1003+ year = 2006,
1004+ booktitle = {Principles of Programming Languages 2006},
1005+ pages = {42--54},
1006+ publisher = {{ACM} Press}
1007+}
1008+
1009+@inproceedings{hutton-exceptions,
1010+ title = {Compiling Exceptions Correctly},
1011+ year = 2004,
1012+ author = {Graham Hutton and Joel Wright},
1013+ booktitle = {Mathematics of Program Construction},
1014+ publisher = {Springer},
1015+ series = {LNCS},
1016+ volume = {3125}
1017+}
1018+
1019+@inproceedings{tagless-staged,
1020+ title = {Tagless Staged Interpreters for Typed Languages},
1021+ year = {2002},
1022+ booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},
1023+ author = {Emir Pa\v{s}al\'{i}c and Walid Taha and Tim Sheard},
1024+ publisher = {{ACM}}
1025+}
1026+
1027+@inproceedings{env-classifiers,
1028+ title = {Environment Classifiers},
1029+ year = 2003,
1030+ author = {Walid Taha},
1031+ booktitle = {Proc. {ACM} Symp. on Principles of Programming Languages (POPL 2003)},
1032+ pages = {26--37},
1033+}
1034+
1035+@inproceedings{dsl-msp,
1036+ title = {{DSL} Implementation in {MetaOCaml}, {Template Haskell}, {and C++}},
1037+ booktitle = {Domain Specific Program Genearation 2004},
1038+ author = {Krzysztof Czarnecki and John O'Donnell and J\"{o}rg Striegnitz and Walid Taha},
1039+ publisher = {Springer},
1040+ series = {LNCS},
1041+ volume = {3016},
1042+ year = 2004
1043+}
1044+
1045+@misc{ gadt-extk,
1046+ author = {Tim Sheard and James Hook and Nathan Linger},
1047+ title = {{GADTs} + Extensible Kinds = Dependent Programming},
1048+ year = 2005,
1049+ misc = {Submitted to {ICFP} '05}
1050+}
1051+
1052+@INPROCEEDINGS{dt-framework,
1053+ TITLE = {A Dependently Typed Framework for Static Analysis of Program Execution Costs},
1054+ YEAR = {2006},
1055+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
1056+ AUTHOR = {Edwin Brady and Kevin Hammond},
1057+ VOLUME = {4015},
1058+ SERIES = {LNCS},
1059+ PAGES = {74--90},
1060+ PUBLISHER = {Springer}
1061+}
1062+
1063+@INPROCEEDINGS{step-counting,
1064+ TITLE = {Accurate Step Counting},
1065+ YEAR = {2006},
1066+ BOOKTITLE = {Proc. Implementation of Functional Languages (IFL 2005)},
1067+ AUTHOR = {Catherine Hope and Graham Hutton},
1068+ PUBLISHER = {Springer}
1069+}
1070+
1071+@misc{multi-taha,
1072+ author = {Walid Taha},
1073+ title = {{A Gentle Introduction to Multi-stage Programming}},
1074+ year = {2003},
1075+ note = {Available from \url{http://www.cs.rice.edu/~taha}},
1076+ notnote = {Available from \url{http://www.cs.rice.edu/~taha/publications/journal/dspg04a.pdf}}
1077+}
1078+
1079+@misc{mckinnabrady-phase,
1080+ title = {Phase Distinctions in the Compilation of {Epigram}},
1081+ year = 2005,
1082+ author = {James McKinna and Edwin Brady},
1083+ note = {Draft}
1084+}
1085+
1086+@phdthesis{ brady-thesis,
1087+ author = {Edwin Brady},
1088+ title = {Practical Implementation of a Dependently Typed Functional Programming Language},
1089+ year = 2005,
1090+ school = {University of Durham}
1091+}
1092+
1093+@phdthesis{ taha-thesis,
1094+ author = {Walid Taha},
1095+ title = {Multi-stage Programming: Its Theory and Applications},
1096+ year = 1999,
1097+ school = {Oregon Graduate Inst. of Science and Technology}
1098+}
1099+
1100+@phdthesis{ pasalic-thesis,
1101+ author = {Emir Pa\v{s}al\'{i}c},
1102+ title = {The Role of Type-Equality in Meta-programming},
1103+ year = 2004,
1104+ school = {OGI School of Science and Engineering}
1105+}
1106+
1107+@misc{ydtm,
1108+ author = {Thorsten Altenkirch and Conor McBride and James McKinna},
1109+ title = {Why Dependent Types Matter},
1110+ note = {Draft},
1111+ year = 2005}
1112+
1113+
1114+@inproceedings { wadler-listless,
1115+ author = {Philip Wadler},
1116+ title = {Listlessness is better than laziness: {Lazy} evaluation and garbage collection at compile-time},
1117+ booktitle = {Proceedings of the 1984 {ACM} Symposium on LISP and functional programming},
1118+ year = 1984,
1119+ pages = {45--52}
1120+}
1121+
1122+@techreport { gofer-impl,
1123+ author = {Mark P. Jones},
1124+ title = {The implementation of the Gofer functional programming system},
1125+ month = {May},
1126+ year = {1994},
1127+ number = {YALEU/DCS/RR-1030},
1128+ institution = {Yale University}
1129+}
1130+
1131+@techreport { pm-opt1,
1132+ author = {Kevin Scott and Norman Ramsey},
1133+ title = {When do match-compilation heuristics matter?},
1134+ month = {May},
1135+ year = {2000},
1136+ number = {CS-2000-13},
1137+ institution = {Department of Computer Science, University of Virginia}
1138+}
1139+
1140+@inproceedings{ pm-opt2,
1141+ author = "Fabrice Le Fessant and Luc Maranget",
1142+ title = "Optimizing Pattern Matching",
1143+ booktitle = "International Conference on Functional Programming",
1144+ pages = "26-37",
1145+ year = "2001",
1146+ url = "citeseer.ist.psu.edu/lefessant01optimizing.html" }
1147+
1148+@incollection{con-engine,
1149+ author = {G\'{e}rard Huet},
1150+ title = {The constructive engine},
1151+ booktitle = {A Perspective in Theoreticak Computer Science},
1152+ publisher = {World Scientific Publishing},
1153+ year = {1989},
1154+ editor = {R. Narasimhan},
1155+ note = {Commemorative Volume for Gift Siromoney},
1156+ pages = {38--69}
1157+}
1158+
1159+@inproceedings{gadts,
1160+ title = {Simple unification-based type inference for {GADTs}},
1161+ author = {Simon {Peyton Jones} and Dimitrios Vytiniotis and Stephanie Weirich and Geoffrey Washburn},
1162+ year = {2006},
1163+ booktitle = {Proc. 2006 International Conf. on Functional Programming ({ICFP} 2006)}
1164+}
1165+
1166+@misc{wobbly,
1167+ author = {Simon {Peyton Jones} and Geoffrey Washburn and Stephanie Weirich},
1168+ title = {Wobbly types: type inference for generalised algebraic data types},
1169+ year = {2004},
1170+ note = {Submitted to POPL 2005}
1171+}
1172+
1173+@misc{epigram-afp,
1174+ author = {Conor McBride},
1175+ title = {Epigram: Practical Programming with Dependent Types},
1176+ year = {2004},
1177+ howpublished = {Lecture Notes, International Summer School on Advanced Functional Programming}
1178+}
1179+
1180+@book{ml85,
1181+ author = {Per Martin-L\"{o}f},
1182+ title = "Intuitionistic Type Theory",
1183+ year = "1985",
1184+ publisher = "Bibliopolis"
1185+}
1186+
1187+@article{modular-fulllazy,
1188+ title = {A Modular Fully Lazy Lambda Lifter in {Haskell}},
1189+ author = {Simon {Peyton Jones} and David Lester},
1190+ year = {1991},
1191+ month = {May},
1192+ journal = {Software Practice and Experience},
1193+ volume = {21},
1194+ number = {5},
1195+ pages = {479--506}
1196+}
1197+
1198+@article{ghani-jay95,
1199+ author = {Barry Jay and Neil Ghani},
1200+ title = {The Virtues of Eta-Expansion},
1201+ journal = {Journal of Functional Programming},
1202+ year = {1995},
1203+ volume = {5},
1204+ number = {2},
1205+ pages = {135-154},
1206+}
1207+
1208+@misc{nkpat,
1209+ author = {Lennart Augustsson},
1210+ title = {n+k patterns},
1211+ year = {1993},
1212+ howpublished = {Message to the haskell mailing list, Mon, 17 May 93}
1213+}
1214+
1215+@article{ danvy98functional,
1216+ author = "Olivier Danvy",
1217+ title = "Functional Unparsing",
1218+ journal = "Journal of Functional Programming",
1219+ volume = "8",
1220+ number = "6",
1221+ pages = "621-625",
1222+ year = "1998",
1223+ url = "citeseer.ist.psu.edu/danvy98functional.html" }
1224+
1225+@inproceedings{SeveriPoll94,
1226+ author = {Paula Severi and Erik Poll},
1227+ booktitle = {Logical Foundations of Computing Science, LFCS'94},
1228+ editor = {A. Nerode and Yu. V. Matiyasevich},
1229+ number = {813},
1230+ pages = {316--328},
1231+ publisher = {Springer},
1232+ series = {LNCS},
1233+ title = {{P}ure {T}ype {S}ystems with {D}efinitions},
1234+ year = {1994}
1235+}
1236+
1237+@inproceedings{coinductive,
1238+ title = {An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol},
1239+ booktitle = {Proceedings of the 1995 Workshop on Types for Proofs and Programs},
1240+ series = {LNCS},
1241+ year = {1995},
1242+ volume = {1158},
1243+ pages = {135-152},
1244+ publisher = {Springer-Verlag},
1245+ author = {Eduardo Gim\'{e}nez}
1246+}
1247+
1248+@book{erlang,
1249+ author = "Joe Armstrong and Robert Virding and Claes Wikstr{\"o}m and Mike Williams",
1250+ title = "Concurrent Programming in Erlang",
1251+ edition = "Second",
1252+ publisher = "Prentice-Hall",
1253+ year = "1996",
1254+ url = "citeseer.ist.psu.edu/armstrong93concurrent.html"
1255+}
1256+
1257+@PhdThesis{alti:phd93,
1258+ author = "Thorsten Altenkirch",
1259+ title = "Constructions, Inductive Types and Strong Normalization",
1260+ school = "University of Edinburgh",
1261+ year = "1993",
1262+ month = "November",
1263+}
1264+
1265+@inproceedings{coq-modules,
1266+ author = "Jacek Chrzaszcz",
1267+ title = "Modules in {Coq} Are and Will Be Correct",
1268+ year = {2004},
1269+ booktitle = {Types for Proofs and Programs 2003},
1270+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
1271+ publisher = {Springer},
1272+ volume = {3085}
1273+}
1274+
1275+@inproceedings{comp-polymorphism,
1276+ author = "Robert Harper and Greg Morrisett",
1277+ title = "Compiling Polymorphism Using Intensional Type Analysis",
1278+ year = "1995",
1279+ booktitle = "Proceedings of the 22nd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programming languages",
1280+ pages = "130 -- 141"
1281+}
1282+
1283+@misc{runtime-loader,
1284+ author = "Andre Pang",
1285+ title = "{GHC} Runtime Loading",
1286+ year = "2004",
1287+ howpublished = {Available from \verb+http://www.algorithm.com.au/wiki/hacking/haskell.ghc_runtime_loading+}
1288+}
1289+
1290+@article{mccarthy-lisp,
1291+ author = "John McCarthy",
1292+ title = "Recursive Functions of Symbolic Expressions and Their Computation By Machine",
1293+ year = "1960",
1294+ journal = "Communications of the {ACM}",
1295+ volume = "3",
1296+ number = "4",
1297+ pages = "184--195"
1298+}
1299+
1300+@book{stl,
1301+ author = " David R. Musser and Atul Saini and Gillmer J. Derge",
1302+ title= "The {STL} Tutorial and Reference Guide: {C++} Programming with the Standard Template Library",
1303+ year = "2001",
1304+ publisher = "Addison Wesley"
1305+}
1306+
1307+@misc{ phase-distinction,
1308+ author = "Luca Cardelli",
1309+ title = "Phase Distinctions in Type Theory",
1310+ howpublished = "Manuscript",
1311+ year = "1988",
1312+ url = "citeseer.ist.psu.edu/cardelli88phase.html" }
1313+
1314+@book {pierce-types,
1315+ author = "Benjamin C. Pierce",
1316+ title = "Type and Programming Languages",
1317+ year = "2002",
1318+ publisher = "MIT Press"
1319+}
1320+
1321+@article{ coqcc,
1322+ Author = "Thierry Coquand and G\'{e}rard Huet",
1323+ title = "The calculus of constructions",
1324+ year = "1988",
1325+ journal = "Information and Computation",
1326+ volume = "76",
1327+ pages = "95--120"
1328+}
1329+
1330+@article{ miller91jlc,
1331+ Author = "Dale Miller",
1332+ Title = "A Logic Programming Language with Lambda-Abstraction,
1333+ Function Variables, and Simple Unification",
1334+ Journal = "Journal of Logic and Computation",
1335+ Volume = "1",
1336+ Number = "4",
1337+ Pages = "497-536",
1338+ Year = "1991",
1339+ URL = "citeseer.ist.psu.edu/miller91logic.html",
1340+ URL = "file://ftp.cis.upenn.edu/pub/papers/miller/jlc91.dvi.Z" }
1341+
1342+@article{miller-unity,
1343+ author = "Dale Miller",
1344+ title = "Unification Under a Mixed Prefix",
1345+ journal = "Journal of Symbolic Computation",
1346+ volume = "14",
1347+ pages = "321--358",
1348+ year = 1992
1349+}
1350+
1351+@inproceedings{ cynthia,
1352+ author = "Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe",
1353+ title = "An {ML} Editor Based on Proofs-As-Programs",
1354+ booktitle = "Automated Software Engineering",
1355+ pages = "166-173",
1356+ year = "1999",
1357+ url = "citeseer.ist.psu.edu/whittle99ml.html" }
1358+
1359+
1360+@misc{ewd340,
1361+ title={The Humble Programmer},
1362+ author={Edsger Dijkstra},
1363+ year={1972},
1364+ note={Turing Award Lecture, EWD 340}
1365+}
1366+
1367+@misc{fortran,
1368+ title={Specifications for the {IBM} Mathematical FORmula TRANslating System, {FORTRAN}},
1369+ author={{IBM Applied Science Division}},
1370+ key={IBM},
1371+ year={1954},
1372+ month={November}
1373+}
1374+
1375+@inproceedings{quickcheck,
1376+ title = {{QuickCheck}: A Lightweight Tool For Random Testing Of {Haskell} Programs},
1377+ author = {Koen Claessen and John Hughes},
1378+ year = {2000},
1379+ booktitle = {International Conference on Functional Programming}
1380+}
1381+
1382+@inproceedings{currylam,
1383+ title = {Functionality in Combinatory Logic},
1384+ author = {Haskell Curry},
1385+ year = {1934},
1386+ booktitle = {Proc. Nat. Acad. Sci, USA},
1387+ volume = {20},
1388+ pages = {584--590}
1389+}
1390+
1391+@article{churchsimplelam1,
1392+ title = {A set of postulates for the foundation of logic},
1393+ author = {Alonzo Church},
1394+ year = {1932},
1395+ journal = {Annals of Mathematics},
1396+ volume = {2},
1397+ number = {33},
1398+ pages = {346--366}
1399+}
1400+
1401+@article{churchsimplelam2,
1402+ title = {A set of postulates for the foundation of logic},
1403+ author = {Alonzo Church},
1404+ year = {1933},
1405+ journal = {Annals of Mathematics},
1406+ volume = {2},
1407+ number = {34},
1408+ pages = {839--864}
1409+}
1410+
1411+@article{churchlam,
1412+ title = {A Formulation of the Simple Theory of Types},
1413+ author = {Alonzo Church},
1414+ year = {1940},
1415+ journal = {Journal of Symbolic Logic},
1416+ volume = {5},
1417+ pages = {56--58}
1418+}
1419+
1420+@book{mitchell,
1421+ title = {Concepts in Programming Languages},
1422+ author = {John C. Mitchell},
1423+ year = {2003},
1424+ publisher = {Cambridge University Press}
1425+}
1426+
1427+@inproceedings{harrison-hol99,
1428+ title = {A Machine-Checked Theory of Floating Point Arithmetic},
1429+ year = {1999},
1430+ booktitle = {Theorem Proving in Higher Order Logics: 12th International Conference, TP},
1431+ pages = {113--130},
1432+ author = {John Harrison},
1433+ crossref = {hol99}
1434+}
1435+
1436+@inproceedings{c--,
1437+ title = {C--: A portable assembly language},
1438+ year = {1997},
1439+ booktitle = {Workshop on Implementing Functional Languages, St Andrews},
1440+ author = {Simon {Peyton Jones} and Thomas Nordin and Dino Oliva},
1441+ crossref = {func-imp97}
1442+}
1443+
1444+@proceedings{func-imp97,
1445+ title = {Workshop on Implementing Functional Languages, St Andrews},
1446+ year = {1997},
1447+ editor = {C Clack},
1448+ publisher = {Springer-Verlag}
1449+}
1450+
1451+@proceedings{hol99,
1452+ volume = {1690},
1453+ title = {Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'99},
1454+ year = {1999},
1455+ editor = {Yves Bertot and Gilles Dowek and Andr{\'e} Hirschowitz and Christine Paul},
1456+ publisher = {Springer-Verlag},
1457+ address = {Nice, France},
1458+ series = {LNCS}
1459+}
1460+
1461+@book{mathlogic,
1462+ title = {Mathematical Logic and Programming Languages},
1463+ year = {1985},
1464+ editor = {C.A.R. Hoare and J.C. Shepherdson},
1465+ publisher = {Prentice-Hall}
1466+}
1467+
1468+@book{automath,
1469+ title = {Selected Papers on Automath},
1470+ year = {1994},
1471+ editor = {S. Abramsky and J. Barwise and K. Fine and H.J. Keisler and A.S. Troelstr},
1472+ publisher = {North-Holland}
1473+}
1474+
1475+@misc{gimps,
1476+ howpublished = {http://www.mersenne.org/prime.htm},
1477+ title = {Great Internet Mersenne Prime Search}
1478+}
1479+
1480+@misc{haskell-report,
1481+ title = {Haskell 98 Language and Libraries --- The Revised Report},
1482+ year = {2002},
1483+ month = {December},
1484+ author = {Simon {Peyton Jones} and others},
1485+ howpublished = {Available from \verb+http://www.haskell.org/+}
1486+}
1487+
1488+@inproceedings{cayenne-{ICFP},
1489+ author = "Lennart Augustsson",
1490+ title = "Cayenne - a Language with Dependent Types",
1491+ booktitle = "Proc. 1998 International Conf. on Functional Programming ({ICFP} '98)",
1492+ pages = "239--250",
1493+ year = "1998",
1494+ url = "citeseer.nj.nec.com/augustsson98cayenne.html"
1495+}
1496+
1497+
1498+@misc{equality-cayenne,
1499+ howpublished = {\verb+http://www.cs.chalmers.se/~augustss/cayenne/+},
1500+ title = {Equality Proofs in Cayenne},
1501+ year = {1999},
1502+ author = {Lennart Augustsson}
1503+}
1504+
1505+@misc{interp-cayenne,
1506+ title = {An exercise in dependent types: A well-typed interpreter},
1507+ year = {1999},
1508+ author = {Lennart Augustsson and Magnus Carlsson}
1509+}
1510+
1511+@inproceedings{balaa00fixpoint,
1512+ title = {Fix-Point Equations for Well-Founded Recursion in Type Theory},
1513+ year = {2000},
1514+ booktitle = {Theorem Proving in Higher Order Logics},
1515+ pages = {1-16},
1516+ author = {Antonia Balaa and Yves Bertot}
1517+}
1518+
1519+@inproceedings{isabelle-maple,
1520+ title = {Theorems and algorithms: An interface between Isabelle and Maple},
1521+ year = {1995},
1522+ booktitle = {International Symposium on Symbolic and Algebraic Computation},
1523+ author = {Ballarin, C. and Homann, K., and Calmet, J.}
1524+}
1525+
1526+@book{barendregt-num,
1527+ title = {The Lambda Calculus, Its Syntax and Semantics},
1528+ year = {1984},
1529+ publisher = {North-Holland},
1530+ author = {Henk Barendregt}
1531+}
1532+
1533+@book{beiler,
1534+ title = {Recreations in the Theory of Numbers},
1535+ year = {1964},
1536+ publisher = {Dover},
1537+ author = {Albert H. Beiler}
1538+}
1539+
1540+@article{multidigit,
1541+ journal = {Advances in Applied Mathematics},
1542+ title = {Multidigit Multiplication for Mathematicians},
1543+ year = {1998},
1544+ author = {Daniel J. Bernstein}
1545+}
1546+
1547+@article{buhler-fox,
1548+ journal = {{ACM} Crossroads 2.1.},
1549+ month = {September},
1550+ title = {The Fox project: A language-structured approach to networking software.},
1551+ year = {1995},
1552+ author = {Buhler, J.},
1553+ note = {Available at http://www.{ACM}.org/crossroads/xrds2-1/foxnet.html}
1554+}
1555+
1556+@techreport{burstall91,
1557+ title = {Computer Assisted Proof for Mathematics: an Introduction Using the \textsc{Lego} Proof System},
1558+ year = {1991},
1559+ institution = {University of Edinburgh},
1560+ author = {Rod Burstall}
1561+}
1562+
1563+@article{plastic,
1564+ title = {An Implementation of {LF} with Coercive Subtyping and Universes},
1565+ author = {Paul Callaghan and Zhaohui Luo},
1566+ journal = {Journal of Automated Reasoning},
1567+ volume = {27},
1568+ number = {1},
1569+ pages = {3--27},
1570+ year = {2001}
1571+}
1572+
1573+@article{coercive,
1574+ title = {Coercive subtyping},
1575+ author = {Zhaohui Luo},
1576+ journal = {J. Logic Comput.},
1577+ volume = {9},
1578+ number = {1},
1579+ year = {1991},
1580+ pages = {105--130}
1581+}
1582+
1583+@inproceedings{calmet-homann,
1584+ title = {Classification of communication and cooperation mechanisms for logical and symbolic computation systems},
1585+ year = {1996},
1586+ booktitle = {Proceedings of the First International Workshop 'Frontiers of Combining S},
1587+ pages = {133-146},
1588+ publisher = {Kluwer},
1589+ author = {J. Calmet and K. Homann}
1590+}
1591+
1592+@techreport{comm-proofs,
1593+ title = {On Communicating Proofs in Interactive Mathematical Documents},
1594+ year = {2000},
1595+ institution = {Eindhoven University of Technology},
1596+ author = {Olga Caprotti and Martijn Oostdijk}
1597+}
1598+
1599+@article{prime2999,
1600+ title = {How to formally and efficiently prove Prime(2999)},
1601+ year = {2001},
1602+ author = {Olga Caprotti and Martijn Oostdijk},
1603+ journal = {Symbolic Computation and Automated Reasoning},
1604+ pages = {114--125}
1605+}
1606+
1607+@book{church-num,
1608+ title = {The Calculi of Lambda-Conversion},
1609+ year = {1941},
1610+ publisher = {Princeton University Press},
1611+ author = {Alonzo Church}
1612+}
1613+
1614+@book{nuprl86,
1615+ title = {Implementing Mathematics with the NuPrl Proof Development System},
1616+ year = {1986},
1617+ publisher = {Prentice-Hall},
1618+ address = {NJ},
1619+ author = {Constable, Robert L. and others}
1620+}
1621+
1622+@book{conway,
1623+ title = {On Numbers and Games},
1624+ year = {1976},
1625+ publisher = {Academic Press},
1626+ author = {J.H. Conway}
1627+}
1628+
1629+@misc{coq-manual,
1630+ howpublished = {\verb+http://coq.inria.fr/+},
1631+ title = {The {Coq} Proof Assistant --- Reference Manual},
1632+ year = {2009},
1633+ author = {{Coq Development Team}}
1634+}
1635+
1636+@misc{tt-prog,
1637+ month = {June},
1638+ title = {Type Theory and Programming},
1639+ year = {1994},
1640+ author = {Thierry Coquand and Bengt Nordstr\"{o}m and Jan M. Smith and Bj\"{o}rn von Sydow}
1641+}
1642+
1643+@book{func-appr,
1644+ title = {The Functional Approach to Programming},
1645+ year = {1998},
1646+ publisher = {Cambridge University Press},
1647+ author = {Guy Cousineau and Michel Mauny}
1648+}
1649+
1650+@misc{ibmspec,
1651+ howpublished = {http://www2.hursley.ibm.com/decimal/},
1652+ month = {January},
1653+ title = {Standard Decimal Arithmetic Specification},
1654+ year = {2001},
1655+ author = {Mike Cowlishaw},
1656+ note = {\copyright IBM Corporation 2001}
1657+}
1658+
1659+@book{dummett,
1660+ title = {Elements of Intuitionism},
1661+ year = {2000},
1662+ edition = {2nd},
1663+ publisher = {Oxford: Clarendon},
1664+ author = {Michael A.E. Dummet}
1665+}
1666+
1667+@article{dybjer94,
1668+ title = {Inductive Families},
1669+ year = {1994},
1670+ author = {Peter Dybjer},
1671+ journal = {Formal Aspects Of Computing},
1672+ volume = {6},
1673+ pages = {440--465}
1674+}
1675+
1676+@misc{octave,
1677+ howpublished = {http://www.octave.org/},
1678+ month = {February},
1679+ title = {GNU Octave -- A high-level interactive language for numerical computations},
1680+ year = {1997},
1681+ author = {John W. Eaton}
1682+}
1683+
1684+@book{comp-methods,
1685+ title = {Computing methods for scientists and engineers},
1686+ year = {1968},
1687+ publisher = {Oxford : Clarendon Press},
1688+ author = {L. Fox and D.F. Mayers}
1689+}
1690+
1691+@misc{guile,
1692+ howpublished = {http://www.gnu.org/software/guile/guile.html},
1693+ title = {Guile -- Project GNU's extension language},
1694+ year = {2001},
1695+ author = {{Free Software Foundation}}
1696+}
1697+
1698+@article{need-dep,
1699+ journal = {Journal of Functional Programming},
1700+ number = {4},
1701+ volume = {10},
1702+ title = {Do we need dependent types?},
1703+ year = {2000},
1704+ pages = {409-415},
1705+ author = {Daniel Fridlender and Mia Indrika}
1706+}
1707+
1708+@book{primes-programming,
1709+ title = {Primes and Programming -- An Introduction to Number Theory with Computing},
1710+ year = {1993},
1711+ publisher = {Cambridge University Press},
1712+ author = {Peter Giblin}
1713+}
1714+
1715+@misc{rec-coq,
1716+ month = {May},
1717+ title = {A Tutorial on Recursive Types in \textsc{Coq}},
1718+ year = {1998},
1719+ author = {Eduardo Gim\'{e}nez}
1720+}
1721+
1722+@article{goldberg91,
1723+ journal = {{ACM} Computing Surveys},
1724+ number = {1},
1725+ volume = {23},
1726+ title = {What every computer scientist should know about floating point arithmetic},
1727+ year = {1991},
1728+ pages = {5-48},
1729+ author = {D. Goldberg}
1730+}
1731+
1732+@article{binary-lambda,
1733+ journal = {Journal of Functional Programming},
1734+ number = {6},
1735+ volume = {10},
1736+ title = {An adequate and efficient left associated binary numeral system in the $\lambda$-calculus},
1737+ year = {2000},
1738+ author = {Mayer Goldberg}
1739+}
1740+
1741+@book{hol,
1742+ title = {Introduction to HOL},
1743+ year = {1993},
1744+ publisher = {Cambridge University Press},
1745+ author = {M. Gordon and T. Melham}
1746+}
1747+
1748+@misc{gmp,
1749+ howpublished = {Available from \verb+http://www.swox.com/gmp/manual/+},
1750+ title = {The {GNU Multiple Precision} Arithmetic Library 4.1.3 --- Manual},
1751+ year = {2004},
1752+ author = {Torbj\"{o}rn Granlund and others}
1753+}
1754+
1755+@article{harrison-fmsd94,
1756+ journal = {Formal Methods in System Design},
1757+ volume = {5},
1758+ title = {Constructing the Real Numbers in {HOL}},
1759+ year = {1994},
1760+ pages = {35--59},
1761+ author = {John Harrison}
1762+}
1763+
1764+@book{harrison-thesis,
1765+ title = {Theorem Proving with the Real Numbers},
1766+ year = {1998},
1767+ publisher = {Springer-Verlag},
1768+ author = {John Harrison}
1769+}
1770+
1771+@techreport{hol-maple,
1772+ title = {Reasing about the Reals: the marriage of HOL and Maple},
1773+ year = {1993},
1774+ institution = {University of Cambridge Computer Laboratory},
1775+ author = {John Harrison and Laurent Th\'{e}ry}
1776+}
1777+
1778+@misc{coq-tutorial,
1779+ howpublished = {http://pauillac.inria.fr/coq},
1780+ title = {The \textsc{Coq} Proof Assistant - A Tutorial},
1781+ author = {G\'{e}rard Huet and Gilles Kahn and Christine Paulin-Mohring}
1782+}
1783+
1784+@misc{restr-haskell,
1785+ howpublished = {http://citeseer.nj.nec.com/253599.html},
1786+ month = {September},
1787+ title = {Restricted Data Types in Haskell},
1788+ year = {1999},
1789+ author = {John Hughes}
1790+}
1791+
1792+@misc{javadec,
1793+ howpublished = {http://www2.hursley.ibm.com/decimalj/decimald.html},
1794+ month = {September},
1795+ title = {Decimal Arithmetic for Java -- a Proposal},
1796+ year = {2000},
1797+ author = {{IBM Corporation}}
1798+}
1799+
1800+@misc{ieee754,
1801+ title = {{IEEE} Standard for Binary Floating Point Arithmetic},
1802+ year = {1985},
1803+ author = {{IEEE Standard 754}}
1804+}
1805+
1806+@misc{ieee854,
1807+ title = {IEEE Standard for Radix-Independent Floating-Point Arithmetic},
1808+ year = {1987},
1809+ author = {{IEEE Standard 854}}
1810+}
1811+
1812+@inproceedings{jon91,
1813+ title = {Completing the Rational and Metric Spaces in \textsc{Lego}},
1814+ year = {1991},
1815+ booktitle = {Proceedings of the Second Workshop on Logical Frameworks},
1816+ author = {Claire Jones}
1817+}
1818+
1819+@misc{ typinghaskell,
1820+ author = "Mark Jones",
1821+ title = "Typing {Haskell} in {Haskell}",
1822+ howpublished = "In Haskell Workshop, September 1999.",
1823+ year = "1999",
1824+ url = "citeseer.ist.psu.edu/article/jones99typing.html" }
1825+
1826+@article{karatsuba,
1827+ journal = {Soviet Physics-Doklady},
1828+ volume = {7},
1829+ title = {Multiplication of multidigit numbers by automata},
1830+ year = {1963},
1831+ pages = {595--596},
1832+ author = {A. Karatsuba and Y. Ofman}
1833+}
1834+
1835+@book{knuth2,
1836+ volume = {2},
1837+ title = {The Art of Computer Programming - Seminumerical Algorithms},
1838+ year = {1969},
1839+ publisher = {Addison Wesley},
1840+ author = {Donald E. Knuth}
1841+}
1842+
1843+@article{next700,
1844+ journal = {Communications of the {ACM}},
1845+ number = {3},
1846+ month = {March},
1847+ volume = {9},
1848+ title = {The next 700 programming languages},
1849+ year = {1966},
1850+ author = {P.J. Landin}
1851+}
1852+
1853+@techreport{luo-spec,
1854+ month = {January},
1855+ title = {Program Specification and Data Refinement in Type Theory},
1856+ year = {1993},
1857+ institution = {Department of Computer Science, University of Edinburgh},
1858+ author = {Zhaohui Luo}
1859+}
1860+
1861+@phdthesis{luo90,
1862+ school = {University of Edinburgh},
1863+ title = {An Extended Calculus Of Constructions},
1864+ year = {1990},
1865+ author = {Zhaohui Luo}
1866+}
1867+
1868+@techreport{lego-manual,
1869+ title = {\textsc{Lego} Proof Development System: User's Manual},
1870+ year = {1992},
1871+ institution = {Department of Computer Science, University of Edinburgh},
1872+ author = {Zhaohui Luo and Robert Pollack}
1873+}
1874+
1875+@inproceedings{alf,
1876+ title = {The {ALF} proof editor and its proof engine},
1877+ year = {1994},
1878+ booktitle = {Formal Proceeding of the 1993 Workshop on Types for Proofs and Programs},
1879+ author = {Lena Magnusson and Bengt N\"{o}rdstrom}
1880+}
1881+
1882+@misc{happy,
1883+ howpublished = {http://www.haskell.org/happy/},
1884+ title = {Happy User Guide},
1885+ year = {2001},
1886+ author = {Simon Marlow and Andy Gill}
1887+}
1888+
1889+@inproceedings{generic-haskell,
1890+ title = {Generic Haskell, Specifically},
1891+ author = {Dave Clarke and Andres L\"{o}h},
1892+ editor = {Jeremy Gibbons and Johan Jeuring},
1893+ booktitle = {Proceedings of the IFIP TC2 Working Conference on Generic Programming},
1894+ year = {2002},
1895+ publisher = {Kluwer Academic Publishers},
1896+ pages = {21--48}
1897+}
1898+
1899+@article{faking-it,
1900+ title = {Faking It -- Simulating Dependent Types in {Haskell}},
1901+ year = {2002},
1902+ author = {Conor McBride},
1903+ journal = {Journal of Functional Programming},
1904+ volume = {12},
1905+ number = {4+5},
1906+ pages = {375--392}
1907+}
1908+
1909+@misc{mcbride-inverting,
1910+ title = {Inverting Inductively Defined Relations in \textsc{Lego}},
1911+ year = {1996},
1912+ author = {Conor McBride}
1913+}
1914+
1915+@phdthesis{mcbride-thesis,
1916+ month = {May},
1917+ school = {University of Edinburgh},
1918+ title = {Dependently Typed Functional Programs and their proofs},
1919+ year = {2000},
1920+ author = {Conor McBride}
1921+}
1922+
1923+@article{mcbride-unification,
1924+ title = {First-Order Unification by Structural Recursion},
1925+ year = {2003},
1926+ author = {Conor McBride},
1927+ journal = {Journal of Functional Programming},
1928+ volume = {13},
1929+ number = {6},
1930+ pages = {1061--1075}
1931+}
1932+
1933+@misc{mckinna-pollack,
1934+ howpublished = {Kluwer Academic Publishers},
1935+ title = {Some Lambda Calculus and Type Theory formalized},
1936+ year = {1998},
1937+ author = {James McKinna and Robert Pollack}
1938+}
1939+
1940+@book{num-theory,
1941+ title = {An Introduction to the Theory of Numbers},
1942+ year = {1980},
1943+ publisher = {John Wiley and Sons},
1944+ author = {Ivan Niven and Herbert S. Zuckerman}
1945+}
1946+
1947+@book{prog-mltt,
1948+ title = {Programming in Martin-L\"{o}f's Type Theory -- An Introduction},
1949+ year = {1990},
1950+ publisher = {Oxford University Press},
1951+ author = {Bengt Nordstr\"{o}m and Kent Petersson and Jan M. Smith},
1952+ note = {Out of print. Available from http://www.cs.chalmers.se/Cs/Research/Logic}
1953+}
1954+
1955+@book{okasaki,
1956+ title = {Purely Functional Data Structures},
1957+ year = {1998},
1958+ publisher = {Cambridge University Press},
1959+ author = {Chris Okasaki}
1960+}
1961+
1962+@book{arith-systems,
1963+ title = {Computer Arithmetic Systems},
1964+ year = {1994},
1965+ publisher = {Prentice-Hall},
1966+ author = {Amos R. Omondi}
1967+}
1968+
1969+@book{pj-imp,
1970+ title = {The Implementation of Functional Programming Languages},
1971+ year = {1987},
1972+ publisher = {Prentice-Hall},
1973+ author = {Simon {Peyton Jones}}
1974+}
1975+
1976+@book{cp-bjc,
1977+ title = {Computational Numerical Methods},
1978+ year = {1986},
1979+ publisher = {John Wiley and Sons},
1980+ author = {C. Phillips and B. Cornelius}
1981+}
1982+
1983+@book{nag,
1984+ title = {The NAG Library: a beginner's guide},
1985+ year = {1986},
1986+ publisher = {Oxford : Clarendon Press},
1987+ author = {Jen Phillips}
1988+}
1989+
1990+@misc{believe,
1991+ month = {September},
1992+ title = {How to Believe a Machine-Checked Proof},
1993+ year = {1996},
1994+ author = {Robert Pollack}
1995+}
1996+
1997+@phdthesis{pollack94,
1998+ school = {University of Edinburgh},
1999+ title = {The Theory of LEGO -- A Proof Checker for the Extended Calculus of Constructions},
2000+ year = {1994},
2001+ author = {Robert Pollack}
2002+}
2003+
2004+@inproceedings{intel-bug,
2005+ series = {LNCS},
2006+ volume = {915},
2007+ title = {Anatomy of the Pentium Bug},
2008+ publisher = {Springer-Verlag},
2009+ year = {1995},
2010+ pages = {97--107},
2011+ author = {V.R. Pratt}
2012+}
2013+
2014+@book{maple,
2015+ title = {The Maple Handbook: Maple V Release 4},
2016+ year = {1996},
2017+ publisher = {Springer},
2018+ author = {Darren Redfern}
2019+}
2020+
2021+@book{crypto,
2022+ title = {Applied Cryptography: protocols, algorithms and source code in C.},
2023+ year = {1996},
2024+ publisher = {Wiley},
2025+ author = {Bruce Schneier}
2026+}
2027+
2028+@article{adts,
2029+ journal = {Mathematical Structures in Computer Science},
2030+ number = {2},
2031+ volume = {10},
2032+ title = {On lists and other abstract data types in the calculus of construction},
2033+ year = {2000},
2034+ pages = {261-276},
2035+ author = {Jonathan P. Seldin}
2036+}
2037+
2038+@article{seldin97,
2039+ journal = {Annals of Pure and Applied Logic},
2040+ number = {1},
2041+ month = {January},
2042+ volume = {83},
2043+ title = {On the proof theory of Coquand's calculus of constructions},
2044+ year = {1997},
2045+ pages = {23--101},
2046+ author = {Jonathan P. Seldin}
2047+}
2048+
2049+@article{wichmann,
2050+ journal = {The Computer Journal},
2051+ volume = {32},
2052+ title = {Towards a Formal Specification of Floating Point},
2053+ year = {1989},
2054+ pages = {432-436},
2055+ author = {B.A. Wichmann}
2056+}
2057+
2058+@book{mathematica,
2059+ title = {Mathematica : a system for doing mathematics by computer},
2060+ year = {1991},
2061+ publisher = {Addison Wesley},
2062+ author = {Stephen Wolfram}
2063+}
2064+
2065+@inproceedings{xi-imp,
2066+author = "Hongwei Xi",
2067+title = {{Imperative Programming with Dependent Types}},
2068+booktitle = "Proceedings of 15th {IEEE} Symposium on Logic in Computer Science",
2069+year = 2000,
2070+month = "June",
2071+address = "Santa Barbara",
2072+pages = "375--387"
2073+}
2074+
2075+@phdthesis{xi-thesis,
2076+ month = {December},
2077+ school = {Department of Mathematical Sciences, Carnegie Mellon University},
2078+ title = {Dependent Types in Practical Programming},
2079+ year = {1998},
2080+ author = {Hongwei Xi}
2081+}
2082+
2083+
2084+@techreport{dtal,
2085+author = {Hongwei Xi and Robert Harper},
2086+title = {A Dependently Typed Assembly Language},
2087+institution = {Computer Science and Engineering Department, Oregon Graduate Institute},
2088+year = 1999,
2089+number = {OGI-CSE-99-008},
2090+month = {July},
2091+}
2092+
2093+@misc{bignum-cmp,
2094+ month = {February},
2095+ title = {Comparison of three public-domain multiprecision libraries: BigNum, Gmp and Pari},
2096+ year = {1998},
2097+ author = {Paul Zimmerman}
2098+}
2099+
2100+@book{perl,
2101+ title = {Programming Perl},
2102+ author = {Larry Wall and Tom Christiansen and Jon Orwant},
2103+ year = {2000},
2104+ edition = {3rd},
2105+ publisher = {O'Reilly}
2106+}
2107+
2108+@misc{python,
2109+ howpublished = {http://www.python.org/doc/current/tut/tut.html},
2110+ month = {April},
2111+ title = {Python Tutorial},
2112+ year = {2001},
2113+ author = {Guido van {Rossum} and Fred L. {Drake, Jr}}
2114+}
2115+
2116+@book{logic,
2117+ title = {The Language of First Order Logic},
2118+ year = {1992},
2119+ publisher = {CSLI Lecture Notes},
2120+ author = {Jon Barwise and John Etchemendy}
2121+}
2122+
2123+@book{haskell,
2124+ title = {Haskell -- The Craft of Functional Programming},
2125+ year = {1999},
2126+ publisher = {Addison Wesley},
2127+ author = {Simon Thompson}
2128+}
2129+
2130+@inproceedings{coq-hol,
2131+ title = {A Comparative Study of Coq and HOL},
2132+ year = {1997},
2133+ booktitle = {Theorem Proving in Higher Order Logics},
2134+ pages = {323-337},
2135+ author = {Vincent Zammit}
2136+}
2137+
2138+@misc{gay90,
2139+ month = {November},
2140+ title = {Correctly Rounded Binary-Decimal and Decimal-Binary Conversions},
2141+ year = {1990},
2142+ author = {David M. Gay},
2143+ note = {AT&T Bell Laboratories, Numerical Analysis Manuscript 90-10}
2144+}
2145+
2146+@article{hughes-matters,
2147+ journal = {Computer Journal},
2148+ number = {2},
2149+ volume = {32},
2150+ title = {Why Functional Programming Matters},
2151+ year = {1989},
2152+ pages = {98--107},
2153+ author = {J. Hughes}
2154+}
2155+
2156+@inproceedings{proofpointing,
2157+ title = {Proof by Pointing},
2158+ year = {1994},
2159+ booktitle = {Proceedings of the International Symposium on Theoretical Aspects of Computer So},
2160+ pages = {141--160},
2161+ editor = {M. Hagiya and J. C. Mitchell},
2162+ publisher = {Springer-Verlag},
2163+ series = {LNCS},
2164+ volume = {789},
2165+ address = {Sendai, Japan},
2166+ author = {Yves Bertot and Gilles Kahn and Laurent Th{\'e}ry}
2167+}
2168+
2169+@misc{inductive-coq,
2170+ month = {December},
2171+ title = {Inductive Definitions in the System Coq -- Rules and Properties},
2172+ year = {1992},
2173+ author = {Christine Paulin-Mohring}
2174+}
2175+
2176+@misc{leiserson98,
2177+ month = {July},
2178+ title = {Using de Bruijn Sequences to Index a 1 in a Computer Word},
2179+ year = {1998},
2180+ author = {{Charles E. Leiserson} and {Harald Prokop} and {Keith H. Randall}}
2181+}
2182+
2183+@inproceedings{proofchecking,
2184+ title = {A two-level approach towards lean proof-checking},
2185+ year = {1996},
2186+ booktitle = {TYPES},
2187+ pages = {16--35},
2188+ author = {G. Barthe and M.P.J. Ruys and H.P. Barendregt}
2189+}
2190+
2191+@inproceedings{congruence,
2192+ title = {Congruence Types},
2193+ year = {1995},
2194+ booktitle = {CSL},
2195+ pages = {36--51},
2196+ author = {Gilles Barthe and Herman Geuvers}
2197+}
2198+
2199+@phdthesis{geuvers-thesis,
2200+ title = {Logic and Type Systems},
2201+ author = {Herman Geuvers},
2202+ year = 1993,
2203+ school = {Katholieke Universiteit Nijmegen}
2204+}
2205+
2206+@techreport{multiple-values,
2207+ title = {Multiple Values in {Standard ML}},
2208+ year = {1994},
2209+ number = {94-312},
2210+ institution = {LFCS, Dept of Computer Science, University of Edinburgh},
2211+ author = {Kevin Mitchell}
2212+}
2213+
2214+@inproceedings{oracle-checking,
2215+ month = {January},
2216+ title = {Oracle-Based Checking of Untrusted Software},
2217+ year = {2001},
2218+ booktitle = {Proceedings of the 28th {ACM} Symposium on Principles of Programming Languages},
2219+ pages = {142--154},
2220+ author = {{George C. Necula} and {S.P. Rahul}}
2221+}
2222+
2223+@article{adams93jfp,
2224+ journal = {Journal of Functional Programming},
2225+ number = {4},
2226+ volume = {3},
2227+ title = {Efficient Sets -- A Balancing Act},
2228+ year = {1993},
2229+ pages = {553--561},
2230+ author = {Stephen Adams}
2231+}
2232+
2233+@inproceedings{hughes-sized,
2234+ title = {Proving the Correctness of Reactive Systems Using Sized Types},
2235+ year = {1996},
2236+ booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-SIGACT symposium on Principles of programmin},
2237+ pages = {410--423},
2238+ author = {John Hughes and Lars Pareto and Amr Sabry}
2239+}
2240+
2241+@inproceedings{whittle99ml,
2242+ title = {An {ML} Editor Based on Proofs-As-Programs},
2243+ year = {1999},
2244+ booktitle = {Automated Software Engineering},
2245+ pages = {166--173},
2246+ author = {Jon Whittle and Alan Bundy and Richard J. Boulton and Helen Lowe}
2247+}
2248+
2249+@book{efp-typeinf,
2250+ title = {Elements of Functional Programming},
2251+ year = {1989},
2252+ publisher = {Addison-Wesley},
2253+ author = {Chris Reade},
2254+ series = {International Computer Science Series}
2255+}
2256+
2257+@incollection{ wadler-views,
2258+ author = "Philip Wadler",
2259+ title = "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction",
2260+ booktitle = "Proceedings, 14th Symposium on Principles of Programming Languages",
2261+ publisher = "Association for Computing Machinery",
2262+ editor = "Steve Munchnik",
2263+ pages = "307--312",
2264+ year = "1987",
2265+ url = "citeseer.nj.nec.com/wadler87views.html" }
2266+
2267+@article{ coquand-checking,
2268+ author = "Thierry Coquand",
2269+ title = "An Algorithm for Type-Checking Dependent Types",
2270+ journal = "Science of Computer Programming",
2271+ volume = "26",
2272+ number = "1-3",
2273+ pages = "167-177",
2274+ year = "1996",
2275+ url = "citeseer.nj.nec.com/coquand96algorithm.html" }
2276+
2277+@misc{coquand-pm,
2278+ author = "Thierry Coquand",
2279+ title = "Pattern Matching with Dependent Types",
2280+ year = "1992",
2281+ howpublished = "Available from \verb+http://www.cs.chalmers.se/~coquand/type.html+"
2282+}
2283+
2284+@misc{pollack-records,
2285+ month = {August},
2286+ title = {Dependently Typed Records for Representing Mathematical Structure},
2287+ year = {2000},
2288+ author = {Robert Pollack}
2289+}
2290+
2291+@article{checking-betarte,
2292+ journal = {Journal of Functional Programming},
2293+ number = {2},
2294+ month = {March},
2295+ volume = {10},
2296+ title = {Type checking dependent (record) types and subtyping},
2297+ year = {2000},
2298+ pages = {137--166},
2299+ author = {Gustavo Betarte}
2300+}
2301+
2302+
2303+@article{ gcode,
2304+ author = "Thomas Johnsson",
2305+ title = "Efficient Compilation of Lazy Evaluation",
2306+ booktitle = "Proceedings of the {{ACM}} {{SIGPLAN}}'84 Symposium on Compiler Con struction",
2307+ journal = "{SIGPLAN} Notices",
2308+ volume = "19",
2309+ number = "6",
2310+ month = "June",
2311+ publisher = "{ACM} Press",
2312+ pages = "58--69",
2313+ year = "1984",
2314+ url = "citeseer.nj.nec.com/johnsson84efficient.html" }
2315+
2316+@misc{kamareddine01,
2317+ month = {February},
2318+ title = {Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems},
2319+ year = {2001},
2320+ author = {Fairouz Kamareddine}
2321+}
2322+
2323+@book{prooftheory,
2324+ title = {Basic Proof Theory},
2325+ year = {1996},
2326+ publisher = {Cambridge University Press},
2327+ author = {A.S. Troelstra and H. Schwichtenberg},
2328+ series = {Cambridge Tracts in Theoretical Computer Science}
2329+}
2330+
2331+@misc{nbe_staged,
2332+ title = {Integrating Normalization-by-Evaluation into a Staged Programming Language},
2333+ year = {1998},
2334+ author = {Tim Sheard}
2335+}
2336+
2337+@inproceedings{nbe2,
2338+ title = {Normalization by evaluation},
2339+ year = {1998},
2340+ author = {Ulrich Berger and Matthias Eberl and Helmut Schwichtenberg},
2341+ booktitle = {Prospects for Hardware Foundations 1998},
2342+ pages = {117--137},
2343+ series = {LNCS}
2344+}
2345+
2346+
2347+
2348+@misc{rtcg_jfp,
2349+ title = {Compiling for Run-time Code Generation},
2350+ year = {2000},
2351+ author = {Frederick Smith and Dan Grossman and Greg Morrisett and Luke Hornof and Trevor J},
2352+ note = {Under consideration for J. Functional Programming}
2353+}
2354+
2355+@phdthesis{fredsmith_thesis,
2356+ month = {January},
2357+ school = {Cornell University},
2358+ title = {Certified Run-time Code Generation},
2359+ year = {2002},
2360+ author = {Frederick Smith}
2361+}
2362+
2363+@inproceedings{xi_arraybounds,
2364+author = "Hongwei Xi and Frank Pfenning",
2365+title = {Eliminating Array Bound Checking through Dependent Types},
2366+booktitle = "Proceedings of {ACM} {SIGPLAN} Conference on Programming Language Design and Implementation",
2367+year = 1998,
2368+month = "June",
2369+address = "Montreal",
2370+pages = "249--257",
2371+}
2372+
2373+@inproceedings{xi_deadcode,
2374+author = "Hongwei Xi",
2375+title = {Dead Code Elimination through Dependent Types},
2376+booktitle = "The First International Workshop on Practical Aspects of Declarative Languages",
2377+year = 1999,
2378+month = "January",
2379+address = "San Antonio",
2380+pages = "228--242"
2381+}
2382+
2383+@book{compilers,
2384+ title = {Compilers --- Principles, Techniques and Tools},
2385+ year = {1986},
2386+ publisher = {Addison-Wesley},
2387+ author = {Alfred Aho and Ravi Sethi and Jeffrey Ullman}
2388+}
2389+
2390+@inproceedings{nhc,
2391+ title = {Highlights from nhc: A space efficient {Haskell} Compiler},
2392+ year = {1995},
2393+ author = "Niklas R{\"o}jemo",
2394+ booktitle = "Functional Programming Languages and Computer Architecture",
2395+ pages = "282--292"
2396+}
2397+
2398+
2399+@misc{mlmatch,
2400+ title = {SML/NJ Match Compiler Notes},
2401+ year = {1992},
2402+ author = {William Aitken}
2403+}
2404+
2405+@misc{mlmatch_sestoft,
2406+ title = {ML pattern match compilation and partial evaluation},
2407+ year = {1992},
2408+ author = {Peter Sestoft}
2409+}
2410+
2411+@inproceedings{compiledstrongreduction,
2412+ title = {A Compiled Implementation of Strong Reduction},
2413+ year = {2002},
2414+ author = {Benjamin Gr\'{e}goire and Xavier Leroy},
2415+ booktitle = {Proc. 2002 International Conf. on Functional Programming ({ICFP} 2002)},
2416+ pages = {235--246}
2417+}
2418+
2419+@misc{tclhaskell,
2420+ howpublished = {http://www.dcs.gla.ac.uk/~meurig/TclHaskell/usermanual.html},
2421+ month = {August},
2422+ title = {TclHaskell - User Manual},
2423+ year = {1999},
2424+ author = {Meurig Sage}
2425+}
2426+
2427+
2428+@InProceedings{nbe-cat,
2429+ author = "Thorsten Altenkirch and Martin Hofmann and Thomas Streicher",
2430+ title = "Categorical reconstruction of a reduction free
2431+ normalization proof",
2432+ year = "1995",
2433+ booktitle = "Category Theory and Computer Science",
2434+ editor = {David Pitt and David E. Rydeheard and Peter Johnstone},
2435+ series = {LNCS},
2436+ volume = {953},
2437+ pages = {182-199}
2438+}
2439+
2440+@inproceedings{presburgerEFSM,
2441+ title = {A Comparison of Presburger Engines for EFSM Reachability},
2442+ year = {1998},
2443+ booktitle = {Computer Aided Verification '98},
2444+ pages = {280--292},
2445+ author = {Thomas R. Shiple and James H. Kukula and Rajeev K. Ranjan}
2446+}
2447+
2448+@misc{typesafecast,
2449+ title = {Type-Safe Cast},
2450+ year = {2000},
2451+ author = {Stephanie Weirich}
2452+}
2453+
2454+@phdthesis{grobauer-thesis,
2455+ school = {University of Aarhus},
2456+ title = {Topics in Semantics Based Program Manipulation},
2457+ year = {2001},
2458+ author = {Bernd Grobauer}
2459+}
2460+
2461+@misc{monads-moggi,
2462+ title = {Computational Lambda Calculus and Monads},
2463+ year = {1989},
2464+ author = {Eugenio Moggi}
2465+}
2466+
2467+@article{gmp-proof,
2468+ title = {A proof of {GMP} square root},
2469+ year = {2002},
2470+ journal = {Journal of Automated Reasoning},
2471+ volume = {29},
2472+ pages = {225--252},
2473+ author = {Yves Bertot and Nicolas Magaud and Paul Zimmerman}
2474+}
2475+
2476+@article{F-tal,
2477+ journal = {{ACM} Transactions on Programming Languages and Systems},
2478+ number = {3},
2479+ month = {May},
2480+ volume = {21},
2481+ title = {From {System F} to Typed Assembly Language},
2482+ year = {1999},
2483+ pages = {528--569},
2484+ author = {Greg Morrisett and David Walker and Karl Crary and Neal Glew}
2485+}
2486+
2487+@techreport{nbe-rtcg,
2488+ month = {December},
2489+ title = {Strong Normalization by Type-Directed Partial Evaluation and Run-Time Code Generation},
2490+ year = {1997},
2491+ institution = {BRICS},
2492+ author = {Vincent Balat and Oliver Danvy}
2493+}
2494+
2495+@misc{yong-schemata,
2496+ howpublished = {http://www.dur.ac.uk/yong.luo/},
2497+ title = {A Methodology for Implementing Inductive Schemata},
2498+ year = {2002},
2499+ author = {Yong Luo and Zhaohui Luo}
2500+}
2501+
2502+@inproceedings{harper93,
2503+ title = {Explicit Polymorphism and CPS Conversion},
2504+ year = {1993},
2505+ booktitle = {20th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
2506+ pages = {206--219},
2507+ publisher = {{ACM} Press, New York, NY, USA},
2508+ author = {Robert Harper and Mark Lillibridge}
2509+}
2510+
2511+@techreport{backends,
2512+ month = {November},
2513+ title = {Functional Back-Ends within the Lambda-Sigma Calculus},
2514+ year = {1996},
2515+ institution = {INRIA},
2516+ author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
2517+}
2518+
2519+@article{stg,
2520+ title = {Implementing lazy functional languages on stock hardware -- the {Spineless Tagless G-machine}},
2521+ year = {1992},
2522+ journal = {Journal of Functional Programming},
2523+ volume = {2},
2524+ number = {2},
2525+ pages = {127--202},
2526+ month = {April},
2527+ author = {Simon {Peyton Jones}}
2528+}
2529+
2530+@article{debruijn,
2531+ journal = {Indagationes Mathematicae},
2532+ volume = {34},
2533+ title = {Lambda calculus notation with nameless dummies},
2534+ year = {1972},
2535+ pages = {381--392},
2536+ author = {N.G. de Bruijn}
2537+}
2538+
2539+@book{assembly,
2540+ month = {January},
2541+ title = {PC Assembly Language},
2542+ year = {2002},
2543+ publisher = {http://www.drpaulcarter.com/},
2544+ author = {Paul A. Carter}
2545+}
2546+
2547+@inproceedings{poly99,
2548+ title = {Once Upon A Polymorphic Type},
2549+ year = {1999},
2550+ booktitle = {26th {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
2551+ publisher = {{ACM}},
2552+ author = {Keith Wansbrough and Simon {Peyton Jones}}
2553+}
2554+
2555+@misc{lazy_intro,
2556+ title = {Compiling Lazy Functional Languages: An introduction},
2557+ year = {1986},
2558+ author = {Thomas Johnsson}
2559+}
2560+
2561+@inproceedings{unboxed-fp,
2562+ month = {Sept},
2563+ title = {Unboxed Values as First Class Citizens in a Non-Strict Functional Language},
2564+ year = {1991},
2565+ author = {Simon {Peyton Jones} and John Launchbury},
2566+ booktitle = {Functional Programming Languages and Computer Architecture (FPCA'91)},
2567+ crossref = {fplca91},
2568+ pages = {636--666}
2569+}
2570+
2571+@inproceedings{abc-machine,
2572+ author = {Sjaak Smetsers and Eric N{\"{o}}cker and John {van Groningen} and Rinus Plasmeijer},
2573+ title = {Generating efficient code for lazy functional languages},
2574+ booktitle = {Functional programming Languages and Computer Architecture},
2575+ year = {1991},
2576+ pages = {592--617},
2577+ crossref = {fplca91}
2578+}
2579+
2580+@proceedings{fplca91,
2581+ title = {Functional programming Languages and Computer Architecture},
2582+ year = {1991},
2583+ volume = {523},
2584+ series = {LNCS},
2585+ publisher = {Springer-Verlag},
2586+ editor = {John Hughes}
2587+}
2588+
2589+
2590+
2591+@inproceedings{nbe,
2592+ title = {An inverse of the evaluation functional for typed $\lambda$-calculus},
2593+ year = {1991},
2594+ booktitle = {Proc. 1991 {IEEE} Symp. on Logic in Comp. Sci.},
2595+ pages = {203--211},
2596+ editor = {R. Vemuri},
2597+ author = {Ulrich Berger and Helmut Schwichtenberg}
2598+}
2599+
2600+@inproceedings{typed-closure,
2601+ title = {Typed Closure Conversion},
2602+ year = {1996},
2603+ booktitle = {Symposium on Principles of Programming Languages},
2604+ pages = {271--283},
2605+ author = {Yasuhiko Minamide and J. Gregory Morrisett and Robert Harper}
2606+}
2607+
2608+@misc{ghc-commentary,
2609+ howpublished = {http://www.cse.unsw.edu.au/~chak/haskell/ghc/comm/},
2610+ title = {The Glasgow Haskell Compiler (GHC) Commentary},
2611+ year = {2002},
2612+ author = {Manuel M. T. Chakravarty and Sigbjorn Finne and Simon Marlow and Simon {Peyton Jones} and Julian Seward and Reuben Thomas},
2613+ note = {Available from GHC CVS repository}
2614+}
2615+
2616+@inproceedings{lambdalift,
2617+ month = {September},
2618+ title = {Lambda Lifting: Transforming Programs to Recursive Equations},
2619+ year = {1985},
2620+ booktitle = {Functional Programming Languages and Computer Architecture},
2621+ pages = {190--203},
2622+ editor = {Jean-Pierre Jouannaud},
2623+ publisher = {Springer-Verlag},
2624+ author = {Thomas Johnsson}
2625+}
2626+
2627+@inproceedings{til,
2628+ title = {TIL: A Type-Directed Optimizing Compiler for ML},
2629+ year = {1996},
2630+ booktitle = {Proc. {{ACM}} {{SIGPLAN}} '96 Conference on Programming Language Design and Implementation},
2631+ pages = {181--192},
2632+ author = {D. Tarditi and G. Morrisett and P. Cheng and C. Stone and R. Harper and P. Lee}
2633+}
2634+
2635+@phdthesis{shao94,
2636+ school = {Princeton University},
2637+ title = {Compiling Standard {ML} for Efficient Execution on Modern Machines},
2638+ year = {1994},
2639+ author = {Zhong Shao}
2640+}
2641+
2642+@inproceedings{gmachine,
2643+ month = {September},
2644+ title = {The {G-Machine}: A fast, graph-reduction evaluator},
2645+ year = {1985},
2646+ booktitle = {Functional Programming Languages and Computer Architecture},
2647+ pages = {400--413},
2648+ editor = {Jean-Pierre Jouannaud},
2649+ publisher = {Springer-Verlag},
2650+ author = {R.B. Kieburtz}
2651+}
2652+
2653+@inproceedings{strictness,
2654+ month = {September},
2655+ title = {Strictness Analysis - A practical approach},
2656+ year = {1985},
2657+ booktitle = {Functional Programming Languages and Computer Hardware},
2658+ pages = {35--49},
2659+ editor = {Jean-Pierre Jouannaud},
2660+ publisher = {Springer-Verlag},
2661+ author = {Chris Clack and Simon {Peyton Jones}}
2662+}
2663+
2664+@book{fl-impl,
2665+ title = {Implementing Functional Languages - A Tutorial},
2666+ year = {1992},
2667+ publisher = {Prentice Hall International},
2668+ author = {Simon {Peyton Jones} and David Lester}
2669+}
2670+
2671+@phdthesis{capretta-thesis,
2672+ school = {Katholieke Universiteit Nijmegen},
2673+ title = {Abstraction and Computation},
2674+ year = {2002},
2675+ author = {Venanzio Capretta}
2676+}
2677+
2678+@article{bird-pointer,
2679+ journal = {Journal of Functional Programming},
2680+ number = {3},
2681+ month = {May},
2682+ volume = {11},
2683+ title = {Unfolding Pointer Algorithms},
2684+ year = {2001},
2685+ pages = {347--358},
2686+ author = {Richard S. Bird}
2687+}
2688+
2689+@article{impl-tp,
2690+ journal = {Journal of Functional Programming},
2691+ number = {2},
2692+ month = {March},
2693+ volume = {9},
2694+ title = {Implementing Theorem Provers in a Purely Functional Style},
2695+ year = {1999},
2696+ pages = {147--166},
2697+ author = {Keith Hanna}
2698+}
2699+
2700+@article{shrink-lambda,
2701+ journal = {Journal of Functional Programming},
2702+ number = {5},
2703+ month = {September},
2704+ volume = {7},
2705+ title = {Shrinking Lambda Expressions in Linear Time},
2706+ year = {1997},
2707+ pages = {515--540},
2708+ author = {Andrew W. Appel and Trevor Jim}
2709+}
2710+
2711+@article{stack-tal,
2712+ journal = {Journal of Functional Programming},
2713+ number = {1},
2714+ month = {January},
2715+ volume = {12},
2716+ title = {Stack-based Typed Assembly Language},
2717+ year = {2002},
2718+ pages = {43--88},
2719+ author = {Greg Morrisset and Karl Crart and Neal Glew and David Walker}
2720+}
2721+
2722+@article{runtime-lamsig,
2723+ journal = {Journal of Functional Programming},
2724+ number = {2},
2725+ month = {March},
2726+ volume = {8},
2727+ title = {Functional Runtime Systems within the lambda-sigma Calculus},
2728+ year = {1998},
2729+ pages = {131--176},
2730+ author = {Th\'{e}r\`{e}se Hardin and Luc Maranget and Bruno Pagano}
2731+}
2732+
2733+@article{busylazy,
2734+ journal = {Journal of Functional Programming},
2735+ number = {6},
2736+ month = {November},
2737+ volume = {11},
2738+ title = {How to look busy while being as lazy as ever: the Implementation of a lazy functional debugger},
2739+ year = {2001},
2740+ pages = {629--671},
2741+ author = {Henrik Nilsson}
2742+}
2743+
2744+@article{lazyveager,
2745+ journal = {Journal of Functional Programming},
2746+ number = {5},
2747+ month = {September},
2748+ volume = {7},
2749+ title = {More haste, less speed: lazy versus eager evaluation},
2750+ year = {1997},
2751+ pages = {541--547},
2752+ author = {Richard Bird and Geraint Jones and Oege {de Moor}}
2753+}
2754+
2755+@article{jvm-fp,
2756+ journal = {Journal of Functional Programming},
2757+ number = {6},
2758+ month = {November},
2759+ volume = {9},
2760+ title = {Compiling lazy functional programs for the Java Virtual Machine},
2761+ year = {1999},
2762+ pages = {579--603},
2763+ author = {David Wakeling}
2764+}
2765+
2766+@book{isabelle,
2767+ publisher = {Springer-Verlag},
2768+ series = {LNCS},
2769+ volume = {2283},
2770+ month = {March},
2771+ title = {Isabelle/HOL - A proof assistant for higher order logic},
2772+ year = {2002},
2773+ author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}
2774+}
2775+
2776+@article{ghc-inliner,
2777+ journal = {Journal of Functional Programming},
2778+ number = {4},
2779+ month = {September},
2780+ volume = {12},
2781+ title = {Secrets of the {Glasgow Haskell Compiler} inliner},
2782+ year = {2002},
2783+ pages = {393--434},
2784+ author = {Simon {Peyton Jones} and Simon Marlow}
2785+}
2786+
2787+@article{dynamic-fp,
2788+ journal = {Journal of Functional Programming},
2789+ number = {1},
2790+ month = {January},
2791+ volume = {8},
2792+ title = {The dynamic compiliation of lazy functional programs},
2793+ year = {1998},
2794+ pages = {61--81},
2795+ author = {David Wakeling}
2796+}
2797+
2798+@misc{isabelle-ref,
2799+ month = {March},
2800+ title = {Isabelle Reference Manual},
2801+ year = {2002},
2802+ author = {Lawrence C. Paulson}
2803+}
2804+
2805+@article{debruijn-nested,
2806+ journal = {Journal of Functional Programming},
2807+ number = {1},
2808+ month = {January},
2809+ volume = {9},
2810+ title = {de Bruijn notation as a nested datatype},
2811+ year = {1999},
2812+ pages = {77--91},
2813+ author = {Richard S. Bird and Ross Paterson}
2814+}
2815+
2816+@article{perfect-trees,
2817+ journal = {Journal of Functional Programming},
2818+ number = {3},
2819+ month = {May},
2820+ volume = {10},
2821+ title = {Perfect trees and bit-reversal permutations},
2822+ year = {2000},
2823+ pages = {305--317},
2824+ author = {Ralf Hinze}
2825+}
2826+
2827+@phdthesis{paulin-extraction,
2828+ school = {Paris 7},
2829+ title = {Extraction de programmes dans le Calcul des Constructions},
2830+ year = {1989},
2831+ author = {Christine Paulin-Mohring}
2832+}
2833+
2834+@phdthesis{santos95,
2835+ school = {University of Glasgow},
2836+ title = {Compilation By Transformation In Non-Strict Functional Languages},
2837+ year = {1995},
2838+ author = {{Andr\'{e} Lu\'{i}s de Medeiros} Santos}
2839+}
2840+
2841+@book{cps,
2842+ title = {Compiling With Continuations},
2843+ year = {1992},
2844+ publisher = {Cambridge University Press},
2845+ author = {Andrew W. Appel}
2846+}
2847+
2848+@techreport{SKIM,
2849+ number = {31},
2850+ title = {The {SKIM} microprogrammer's guide},
2851+ year = {1983},
2852+ institution = {University of Cambridge},
2853+ author = {W.R. Stoye}
2854+}
2855+
2856+@misc{NORMA,
2857+ title = {An Overview of Burroughs {NORMA}},
2858+ year = {1985},
2859+ author = {H. Richards}
2860+}
2861+
2862+@book{ml,
2863+ title = {The Definition of Standard ML --- Revised},
2864+ year = {1997},
2865+ publisher = {MIT Press},
2866+ author = {Robin Milner and Mads Tofte and Robert Harper and David MacQueen}
2867+}
2868+
2869+@misc{ml71,
2870+ title = {An intuitionistic theory of types},
2871+ year = {1971},
2872+ author = {Per Martin-L\"{o}f}
2873+}
2874+
2875+@phdthesis{girard-thesis,
2876+ school = {Universit\'{e} Paris VII},
2877+ title = {Interpr\'{e}tation fonctionelle et \'{e}limination des coupures de l'arithm\'{e}tique d'ordre sup\'{e}rieur},
2878+ year = {1972},
2879+ author = {Jean-Yves Girard}
2880+}
2881+
2882+@inproceedings{ml75,
2883+ title = {An intuitionistic theory of types: predicative part},
2884+ year = {1975},
2885+ booktitle = {Logic Colloquium '73},
2886+ editor = {H. Rose and J.C. Shepherdson},
2887+ publisher = {North-Holland},
2888+ author = {Per Martin-L\"{o}f}
2889+}
2890+
2891+@inproceedings{cpm90,
2892+ title = {Inductively defined types},
2893+ year = {1990},
2894+ author = {Thierry Coquand and Christine Paulin-Mohring},
2895+ series = {LNCS},
2896+ volume = {417},
2897+ publusher = {Springer-Verlag}
2898+}
2899+
2900+@phdthesis{fpcustom,
2901+ month = {May},
2902+ school = {Computer Lab, University of Cambridge},
2903+ title = {The Implementation of Functional Languages using Custom Hardware},
2904+ year = {1985},
2905+ author = {W.R. Stoye}
2906+}
2907+
2908+@phdthesis{hughesthesis,
2909+ month = {September},
2910+ school = {Programming Research Group, Oxford},
2911+ title = {The design and implementation of programming languages},
2912+ year = {1984},
2913+ author = {John Hughes}
2914+}
2915+
2916+@inproceedings{tim,
2917+ volume = {274},
2918+ title = {{TIM} -- A simple lazy abstract machine to execute supercombinators},
2919+ year = {1987},
2920+ booktitle = {Functional Programming Languages and Computer Architecture},
2921+ publisher = {Springer-Verlag},
2922+ author = {John Fairbairn and Stuart Wray},
2923+ pages = {34--45},
2924+ series = {LNCS}
2925+}
2926+
2927+@techreport{abc,
2928+ title = {The {ABC} machine -- A Sequential Stack-based Abstract Machine For Graph Rewriting},
2929+ year = {1990},
2930+ institution = {University of Nijmegen},
2931+ 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}
2932+}
2933+
2934+@techreport{implicit,
2935+ title = {On Implicit Arguments},
2936+ year = {1994},
2937+ institution = {Faculty of Science, University of Tokyo},
2938+ author = {Masami Hagiya and Yozo Toda}
2939+}
2940+
2941+@book{semantics,
2942+ title = {Denotational Semantics},
2943+ year = {1986},
2944+ publisher = {Wm. C. Brown},
2945+ author = {David A. Schmidt}
2946+}
2947+
2948+@inproceedings{lazyml,
2949+ month = {August},
2950+ title = {A compiler for {Lazy} {ML}},
2951+ year = {1984},
2952+ booktitle = {Proceedings of the {{ACM}} Symposium on Lisp and Functional Programming},
2953+ pages = {218--227},
2954+ author = {Lennart Augustsson}
2955+}
2956+
2957+@inproceedings{nu-g,
2958+ title = {Parallel graph reduction with the $\langle\nu,G\rangle$-machine},
2959+ year = {1989},
2960+ booktitle = {Functional Programming Languages and Computer Architecture},
2961+ publisher = {{ACM} Press},
2962+ author = {Lennart Augustsson and Thomas Johnsson}
2963+}
2964+
2965+@book{k&r,
2966+ title = {The C programming language},
2967+ year = {1988},
2968+ publisher = {Prentice-Hall},
2969+ author = {Brian W. Kernighan and Dennis M. Ritchie}
2970+}
2971+
2972+@misc{c--garbage,
2973+ title = {C--: a portable assembly language that supports garbage collection},
2974+ year = {1999},
2975+ author = {Simon {Peyton Jones} and Norman Ramsey and Fermin Reig},
2976+ note = {Invited talk at PPDP'99}
2977+}
2978+
2979+@misc{epigram,
2980+ howpublished = {http://www.dur.ac.uk/CARG/epigram.html},
2981+ title = {Project Proposal: {Epigram}: Innovative Programming via Inductive Families},
2982+ year = {2002},
2983+ author = {Zhaohui Luo and James McKinna and Paul Callaghan and Conor McBride}
2984+}
2985+
2986+@misc{ghc-rewrite,
2987+ title = {Playing by the Rules: Rewriting as a practical optimisation technique in {GHC}},
2988+ year = {2001},
2989+ author = {Simon {Peyton Jones} and Andrew Tolmach and Tony Hoare}
2990+}
2991+
2992+@UNPUBLISHED{implicit-pollack,
2993+ AUTHOR = {Robert Pollack},
2994+ TITLE = {Implicit Syntax},
2995+ NOTE = {Informal Proceedings of First Workshop on
2996+ Logical Frameworks, Antibes},
2997+ YEAR = {1990},
2998+ MONTH = MAY
2999+}
3000+
3001+
3002+@article{transform-haskell,
3003+ journal = {Science of Computer Programming},
3004+ volume = {32},
3005+ title = {A transformation-based optimiser for {Haskell}},
3006+ year = {1998},
3007+ pages = {3--47},
3008+ author = {Simon {Peyton Jones} and Andr\'{e} L. M. Santos}
3009+}
3010+
3011+@inproceedings{knuth-bendix,
3012+ title = {Simple Word Problems in Universal Algebras},
3013+ year = {1970},
3014+ booktitle = {Computational Problems in Abstract Algebra},
3015+ pages = {263--298},
3016+ editor = {John Leech},
3017+ publisher = {Pergamon Press},
3018+ author = {Donald E. Knuth and Peter B. Bendix}
3019+}
3020+
3021+@inproceedings{phantomfun,
3022+ title = {Fun With Phantom Types},
3023+ author = {Ralf Hinze},
3024+ pages = {245--262},
3025+ year = {2003},
3026+ crossref = {funprogramming},
3027+ booktitle = {The Fun Of Programming},
3028+ publisher = {Palgrave}
3029+}
3030+
3031+@book{funprogramming,
3032+ month = {March},
3033+ title = {The Fun Of Programming},
3034+ year = {2003},
3035+ editor = {Jeremy Gibbons and Oege {de Moor}},
3036+ publisher = {Palgrave},
3037+ series = {Cornerstones of Computing}
3038+}
3039+
3040+@inproceedings{anderson-proof,
3041+ title = {Representing Proof Transformations For Program Optimization},
3042+ year = {1994},
3043+ booktitle = {International Conference On Automated Deduction},
3044+ publisher = {Springer Verlag},
3045+ author = {Penny Anderson}
3046+}
3047+
3048+@phdthesis{daria-thesis,
3049+ month = {April},
3050+ school = {Institute of Informatics, Warsaw University},
3051+ title = {Termination of Rewriting in the Calculus of Constructions},
3052+ year = {2003},
3053+ author = {Daria Walukiewicz-Chrzaszcz}
3054+}
3055+
3056+@inproceedings{change-data,
3057+ title = {Changing Data Structures In Type Theory: A Study Of Natural Numbers},
3058+ year = {2001},
3059+ booktitle = {Types For Proofs And Programs 2000},
3060+ pages = {181--196},
3061+ editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
3062+ publisher = {Springer},
3063+ author = {Nicolas Magaud and Yves Bertot}
3064+}
3065+
3066+@phdthesis{nico-thesis,
3067+ title = {Changement de Representation des donn\'{e}es dans le Calcul de Constructions},
3068+ author = {Nicolas Magaud},
3069+ year = {2003},
3070+ month = {October},
3071+ school = {Universit\'{e} de Nice - Sophia Antipolis}
3072+}
3073+
3074+
3075+@book{patterns,
3076+ title = {Design Patterns},
3077+ year = {1995},
3078+ publisher = {Addison Wesley},
3079+ author = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides}
3080+}
3081+
3082+@misc{ghchugs,
3083+ month = {August},
3084+ title = {The New {GHC}/{Hugs} Runtime System},
3085+ year = {1998},
3086+ author = {Simon Marlow and Simon {Peyton Jones}}
3087+}
3088+
3089+@misc{stgrevised,
3090+ month = {February},
3091+ title = {The {STG} runtime system (revised)},
3092+ year = {1999},
3093+ author = {Simon {Peyton Jones} and Simon Marlow and Alastair Reid},
3094+ howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
3095+}
3096+
3097+@inproceedings{optimistic,
3098+ month = {March},
3099+ title = {Optimistic Evaluation --- an adaptive evaluation strategy for non-strict programs},
3100+ year = {2003},
3101+ author = {Robert Ennals and Simon {Peyton Jones}},
3102+ booktitle = {International Conference on Functional Programming},
3103+ pages = {287--298}
3104+}
3105+
3106+@phdthesis{ennals-thesis,
3107+ title = {Adaptive Evaluation of Non-Strict Programs},
3108+ author = {Robert Ennals},
3109+ year = {2003},
3110+ month = {December},
3111+ school = {King's College, University of Cambridge}
3112+}
3113+
3114+@article{garbage,
3115+ journal = {{ACM} Computing Surveys},
3116+ number = {3},
3117+ volume = {13},
3118+ title = {Garbage Collection of Linked Data Structures},
3119+ year = {1981},
3120+ pages = {341--367},
3121+ author = {Jacques Cohen}
3122+}
3123+
3124+@article{baker-gc,
3125+ journal = {Communications of the {ACM}},
3126+ number = {4},
3127+ month = {April},
3128+ volume = {21},
3129+ title = {List Processing In Real Time On A Serial Computer},
3130+ year = {1978},
3131+ pages = {280--294},
3132+ author = {Henry G. {Baker Jr}}
3133+}
3134+
3135+@misc{bc-rec,
3136+ month = {February},
3137+ title = {Modelling General Recursion in Type Theory},
3138+ year = {2003},
3139+ note = {Under consideration for publication in Math. Struct. in Comp. Science. Draft, DCS, CTH --- INRIA, Sophia Antipolis, France},
3140+ author = {Ana Bove and Venanzio Capretta}
3141+}
3142+
3143+@misc{global-tag,
3144+ title = {Global Tagging Optimization by Type Inference},
3145+ year = {1992},
3146+ author = {Fritz Henglein}
3147+}
3148+
3149+@book{esr,
3150+ month = {October},
3151+ title = {The Cathedral And The Bazaar},
3152+ year = {1999},
3153+ publisher = {O'Reilly},
3154+ author = {Eric Raymond}
3155+}
3156+
3157+@book{manmonth,
3158+ title = {The Mythical Man-month: Essays on Software Engineering},
3159+ year = {1975},
3160+ publisher = {Addison Wesley},
3161+ author = {Frederick P. Brooks}
3162+}
3163+
3164+@inproceedings{evalpush,
3165+ title = {How to make a fast curry: push/enter vs eval/apply},
3166+ year = {2004},
3167+ author = {Simon Marlow and Simon {Peyton Jones}},
3168+ booktitle = {International Conference on Functional Programming, Snowbird},
3169+ pages = {4--15}
3170+}
3171+
3172+@phdthesis{boquist-thesis,
3173+ month = {April},
3174+ school = {Chalmers University of Technology},
3175+ title = {Code Optimisation Techniques for Lazy Functional Languages},
3176+ year = {1999},
3177+ author = {Urban Boquist}
3178+}
3179+
3180+@book{formal-spec,
3181+ title = {Formal Specification Of Programming Languages},
3182+ year = {1981},
3183+ publisher = {Prentice-Hall},
3184+ author = {Frank G. Pagan}
3185+}
3186+
3187+@inproceedings{elim-motive,
3188+ title = {Elimination With A Motive},
3189+ year = {2000},
3190+ booktitle = {Types for Proofs and Programs},
3191+ pages = {197--216},
3192+ editor = {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
3193+ publisher = {Springer},
3194+ author = {Conor McBride}
3195+}
3196+
3197+@article{telescope,
3198+ journal = {Information and Computation},
3199+ number = {2},
3200+ month = {April},
3201+ volume = {91},
3202+ title = {Telescoping Mappings in Typed Lambda Calculus},
3203+ year = {1991},
3204+ pages = {189--204},
3205+ author = {N.G. de Bruijn}
3206+}
3207+
3208+@misc{typeintype,
3209+ title = {Typechecking is undecidable when 'type' is a type},
3210+ year = {1989},
3211+ author = {Mark B. Reinhold}
3212+}
3213+
3214+@misc{core,
3215+ month = {September},
3216+ title = {An External Representation for the {GHC} Core Language},
3217+ year = {2001},
3218+ author = {Andrew Tolmach and {The GHC Team}}
3219+}
3220+
3221+@article{deforestation,
3222+ journal = {Theoretical Computer Science},
3223+ volume = {73},
3224+ title = {Deforestation: Transforming programs to eliminate trees},
3225+ year = {1990},
3226+ pages = {231--248},
3227+ author = {Philip Wadler}
3228+}
3229+
3230+@misc{hep,
3231+ month = {July},
3232+ title = {Architecture of the {Haskell} Execution Platform},
3233+ year = {1999},
3234+ author = {Julian Seward and Simon Marlow and Andy Gill and Sigbjorn Finne and Simon {Peyton Jones} },
3235+ note = {Version 6},
3236+ howpublished = {Available from \verb+http://www.haskell.org/ghc/documentation.html+}
3237+}
3238+
3239+@mastersthesis{wahlstedt-thesis,
3240+ month = {October},
3241+ school = {Chalmers University Of Technology},
3242+ title = {Detecting Termination Using Size Change In Parameter Values},
3243+ year = {2000},
3244+ author = {David Wahlstedt}
3245+}
3246+
3247+@inproceedings{size-change,
3248+ title = {The size-change principle for program termination},
3249+ year = {2001},
3250+ booktitle = {Proceedings of the 28th Annual {ACM} {SIGPLAN}-SIGACT Symposium on Principles of Programming Languages},
3251+ author = {Chin Soon Lee and Neil D. Jones and Amir Ben-Amram. }
3252+}
3253+
3254+@article{ski-turner,
3255+ journal = {Software -- Practice and Experience},
3256+ volume = {9},
3257+ title = {A new implementation technique for applicative languages},
3258+ year = {1979},
3259+ pages = {31--49},
3260+ author = {David Turner}
3261+}
3262+
3263+@inproceedings{turner-strong,
3264+ number = {1022},
3265+ title = {Elementary Strong Functional Programming},
3266+ year = {1996},
3267+ booktitle = {First International Symposium on Functional Programming Languages in Education, Nijmegen, Netherlands, December 1995.},
3268+ pages = {1--13},
3269+ publisher = {Springer},
3270+ author = {David Turner},
3271+ series = {LNCS}
3272+}
3273+
3274+@misc{clean,
3275+ title = {The {Concurrent CLEAN} Language Report (draft)},
3276+ year = {2003},
3277+ author = {Rinus Plasmeijer and Marko van Eekelen},
3278+ howpublished = {Available from \verb+http://www.cs.kun.nl/~clean/+}
3279+}
3280+
3281+@article{burstall-struct,
3282+ journal = {Computer Journal},
3283+ number = {1},
3284+ volume = {12},
3285+ title = {Proving Properties of Programs By Structural Induction},
3286+ year = {1969},
3287+ pages = {41--48},
3288+ author = {Rod Burstall}
3289+}
3290+
3291+@incollection{ barendregt-types,
3292+ author = "Henk Barendregt",
3293+ title = "Lambda Calculi with Types",
3294+ booktitle = "Handbook of Logic in Computer Science, Volumes 1 (Background: Mathematical Structures) and 2 (Background: Computational Structures), Abramsky \& Gabbay \& Maibaum (Eds.)",
3295+ publisher = "Clarendon",
3296+ volume = "2",
3297+ year = "1992",
3298+ url = "citeseer.nj.nec.com/barendregt92lambda.html" }
3299+
3300+@book{curry-feys,
3301+ title = {Combinatory Logic, volume 1},
3302+ year = {1958},
3303+ publisher = {North Holland},
3304+ author = {Haskell B. Curry and Robert Feys}
3305+}
3306+
3307+@phdthesis{bove-thesis,
3308+ month = {November},
3309+ school = {Chalmers University of Technology},
3310+ title = {General Recursion in Type Theory},
3311+ year = {2002},
3312+ author = {Ana Bove}
3313+}
3314+
3315+@inbook{ml-cm,
3316+ title = {Constructive Mathematics and Computer Programming},
3317+ year = {1985},
3318+ booktitle = {Mathematical Logic and Programming Languages},
3319+ publisher = {Prentice Hall},
3320+ author = {Per Martin-L\"{o}f}
3321+}
3322+
3323+@inproceedings{howard,
3324+ title = {The formulae-as-types notion of construction},
3325+ year = {1980},
3326+ booktitle = {To H.B.Curry: Essays on combinatory logic, lambda calculus and formalism},
3327+ editor = {Jonathan P. Seldin and J. Roger Hindley},
3328+ publisher = {Academic Press},
3329+ author = {William A. Howard},
3330+ note = {A reprint of an unpublished manuscript from 1969}
3331+}
3332+
3333+@inproceedings{talx86,
3334+ title = {TALx86: A Realistic Typed Assembly Language},
3335+ year = {1999},
3336+ booktitle = {{ACM} {SIGPLAN} Workshop on Compiler Support for System Software},
3337+ pages = {25--35},
3338+ 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}
3339+}
3340+
3341+@inproceedings{bove-capretta,
3342+ volume = {2152},
3343+ title = {Nested General Recursion and Partiality in Type Theory},
3344+ year = {2001},
3345+ booktitle = {Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLS 2001},
3346+ pages = {121--135},
3347+ editor = {Richard J. Boulton and Paul B. Jackson},
3348+ publisher = {Springer-Verlag},
3349+ author = {Ana Bove and Venanzio Capretta},
3350+ series = {LNCS}
3351+}
3352+
3353+@misc{lvm,
3354+ month = {November},
3355+ title = {LVM, the lazy virtual machine},
3356+ year = {2002},
3357+ author = {Daan Leijen}
3358+}
3359+
3360+@misc{ocaml,
3361+ howpublished = {\verb+http://caml.inria.fr/ocaml/htmlman/+},
3362+ month = {August},
3363+ title = {The {Objective Caml} system release 3.06},
3364+ year = {2002},
3365+ author = {Xavier Leroy}
3366+}
3367+
3368+@misc{lambdagoto,
3369+ title = {Lambda : The Ultimate Goto},
3370+ year = {1977},
3371+ author = {Guy L. {Steele Jr}},
3372+ note = {MIT AI Memo 443}
3373+}
3374+
3375+@inproceedings{ liu-tail,
3376+ author = "Yanhong A. Liu and Scott D. Stoller",
3377+ title = "From Recursion to Iteration: What are the Optimizations?",
3378+ booktitle = "Partial Evaluation and Semantic-Based Program Manipulation",
3379+ pages = "73-82",
3380+ year = "2000",
3381+ url = "citeseer.nj.nec.com/liu00from.html" }
3382+
3383+@inproceedings{aczel77,
3384+ title = {An Introduction To Inductive Definitions},
3385+ year = {1977},
3386+ booktitle = {Handbook of Mathematical Logic},
3387+ editor = {J. Barwise},
3388+ publisher = {North Holland},
3389+ author = {Peter Aczel}
3390+}
3391+
3392+@inproceedings{inductive-plastic,
3393+ volume = {1956},
3394+ title = {Implementation Techniques for Inductive Types in {Plastic}},
3395+ year = {1999},
3396+ booktitle = {Types for Proofs and Programs},
3397+ pages = {94--113},
3398+ editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith},
3399+ publisher = {Springer-Verlag},
3400+ author = {Paul Callaghan and Zhaohui Luo},
3401+ series = {LNCS}
3402+}
3403+
3404+@misc{graham,
3405+ howpublished = {Available from \verb+http://www.paulgraham.com/+},
3406+ month = {April},
3407+ title = {The Hundred Year Language},
3408+ year = {2003},
3409+ author = {Paul Graham},
3410+ note = {Keynote address at PyCon 2003}
3411+}
3412+
3413+@inproceedings{gimenez98,
3414+ volume = {1443},
3415+ title = {Structural Recursive Definitions in Type Theory},
3416+ year = {1998},
3417+ booktitle = {Proceedings of ICALP '98},
3418+ publisher = {Springer-Verlag},
3419+ author = {Eduardo Gim\'{e}nez},
3420+ series = {LNCS}
3421+}
3422+
3423+@article{quicksort,
3424+ journal = {Computer Journal},
3425+ number = {1},
3426+ volume = {5},
3427+ title = {Quicksort},
3428+ year = {1962},
3429+ pages = {10--15},
3430+ author = {C.A.R. Hoare}
3431+}
3432+
3433+@phdthesis{goguen-thesis,
3434+ school = {University of Edinburgh},
3435+ title = {A Typed Operational Semantics for Type Theory},
3436+ year = {1994},
3437+ author = {Healfdene Goguen}
3438+}
3439+
3440+@article{ph-universes,
3441+ journal = {Theoretical Computer Science},
3442+ number = {1},
3443+ volume = {89},
3444+ title = {Type Checking With Universes},
3445+ year = {1991},
3446+ pages = {107--136},
3447+ author = {Robert Harper and Randy Pollack}
3448+}
3449+
3450+@inproceedings{pm-compile,
3451+ month = {September},
3452+ title = {Compiling Pattern Matching},
3453+ year = {1985},
3454+ booktitle = {Functional Programming Languages and Computer Architecture},
3455+ pages = {368--381},
3456+ editor = {Jean-Pierre Jouannaud},
3457+ publisher = {Springer-Verlag},
3458+ author = {Lennart Augustsson}
3459+}
3460+
3461+@phdthesis{lena-thesis,
3462+ school = {Chalmers University of Technology, G\"{o}teborg},
3463+ title = {The implementation of {ALF} -- A Proof Editor based on {Martin-L\"{o}f}'s Monomorphic Type Theory with Explicit Substitutions},
3464+ year = {1994},
3465+ author = {Lena Magnusson}
3466+}
3467+
3468+@article{view-left,
3469+ journal = {Journal of Functional Programming},
3470+ number = {1},
3471+ volume = {14},
3472+ title = {The View From The Left},
3473+ year = {2004},
3474+ author = {Conor McBride and James McKinna},
3475+ pages = {69--111}
3476+}
3477+
3478+@inproceedings{not-a-number,
3479+ author = {Conor McBride and James McKinna},
3480+ title = {I am not a number, {I} am a free variable},
3481+ year = {2004},
3482+ booktitle = {Proceedings of the {ACM} {SIGPLAN} Haskell Workshop}
3483+}
3484+
3485+
3486+@misc{profiling,
3487+ title = {Time and Space Profiling for Non-Strict, Higher Order Functional Languages},
3488+ year = {1995},
3489+ author = {Patrick M. Sansom and Simon {Peyton Jones}}
3490+}
3491+
3492+@inbook{pattern-matching,
3493+ title = {The Implementation of Functional Programming Languages},
3494+ year = {1987},
3495+ booktitle = {The Implementation of Functional Programming Languages},
3496+ pages = {78--103},
3497+ editor = {Simon {Peyton Jones}},
3498+ chapter = {5},
3499+ publisher = {Prentice Hall},
3500+ author = {Philip Wadler},
3501+ crossref = {pj-imp}
3502+}
3503+
3504+@article{pe-problems,
3505+ author = {Jones, N. D.},
3506+ title = {Challenging problems in partial evaluation and mixed computation},
3507+ journal = {New Gen. Comput.},
3508+ volume = {6},
3509+ number = {2-3},
3510+ year = {1988},
3511+ issn = {0288-3635},
3512+ pages = {291--302},
3513+ doi = {http://dx.doi.org/10.1007/BF03037143},
3514+ publisher = {Ohmsha},
3515+ address = {Tokyo, Japan, Japan},
3516+ }
3517+
3518+@inproceedings{tag-elim,
3519+ title = {Tag Elimination -- or -- Type Specialisation is a Type Indexed Effect},
3520+ year = {2000},
3521+ booktitle = {Subtyping and Dependent Types in Programming, APPSEM Workshop},
3522+ author = {Walid Taha and Henning Makholm}
3523+}
3524+
3525+@inproceedings{extraction-coq,
3526+ title = {A New Extraction for {Coq}},
3527+ year = {2002},
3528+ booktitle = {Types for proofs and programs},
3529+ editor = {Herman Geuvers and Freek Wiedijk},
3530+ publisher = {Springer},
3531+ author = {Pierre Letouzey},
3532+ series = {LNCS}
3533+}
3534+
3535+@phdthesis{mcbride-snr-thesis,
3536+ school = {Queen's University of Belfast},
3537+ title = {Computer Aided Manipulation of Symbols},
3538+ year = {1970},
3539+ author = {Fred McBride}
3540+}
3541+
3542+@article{ho-strictness,
3543+ journal = {Science of Computer Programming},
3544+ volume = {7},
3545+ title = {Strictness analysis for higher-order functions},
3546+ year = {1986},
3547+ pages = {249--278},
3548+ author = { Geoffrey L. Burn and Chris Hankin and Samson Abramsky}
3549+}
3550+
3551+@phdthesis{mycroft-thesis,
3552+ school = {Dept Computer Science, University of Edinburgh},
3553+ title = {Abstract interpretation and optimising transformations for applicative programs},
3554+ year = {1981},
3555+ author = {A. Mycroft}
3556+}
3557+
3558+@inproceedings{bc-nested,
3559+ month = {September},
3560+ volume = {2152},
3561+ title = {Nested General Recursion and Partiality in Type Theory},
3562+ year = {2001},
3563+ booktitle = {Theorem Proving In Higher Order Logics: 14th International Conferences, TPHOLS 2001},
3564+ pages = {121--135},
3565+ publisher = {Springer--Verlag},
3566+ author = {Ana Bove and Venanzio Capretta},
3567+ series = {LNCS}
3568+}
3569+
3570+@techreport{bove-mutual,
3571+ month = {May},
3572+ title = {Mutual General Recursion in Type Theory},
3573+ year = {2002},
3574+ institution = {Department of Computing Science, Chalmers University of Technology},
3575+ author = {Ana Bove}
3576+}
3577+
3578+@article{berardi-pruning,
3579+ journal = {Journal of Logic and Computation},
3580+ number = {5},
3581+ volume = {6},
3582+ title = {Pruning Simply Typed Lambda Terms},
3583+ year = {1996},
3584+ pages = {663--681},
3585+ author = {Stefano Berardi}
3586+}
3587+
3588+@article{milner-tc,
3589+ journal = {Journal of Computer and System Science},
3590+ volume = {17},
3591+ title = {A Theory of Type Polymorphism in Programming},
3592+ year = {1978},
3593+ pages = {348--75},
3594+ author = {R. Milner}
3595+}
3596+
3597+@inproceedings{extt,
3598+ title = {Inductive Families Need Not Store Their Indices},
3599+ year = {2004},
3600+ booktitle = {Types for Proofs and Programs 2003},
3601+ author = {Edwin Brady and Conor McBride and James McKinna},
3602+ editor = {Stefano Berardi and Mario Coppo and Ferruccio Damiani},
3603+ series = {Lecture Notes in Computer Science},
3604+ publisher = {Springer},
3605+ volume = {3085},
3606+ pages = {115--129}
3607+}
3608+
3609+@book{luo94,
3610+ title = {Computation and Reasoning -- A Type Theory for Computer Science},
3611+ year = {1994},
3612+ publisher = {OUP},
3613+ author = {Zhaohui Luo},
3614+ series = {Intl. Series of Monographs on Comp. Sci.}
3615+}
3616+
3617+@article{backus78,
3618+ journal = {Communications of the {ACM}},
3619+ month = {August},
3620+ volume = {21},
3621+ title = {Can Programming Be Liberated From the {Von Neumann} Style?},
3622+ year = {1978},
3623+ pages = {280--294},
3624+ author = {John Backus}
3625+}
3626+
3627+@misc{henk,
3628+ month = {May},
3629+ title = {Henk: A Typed Intermediate Language},
3630+ year = {1997},
3631+ author = {Simon {Peyton Jones} and Erik Meijer}
3632+}
3633+
3634+@article{thunks,
3635+ journal = {Journal of Functional Programming},
3636+ number = {3},
3637+ month = {May},
3638+ volume = {7},
3639+ title = {Thunks and the $\lambda$-calculus},
3640+ year = {1997},
3641+ pages = {303--319},
3642+ author = {John Hatcliff and Olivier Danvy}
3643+}
3644+
3645+@inproceedings{grin-project,
3646+ author = "Urban Boquist and Thomas Johnsson",
3647+ title = "The {GRIN} Project: A Highly Optimising Back End for Lazy Functional Languages",
3648+ booktitle = "Implementation of Functional Languages",
3649+ pages = "58--84",
3650+ year = "1996",
3651+ url = "citeseer.ist.psu.edu/boquist96grin.html" }
3652+
3653+@misc{boehm-gc,
3654+ nothowpublished = {\url{http://www.hpl.hp.com/personal/Hans_Boehm/gc/}},
3655+ title = {A garbage collector for {C} and {C++}},
3656+ year = {2001},
3657+ author = {Hans-J. Boehm and Alan J. Demers and {Xerox Corporation Silicon Graphic} and {Hewlett-Packard Company}}
3658+}
3659+
3660+@misc{art-interpreter,
3661+ month = {May},
3662+ title = {The Art of the Interpreter or, the Modularity Complex (Parts Zero, One, and Two)},
3663+ year = {1978},
3664+ author = {Guy Lewis {Steele, Jr.} and Gerald Jay Sussman},
3665+ note = {MIT AI Lab. AI Lab Memo AIM-453}
3666+}
3667+
3668+@inproceedings{gimenez,
3669+ title = {Codifying Guarded Definitions With Recursive Schemes},
3670+ year = {1994},
3671+ booktitle = {Proceedings of TYPES 1994},
3672+ pages = {39--59},
3673+ author = {Eduardo Gim\'{e}nez}
3674+}
3675+
3676+@manual{ghc-manual,
3677+ title = {The Glasgow Haskell Compiler User's Guide, Version 6.0},
3678+ year = {2003},
3679+ author = {The {GHC Team}}
3680+}
3681+
3682+@article{rbtree,
3683+ journal = {Journal of Functional Programming},
3684+ number = {4},
3685+ month = {May},
3686+ volume = {9},
3687+ title = {Red-Black Trees In A Functional Setting},
3688+ year = {1999},
3689+ pages = {471--477},
3690+ author = {Chris Okasaki}
3691+}
3692+
3693+@inproceedings{dt-data,
3694+author = "Hongwei Xi",
3695+title = {{Dependently Typed Data Structures}},
3696+booktitle = "Proceedings of Workshop of Algorithmic Aspects of Advanced Programming Languages (WAAAPL '99)",
3697+year = 1999,
3698+month = "September",
3699+pages = "17--32",
3700+address = "Paris",
3701+}
3702+
3703+@misc{krivine,
3704+ title = {On the Correctness and Efficiency of the {Krivine} Machine},
3705+ year = {2003},
3706+ month = {October},
3707+ author = {Mitchell Wand and Daniel P. Friedman},
3708+ howpublished = {Submitted for publication}
3709+ }
3710+
3711+@inproceedings{nbe-filinski,
3712+ title = {Normalization by Evaluation for the Computational Lambda-Calculus},
3713+ year = {2001},
3714+ month = {May},
3715+ booktitle = {Typed Lambda Calculi and Applications: 5th International Conference, TLCA 2001},
3716+ author = {Andrzej Filinski},
3717+ pages = {151--165},
3718+ publisher = {Springer-Verlag},
3719+ series = {LNCS},
3720+ volume = {2044}
3721+}
3722+
3723+@inproceedings{filinski-nbesem,
3724+ title = {A semantic account of type-directed partial evaluation},
3725+ year = {1999},
3726+ author = {Andrzej Filinski},
3727+ editor = {G. Nadathur},
3728+ booktitle = {International Conference on Principles and Practice of Declarative Programming},
3729+ volume = {1702},
3730+ series = {LNCS},
3731+ pages = {378--395},
3732+ publisher = {Springer-Verlag}
3733+}
3734+
3735+@article{secd,
3736+ title = {The mechanical evaluation of expressions},
3737+ author = {P.J. Landin},
3738+ year = {1964},
3739+ journal = {Computer Journal},
3740+ volume = {6},
3741+ pages = {308--320}
3742+}
3743+
3744+@misc{lispkit,
3745+ title = {The {LispKit} Manual},
3746+ author = {Peter Henderson and Geraint Jones and Simon Jones},
3747+ year = {1982},
3748+ howpublished = {Oxford University Computing Laboratory}
3749+}
3750+
3751+@inproceedings{wells-undecidable,
3752+ title = {Typability and Type Checking in the Second-order $\lambda$-calculus are equivalent and undecidable},
3753+ author = {J. Wells},
3754+ year = {1994},
3755+ month = {July},
3756+ booktitle = {Proc. 9th Ann. {IEEE} Symp. Logic Comput. Sci.}
3757+}
3758+
3759+@misc{patguards,
3760+ title = {Pattern Guards and Transformational Patterns},
3761+ author = {Martin Erwig and Simon {Peyton Jones}},
3762+ year = {2000},
3763+ howpublished = {Haskell Workshop}
3764+}
3765+
3766+@misc{alfa-manual,
3767+ title = {Alfa Users' Guide},
3768+ author = {Thomas Hallgren},
3769+ year = {2001},
3770+ howpublished = {Available from \verb+http://www.cs.chalmers.se/~hallgren/Alfa/+}
3771+}
3772+
3773+@inproceedings{nofib,
3774+ title = {The nofib Benchmark Suite of {Haskell} Programs},
3775+ author = {Will Partain},
3776+ year = {1992},
3777+ booktitle = {Functional Programming},
3778+ editor = {J. Launchbury and P.L. Sansom},
3779+ series = {Workshops in Computing},
3780+ publisher = {Springer Verlag}
3781+}
3782+
3783+@article{shape,
3784+ title = {Shape in Computing},
3785+ author = {Barry Jay},
3786+ journal = "{{ACM}} Computing Surveys",
3787+ year = "1996",
3788+ volume = "28",
3789+ number = "2",
3790+ pages = "355--357",
3791+}
3792+
3793+@misc{ffi,
3794+ title = {The {Haskell 98} Foreign Function Interface 1.0: An Addendum to the {Haskell 98} Report},
3795+ editor = {Manuel Chakravarty},
3796+ key = {FFI},
3797+ year = {2002},
3798+ month = {December},
3799+ howpublished = {Available from \verb+http://www.haskell.org/+}
3800+}
3801+
3802+@misc{perlxs,
3803+ title = {Perl {XS} Reference Manual},
3804+ author = {Dean Roehrich and {The Perl Porters}},
3805+ year = {1996},
3806+ howpublished = {\verb+http://www.perldoc.com/perl5.6/pod/perlxs.html+}
3807+}
3808+
3809+@misc{swig,
3810+ title = {{SWIG} : An Easy to Use Tool for Integrating Scripting Languages with {C} and {C++}},
3811+ author = {David M. Beazley},
3812+ year = {1996},
3813+ howpublished = {\verb+http://www.swig.org/papers/Tcl96/tcl96.html+}
3814+}
3815+
3816+@inproceedings{types-prog,
3817+ title = {Type Systems for Programming Languages},
3818+ booktitle = {Handbook of Theoretical Computer Science},
3819+ author = {John C. Mitchell},
3820+ pages = {365--458},
3821+ year = {1990},
3822+ crossref = {htcs}
3823+}
3824+
3825+@book{htcs,
3826+ title = {Handbook of Theoretical Computer Science},
3827+ editor = {J. van Leeuwen},
3828+ publisher = {Elsevier Science},
3829+ year = {1990}
3830+}
3831+
3832+@misc{r5rs,
3833+ title = {Revised$^5$ Report on the Algorithmic Language Scheme},
3834+ author = {Richard Kelsey and William Clinger and Jonathan Rees},
3835+ year = {1998},
3836+ month = {February},
3837+ howpublished = {Available from \verb+http://www.schemers.org/+}
3838+ }
3839+
3840+@misc{gmail-outage,
3841+ title = {Update on today's {Gmail} Outage},
3842+ author = {{Official Gmail Blog}},
3843+ howpublished = {\url{http://gmailblog.blogspot.com/2009/02/update-on-todays-gmail-outage.html}},
3844+ note = {Retrieved 26th February 2009},
3845+ year = 2009
3846+}