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