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}