Converted Filet-o-Fish Literate Haskell code into a Technical Note
[barrelfish] / tools / fof / FiletOFish.bib
1 @inproceedings{schuepbach:mmcs08,
2         author = {Schapbach, Adrian   and Peter, Simon   and Baumann, Andrew   and Roscoe, Timothy   and Barham, Paul   and Harris, Tim   and Isaacs, Rebecca  },
3         booktitle = {Proceedings of the Workshop on Managed Many-Core Systems},
4         citeulike-article-id = {3416014},
5         keywords = {multi-core, os, project-master-thesis},
6         month = {June},
7         posted-at = {2008-10-15 22:55:03},
8         priority = {0},
9         title = {Embracing diversity in the Barrelfish manycore operating system},
10         year = {2008}
11 }
12
13 @incollection{leroy-frontend,
14         abstract = {This paper presents the formal verification of a compiler front-end that translates a subset of the C language into the Cminor intermediate language. The semantics of the source and target languages as well as the translation between them have been written in the specification language of the Coq proof assistant. The proof of observational semantic equivalence between the source and generated code has been machine-checked using Coq. An executable compiler was obtained by automatic extraction of executable Caml code from the Coq specification of the translator, combined with a certified compiler back-end generating PowerPC assembly code from Cminor, described in previous work.},
15         author = {Blazy, Sandrine   and Dargaye, Zaynah   and Leroy, Xavier  },
16         citeulike-article-id = {3338183},
17         doi = {10.1007/11813040\_31},
18         journal = {FM 2006: Formal Methods},
19         keywords = {certification, compiler, coq, formal-proof},
20         pages = {460--475},
21         posted-at = {2008-09-25 21:31:23},
22         priority = {0},
23         title = {Formal Verification of a C Compiler Front-End},
24         url = {http://dx.doi.org/10.1007/11813040\_31},
25         year = {2006}
26 }
27
28 @article{leroy-backend,
29         address = {New York, NY, USA},
30         author = {Leroy, Xavier  },
31         citeulike-article-id = {2967319},
32         doi = {10.1145/1111320.1111042},
33         issn = {0362-1340},
34         journal = {SIGPLAN Not.},
35         keywords = {compiler, coq-programming, software-verification},
36         month = {January},
37         number = {1},
38         pages = {42--54},
39         posted-at = {2008-07-06 14:47:57},
40         priority = {0},
41         publisher = {ACM},
42         title = {Formal certification of a compiler back-end or: programming a compiler with a proof assistant},
43         url = {http://dx.doi.org/10.1145/1111320.1111042},
44         volume = {41},
45         year = {2006}
46 }
47
48 @phdthesis{swierstra-phd,
49         author = {Swierstra, Wouter  },
50         citeulike-article-id = {4220206},
51         keywords = {effects, functional-programming, hoare-type-theory, language-agda, language-haskell, specification, types},
52         month = {November},
53         posted-at = {2009-03-25 17:32:07},
54         priority = {0},
55         title = {A Functional Specification of Effects},
56         year = {2008}
57 }
58
59 @inproceedings{swierstra-beast,
60         abstract = {It can be very difficult to debug impure code, let alone prove its correctness. To address these problems, we provide a functional specification of three central components of Peyton Jones's awkward squad: teletype IO, mutable state, and concurrency. By constructing an internal model of such concepts within our programming language, we can test, debug, and reason about programs that perform IO as if they were pure. In particular, we demonstrate how our specifications may be used in tandem with QuickCheck to automatically test complex pointer algorithms and concurrent programs.},
61         address = {New York, NY, USA},
62         author = {Swierstra, Wouter   and Altenkirch, Thorsten  },
63         booktitle = {Haskell '07: Proceedings of the ACM SIGPLAN workshop on Haskell workshop},
64         citeulike-article-id = {3360998},
65         doi = {10.1145/1291201.1291206},
66         isbn = {978-1-59593-674-5},
67         keywords = {formal-proof, functional-programming, language-haskell, monads, pure},
68         location = {Freiburg, Germany},
69         pages = {25--36},
70         posted-at = {2008-10-01 00:16:24},
71         priority = {0},
72         publisher = {ACM},
73         title = {Beauty in the beast},
74         url = {http://dx.doi.org/10.1145/1291201.1291206},
75         year = {2007}
76 }
77
78 @article{swierstra-expression,
79         abstract = {This paper describes a technique for assembling both data types and functions from isolated individual components. We also explore how the same technology can be used to combine free monads and, as a result, structure Haskell's monolithic IO monad.},
80         author = {Swierstra, Wouter  },
81         citeulike-article-id = {2742096},
82         journal = {Journal of Functional Programming},
83         keywords = {expression-problem, functional-programming, language-haskell, monads},
84         number = {-1},
85         pages = {1--14},
86         posted-at = {2008-05-13 09:00:51},
87         priority = {0},
88         title = {Data types \`{a} la carte},
89         url = {http://journals.cambridge.org/action/displayAbstract?fromPage=online\&aid=1813324},
90         volume = {Forthcoming},
91         year = {2008}
92 }
93
94 @incollection{hughes-pprinter,
95         abstract = {Layouts We'll begin by looking for an abstract model of a pretty-printer's output --- that is, prettily indented text. We could say that the output is just a string, but a string has so little structure that we can derive no intuition from it. Let us say instead, that a layout is a sequence of indented lines, which we can model as type Layout = [(Int; String)] + Notice that we shall allow indentations to be negative: later on this will contribute to a nicer algebra, just as integers have a...},
96         author = {Hughes, John  },
97         booktitle = {Advanced Functional Programming},
98         citeulike-article-id = {828959},
99         editor = {Jeuring, J.  and Meijer, E. },
100         keywords = {combinator, functional-programming, language-haskell},
101         posted-at = {2007-11-23 04:14:01},
102         priority = {2},
103         publisher = {Springer Verlag},
104         title = {The {D}esign of a {P}retty-printing {L}ibrary},
105         url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.8777},
106         volume = {925},
107         year = {1995}
108 }
109
110 @article{wadler-pprinter,
111         abstract = {John Hughes has made pretty printers one of the prime demonstrations of using combinators to develop a library, and algebra to implement it. This note presents a new design for pretty printers which improves on Hughes's classic design. The new design is based on a single concatenation operator which is associative and has a left and right unit. Hughes's design requires two separate operators for concatenation, where horizontal concatenation has a right unit but no left unit, and vertical...},
112         author = {Wadler, Philip  },
113         citeulike-article-id = {828960},
114         journal = {Journal of Functional Programming},
115         keywords = {combinator, functional-programming, language-haskell, lecture-cs-252r},
116         posted-at = {2008-08-23 07:28:25},
117         priority = {0},
118         title = {A prettier printer},
119         url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.19.635},
120         year = {1999}
121 }
122
123 @Misc{kmett-free-monad,
124   author =       {Kmett, Edward},
125   title =        {Monads for Free},
126   year =         {2008},
127   url =          {http://comonad.com/reader/2008/monads-for-free/},
128 }
129
130 @Misc{hurricane-names,
131   author =       {National Hurricane Center},
132   title =        {Retired Hurricane Names Since 1954},
133   url =          {http://www.nhc.noaa.gov/retirednames.shtml},
134 }
135
136 @Misc{ramsey-hoopl,
137   author =       {Ramsey, Norman and Dias, John and Peyton Jones, Simon },
138   title =        {Hoopl: Dataflow Optimization Made Simple},
139   year =         {2009},
140   url =          {http://research.microsoft.com/en-us/um/people/simonpj/papers/c--/dfopt.pdf},
141 }
142
143 @article{necula-tvi,
144     author = {Necula, George C.},
145     title = {Translation validation for an optimizing compiler},
146     volume = {35},
147     year = {2000}
148 }