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