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