adam@310
|
1 @Book{TAPL,
|
adam@310
|
2 author = "Benjamin C. Pierce",
|
adam@310
|
3 title = "Types and Programming Languages",
|
adam@310
|
4 year = "2002",
|
adam@310
|
5 publisher = "MIT Press"
|
adam@310
|
6 }
|
adam@310
|
7
|
adam@310
|
8 @Book{CAR,
|
adam@310
|
9 author = "Matt Kaufmann and Panagiotis Manolios and J Strother Moore",
|
adam@310
|
10 title = "Computer-Aided Reasoning: An Approach",
|
adam@310
|
11 year = "2000",
|
adam@310
|
12 publisher = "Kluwer Academic Publishers"
|
adam@310
|
13 }
|
adam@310
|
14
|
adam@310
|
15 @Article{AMD,
|
adam@310
|
16 author = {J Strother Moore and Tom Lynch and Matt Kaufmann},
|
adam@310
|
17 title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
|
adam@310
|
18 journal = {IEEE Transactions on Computers},
|
adam@310
|
19 volume = {47(9)},
|
adam@464
|
20 pages = {913--926},
|
adam@310
|
21 year = {1998}
|
adam@310
|
22 }
|
adam@310
|
23
|
adam@310
|
24 @Book{Piton,
|
adam@310
|
25 author={J Strother Moore},
|
adam@310
|
26 title = {Piton: A Mechanically Verified Assembly-Level Language},
|
adam@310
|
27 year = "1996",
|
adam@310
|
28 series = "Automated Reasoning Series",
|
adam@310
|
29 publisher = "Kluwer Academic Publishers"
|
adam@310
|
30 }
|
adam@310
|
31
|
adam@310
|
32 @Article{Nqthm,
|
adam@310
|
33 title = {The {Boyer-Moore} Theorem Prover and Its Interactive Enhancement},
|
adam@310
|
34 author = {Robert S. Boyer and Matt Kaufmann and J Strother Moore},
|
adam@310
|
35 journal = {Computers and Mathematics with Applications},
|
adam@310
|
36 volume = {29(2)},
|
adam@310
|
37 year = {1995},
|
adam@310
|
38 pages = {27--62}
|
adam@310
|
39 }
|
adam@310
|
40
|
adam@310
|
41 @Article{4C,
|
adam@310
|
42 author = {Gonthier, Georges},
|
adam@310
|
43 year = {2008},
|
adam@310
|
44 title = {Formal Proof--The Four-Color Theorem},
|
adam@310
|
45 journal = {Notices of the American Mathematical Society},
|
adam@310
|
46 volume = {55(11)},
|
adam@434
|
47 pages = {1382--1393}
|
adam@310
|
48 }
|
adam@310
|
49
|
adam@310
|
50 @Article{CompCert,
|
adam@310
|
51 author = {Leroy, Xavier},
|
adam@310
|
52 year = {2009},
|
adam@310
|
53 title = {A formally verified compiler back-end},
|
adam@310
|
54 journal = {Journal of Automated Reasoning},
|
adam@310
|
55 volume = {43(4)},
|
adam@310
|
56 pages = {363--446}
|
adam@310
|
57 }
|
adam@310
|
58
|
adam@310
|
59 @InProceedings{seL4,
|
adam@310
|
60 author = {Gerwin Klein
|
adam@310
|
61 and Kevin Elphinstone
|
adam@310
|
62 and Gernot Heiser
|
adam@310
|
63 and June Andronick
|
adam@310
|
64 and David Cock
|
adam@310
|
65 and Philip Derrin
|
adam@310
|
66 and Dhammika Elkaduwe
|
adam@310
|
67 and Kai Engelhardt
|
adam@310
|
68 and Rafal Kolanski
|
adam@310
|
69 and Michael Norrish
|
adam@310
|
70 and Thomas Sewell
|
adam@310
|
71 and Harvey Tuch
|
adam@310
|
72 and Simon Winwood},
|
adam@310
|
73 title = {{seL4}: Formal Verification of an {OS} Kernel},
|
adam@310
|
74 booktitle = {Proceedings of the 22nd {ACM Symposium on Operating Systems Principles}},
|
adam@310
|
75 year = {2009},
|
adam@310
|
76 }
|
adam@310
|
77
|
adam@310
|
78 @Book{Isabelle/HOL,
|
adam@310
|
79 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
|
adam@310
|
80 title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
|
adam@310
|
81 publisher = {Springer},
|
adam@310
|
82 series = {Lecture Notes in Computer Science},
|
adam@310
|
83 volume = 2283,
|
adam@310
|
84 year = 2002
|
adam@310
|
85 }
|
adam@310
|
86
|
adam@310
|
87 @Book{Isabelle,
|
adam@310
|
88 author = {Paulson, Lawrence C.},
|
adam@310
|
89 year = {1994},
|
adam@310
|
90 title = {Isabelle: A Generic Theorem Prover},
|
adam@310
|
91 series = {Lecture Notes in Computer Science},
|
adam@310
|
92 volume = {828},
|
adam@310
|
93 publisher = {Springer}
|
adam@310
|
94 }
|
adam@310
|
95
|
adam@310
|
96 @Book{CoqArt,
|
adam@310
|
97 author = "Bertot, Yves and Cast\'eran, Pierre",
|
adam@310
|
98 title = "Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions",
|
adam@310
|
99 series = "Texts in Theoretical Computer Science",
|
adam@310
|
100 year = "2004",
|
adam@310
|
101 publisher = "Springer Verlag",
|
adam@310
|
102 }
|
adam@310
|
103
|
adam@310
|
104 @unpublished{CoqManual,
|
adam@310
|
105 author = "{Coq Development Team}",
|
adam@434
|
106 title = "The {Coq} proof assistant reference manual, version 8.4",
|
adam@434
|
107 year = 2012,
|
adam@310
|
108 url={http://coq.inria.fr/refman/}
|
adam@310
|
109 }
|
adam@311
|
110
|
adam@311
|
111 @inproceedings{CIC,
|
adam@311
|
112 author = {Christine Paulin-Mohring},
|
adam@311
|
113 title = {Inductive Definitions in the System {Coq} - Rules and Properties},
|
adam@311
|
114 year = {1993},
|
adam@311
|
115 booktitle = {Proceedings of the International Conference on {Typed Lambda Calculi and Applications}},
|
adam@311
|
116 }
|
adam@311
|
117
|
adam@311
|
118 @inproceedings{SetsInTypes,
|
adam@311
|
119 author = {Benjamin Werner},
|
adam@311
|
120 title = {Sets in Types, Types in Sets},
|
adam@311
|
121 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
|
adam@311
|
122 year = {1997},
|
adam@311
|
123 }
|
adam@311
|
124
|
adam@311
|
125 @article{CoC,
|
adam@311
|
126 author = {Thierry Coquand and G\'erard Huet},
|
adam@311
|
127 title = {The {Calculus} of {Constructions}},
|
adam@311
|
128 journal = {Information and Computation},
|
adam@311
|
129 volume = {76(2-3)},
|
adam@311
|
130 year = {1988}
|
adam@311
|
131 }
|
adam@312
|
132
|
adam@315
|
133 @inproceedings{GADT,
|
adam@312
|
134 author = {Hongwei Xi and Chiyan Chen and Gang Chen},
|
adam@312
|
135 title = {Guarded Recursive Datatype Constructors},
|
adam@312
|
136 booktitle = {Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages},
|
adam@312
|
137 year = {2003}
|
adam@312
|
138 }
|
adam@315
|
139
|
adam@315
|
140 @article{Curry,
|
adam@315
|
141 title={Functionality in Combinatory Logic},
|
adam@315
|
142 author = {H. B. Curry},
|
adam@315
|
143 journal = {Proceedings of the National Academy of Sciences of the United States of America},
|
adam@315
|
144 volume = {20(11)},
|
adam@315
|
145 year = {1934},
|
adam@315
|
146 pages = {584--590}
|
adam@315
|
147 }
|
adam@315
|
148
|
adam@315
|
149 @incollection{Howard,
|
adam@315
|
150 author = {Howard, William A.},
|
adam@315
|
151 title = {The formulae-as-types notion of construction},
|
adam@315
|
152 editor = {Seldin, Jonathan P. and Hindley, J. Roger},
|
adam@315
|
153 booktitle = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
|
adam@315
|
154 publisher = {Academic Press},
|
adam@315
|
155 pages = {479--490},
|
adam@315
|
156 year = {1980},
|
adam@315
|
157 note = {Original paper manuscript from 1969}
|
adam@315
|
158 }
|
adam@316
|
159
|
adam@316
|
160 @inproceedings{HOAS,
|
adam@316
|
161 author = {Pfenning, F. and Elliot, C.},
|
adam@316
|
162 title = {Higher-order abstract syntax},
|
adam@316
|
163 booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
|
adam@316
|
164 year = {1988},
|
adam@464
|
165 % pages = {199--208},
|
adam@316
|
166 }
|
adam@317
|
167
|
adam@317
|
168 @article{HOU,
|
adam@317
|
169 author = {G\'erard Huet},
|
adam@317
|
170 title = {The undecidability of unification in third order logic},
|
adam@317
|
171 journal = {Information and Control},
|
adam@317
|
172 voluem = {22(3)},
|
adam@317
|
173 year = {1973},
|
adam@317
|
174 pages = {257--267}
|
adam@317
|
175 }
|
adam@328
|
176
|
adam@328
|
177 @InBook{TAPLNatDed,
|
adam@328
|
178 author = "Benjamin C. Pierce",
|
adam@328
|
179 title = "Types and Programming Languages",
|
adam@328
|
180 year = "2002",
|
adam@328
|
181 publisher = "MIT Press",
|
adam@328
|
182 chapter = "9.4"
|
adam@328
|
183 }
|
adam@328
|
184
|
adam@328
|
185 @inproceedings{Monads,
|
adam@328
|
186 author = {Wadler, Philip},
|
adam@328
|
187 title = {The essence of functional programming},
|
adam@328
|
188 booktitle = {Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
adam@328
|
189 year = {1992},
|
adam@328
|
190 }
|
adam@328
|
191
|
adam@328
|
192 @inproceedings{IO,
|
adam@328
|
193 author = {Peyton Jones, Simon L. and Wadler, Philip},
|
adam@328
|
194 title = {Imperative functional programming},
|
adam@328
|
195 booktitle = {Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
adam@328
|
196 year = {1993},
|
adam@328
|
197 }
|
adam@328
|
198
|
adam@328
|
199 @InProceedings{separation,
|
adam@328
|
200 author = {John C. Reynolds},
|
adam@328
|
201 title = {Separation Logic: A Logic for Shared Mutable Data Structures},
|
adam@328
|
202 booktitle = {Proceedings of the IEEE Symposium on Logic in Computer Science},
|
adam@328
|
203 year = {2002}
|
adam@338
|
204 }
|
adam@338
|
205
|
adam@338
|
206 @article{Okasaki,
|
adam@338
|
207 author = {Okasaki, Chris},
|
adam@338
|
208 title = {Red-black trees in a functional setting},
|
adam@338
|
209 journal = {J. Funct. Program.},
|
adam@338
|
210 volume = {9},
|
adam@338
|
211 issue = {4},
|
adam@338
|
212 year = {1999},
|
adam@338
|
213 pages = {471--477},
|
adam@338
|
214 }
|
adam@342
|
215
|
adam@342
|
216 @Article{DeBruijn,
|
adam@342
|
217 author = "Nicolas G. de Bruijn",
|
adam@342
|
218 title = "Lambda-calculus notation with nameless dummies: a tool for automatic formal manipulation with application to the {Church-Rosser} theorem",
|
adam@342
|
219 journal = "Indag. Math.",
|
adam@342
|
220 volume = "34(5)",
|
adam@342
|
221 pages = "381--392",
|
adam@342
|
222 year = "1972"
|
adam@342
|
223 }
|
adam@343
|
224
|
adam@343
|
225 @INPROCEEDINGS{GirardsParadox,
|
adam@343
|
226 author = {Thierry Coquand},
|
adam@343
|
227 title = {An Analysis of {Girard's} Paradox},
|
adam@343
|
228 booktitle = {Proceedings of the Symposium on Logic in Computer Science},
|
adam@343
|
229 year = {1986},
|
adam@343
|
230 pages = {227--236}
|
adam@343
|
231 }
|
adam@344
|
232
|
adam@344
|
233 @inproceedings{PCC,
|
adam@344
|
234 author = {George C. Necula},
|
adam@344
|
235 title = {Proof-carrying code},
|
adam@344
|
236 booktitle = {Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
adam@344
|
237 year = {1997},
|
adam@344
|
238 }
|
adam@344
|
239
|
adam@344
|
240 @inproceedings{XCAP,
|
adam@344
|
241 author = {Ni, Zhaozhong and Shao, Zhong},
|
adam@344
|
242 title = {Certified assembly programming with embedded code pointers},
|
adam@344
|
243 booktitle = {Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
adam@344
|
244 year = {2006},
|
adam@344
|
245 }
|
adam@346
|
246
|
adam@346
|
247 @TechReport{IT,
|
adam@346
|
248 title = "A Tutorial on Recursive Types in {Coq}",
|
adam@346
|
249 author = "Eduardo Gim\'enez",
|
adam@346
|
250 year = "1998",
|
adam@346
|
251 month = may,
|
adam@346
|
252 number = "0221",
|
adam@346
|
253 institution = "INRIA",
|
adam@346
|
254 }
|
adam@347
|
255
|
adam@347
|
256 @inproceedings{BigStep,
|
adam@347
|
257 author = {Xavier Leroy and Herv\'e Grall},
|
adam@347
|
258 title = {Coinductive big-step operational semantics},
|
adam@347
|
259 year = {2006},
|
adam@347
|
260 booktitle = {Proceedings of the 15th European Symposium on Programming}
|
adam@347
|
261 }
|
adam@355
|
262
|
adam@355
|
263 @InBook{WinskelDomains,
|
adam@355
|
264 author = "Glynn Winskel",
|
adam@355
|
265 title = "The Formal Semantics of Programming Languages",
|
adam@355
|
266 year = "1993",
|
adam@355
|
267 publisher = "MIT Press",
|
adam@355
|
268 chapter = "8"
|
adam@355
|
269 }
|
adam@356
|
270
|
adam@356
|
271 @article{Capretta,
|
adam@356
|
272 author = {Venanzio Capretta},
|
adam@356
|
273 title = {General Recursion via Coinductive Types},
|
adam@356
|
274 journal = {Logical Methods in Computer Science},
|
adam@356
|
275 volume = 1,
|
adam@356
|
276 number = 2,
|
adam@356
|
277 year = 2005,
|
adam@356
|
278 pages = {1--18},
|
adam@356
|
279 }
|
adam@356
|
280
|
adam@356
|
281 @inproceedings{Megacz,
|
adam@356
|
282 author = {Adam Megacz},
|
adam@356
|
283 title = {A coinductive monad for prop-bounded recursion},
|
adam@356
|
284 booktitle = {Proceedings of the {ACM} Workshop Programming
|
adam@356
|
285 Languages meets Program Verification},
|
adam@356
|
286 pages = {11--20},
|
adam@356
|
287 year = {2007},
|
adam@356
|
288 }
|
adam@358
|
289
|
adam@358
|
290 @inproceedings{modules,
|
adam@358
|
291 author = {MacQueen, David},
|
adam@358
|
292 title = {Modules for {Standard ML}},
|
adam@358
|
293 booktitle = {Proceedings of the 1984 ACM Symposium on LISP and Functional Programming},
|
adam@358
|
294 year = {1984},
|
adam@358
|
295 pages = {198--207},
|
adam@358
|
296 }
|
adam@358
|
297
|
adam@358
|
298 @inproceedings{typeclasses,
|
adam@358
|
299 author = {Wadler, P. and Blott, S.},
|
adam@358
|
300 title = {How to make ad-hoc polymorphism less ad hoc},
|
adam@358
|
301 booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
adam@358
|
302 year = {1989},
|
adam@464
|
303 % pages = {60--76},
|
adam@358
|
304 }
|
adam@360
|
305
|
adam@360
|
306 @inproceedings{reflection,
|
adam@360
|
307 author = {Boutin, Samuel},
|
adam@360
|
308 title = {Using reflection to build efficient and certified decision procedures},
|
adam@360
|
309 booktitle = {Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software},
|
adam@360
|
310 year = {1997},
|
adam@360
|
311 }
|
adam@364
|
312
|
adam@364
|
313 @inproceedings{JMeq,
|
adam@364
|
314 author = {McBride, Conor},
|
adam@364
|
315 title = {Elimination with a Motive},
|
adam@364
|
316 booktitle = {Proceedings of the International Workshop on Types for Proofs and Programs},
|
adam@364
|
317 year = {2000},
|
adam@364
|
318 pages = {197--216}
|
adam@364
|
319 }
|
adam@364
|
320
|
adam@364
|
321 @phdthesis{AxiomK,
|
adam@364
|
322 author = {Thomas Streicher},
|
adam@364
|
323 title = {Semantical Investigations into Intensional Type Theory},
|
adam@364
|
324 type = {Habilitationsschrift},
|
adam@364
|
325 school = {LMU M\"unchen},
|
adam@364
|
326 year= {1993}
|
adam@364
|
327 }
|
adam@381
|
328
|
adam@381
|
329 @article{BGB,
|
adam@381
|
330 author = {Geoffrey Washburn and Stephanie Weirich},
|
adam@381
|
331 title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
|
adam@381
|
332 journal = {J. Funct. Program.},
|
adam@381
|
333 volume = {18},
|
adam@381
|
334 number = {1},
|
adam@381
|
335 year = {2008},
|
adam@381
|
336 pages = {87--140},
|
adam@381
|
337 publisher = {Cambridge University Press},
|
adam@381
|
338 address = {New York, NY, USA},
|
adam@381
|
339 }
|
adam@381
|
340
|
adam@381
|
341 @InProceedings{PhoasICFP08,
|
adam@381
|
342 author = {Adam Chlipala},
|
adam@381
|
343 title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
|
adam@381
|
344 booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
|
adam@381
|
345 year = {2008},
|
adam@381
|
346 pages = {143--156}
|
adam@381
|
347 }
|
adam@381
|
348
|
adam@381
|
349 @article{parametricity,
|
adam@381
|
350 author = {Reynolds, J.C.},
|
adam@381
|
351 year = {1983},
|
adam@381
|
352 title = {Types, abstraction, and parametric polymorphism},
|
adam@381
|
353 journal = {Information Processing},
|
adam@381
|
354 pages = {513--523}
|
adam@381
|
355 }
|
adam@381
|
356
|
adam@381
|
357 @InProceedings{CompilerPOPL10,
|
adam@381
|
358 author = {Adam Chlipala},
|
adam@381
|
359 title = {A Verified Compiler for an Impure Functional Language},
|
adam@381
|
360 booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
|
adam@381
|
361 year = {2010},
|
adam@381
|
362 }
|
adam@387
|
363
|
adam@387
|
364 @inproceedings{Isar,
|
adam@387
|
365 author = {Wenzel, Markus},
|
adam@387
|
366 title = {Isar - A Generic Interpretative Approach to Readable Formal Proof Documents},
|
adam@387
|
367 booktitle = {Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
|
adam@387
|
368 year = {1999},
|
adam@387
|
369 }
|
adam@394
|
370
|
adam@394
|
371 @article{continuations,
|
adam@394
|
372 author = {Reynolds, John C.},
|
adam@394
|
373 title = {The discoveries of continuations},
|
adam@394
|
374 journal = {Lisp Symb. Comput.},
|
adam@394
|
375 issue_date = {Nov. 1993},
|
adam@394
|
376 volume = {6},
|
adam@394
|
377 number = {3-4},
|
adam@394
|
378 month = nov,
|
adam@394
|
379 year = {1993},
|
adam@394
|
380 issn = {0892-4635},
|
adam@394
|
381 pages = {233--248},
|
adam@394
|
382 numpages = {16},
|
adam@394
|
383 url = {http://dx.doi.org/10.1007/BF01019459},
|
adam@394
|
384 doi = {10.1007/BF01019459},
|
adam@394
|
385 acmid = {198114},
|
adam@394
|
386 publisher = {Kluwer Academic Publishers},
|
adam@394
|
387 address = {Hingham, MA, USA},
|
adam@394
|
388 keywords = {continuation, continuation-passing style, semantics},
|
adam@394
|
389 }
|
adam@394
|
390
|
adam@394
|
391 @article{unification,
|
adam@394
|
392 author = {Robinson, J. A.},
|
adam@394
|
393 title = {A Machine-Oriented Logic Based on the Resolution Principle},
|
adam@394
|
394 journal = {J. ACM},
|
adam@394
|
395 issue_date = {Jan. 1965},
|
adam@394
|
396 volume = {12},
|
adam@394
|
397 number = {1},
|
adam@394
|
398 month = jan,
|
adam@394
|
399 year = {1965},
|
adam@394
|
400 issn = {0004-5411},
|
adam@394
|
401 pages = {23--41},
|
adam@394
|
402 numpages = {19},
|
adam@394
|
403 url = {http://doi.acm.org/10.1145/321250.321253},
|
adam@394
|
404 doi = {10.1145/321250.321253},
|
adam@394
|
405 acmid = {321253},
|
adam@394
|
406 publisher = {ACM},
|
adam@394
|
407 address = {New York, NY, USA},
|
adam@394
|
408 }
|
adam@395
|
409
|
adam@395
|
410 @ARTICLE{whyfp,
|
adam@395
|
411 author = {John Hughes},
|
adam@395
|
412 title = {Why Functional Programming Matters},
|
adam@395
|
413 journal = {The Computer Journal},
|
adam@395
|
414 year = {1984},
|
adam@395
|
415 volume = {32},
|
adam@395
|
416 pages = {98--107}
|
adam@395
|
417 }
|
adam@395
|
418
|
adam@395
|
419 @Book{Prolog,
|
adam@395
|
420 author = "Leon Sterling and Ehud Shapiro",
|
adam@395
|
421 title = "The Art of Prolog, 2nd Edition",
|
adam@395
|
422 year = "1994",
|
adam@395
|
423 publisher = "MIT Press"
|
adam@395
|
424 }
|
adam@395
|
425
|
adam@395
|
426 @Book{LogicProgramming,
|
adam@395
|
427 author = "John W. Lloyd",
|
adam@395
|
428 title = "Foundations of Logic Programming, 2nd Edition",
|
adam@395
|
429 year = "1987",
|
adam@395
|
430 publisher = "Springer"
|
adam@395
|
431 }
|
adam@395
|
432
|
adam@395
|
433 @InBook{deriving,
|
adam@395
|
434 title = "Haskell 98 Language and Libraries: The Revised Report",
|
adam@395
|
435 author = "Simon {Peyton Jones} and Lennart Augustsson and Dave Barton and Brian Boutel and Warren Burton and Joseph Fasel and Kevin Hammond and Ralf Hinze and Paul Hudak and John Hughes and Thomas Johnsson and Mark Jones and John Launchbury and Erik Meijer and John Peterson and Alastair Reid and Colin Runciman and Philip Wadler",
|
adam@395
|
436 year = "1998",
|
adam@395
|
437 chapter = "4.3.3",
|
adam@395
|
438 url = {http://www.haskell.org/onlinereport/decls.html#derived-decls}
|
adam@395
|
439 }
|