other.bib

   1
   2 @mastersthesis{crooijmans_reducing_2021,
   3         address = {Nijmegen},
   4         title = {Reducing the {Power} {Consumption} of {IoT} {Devices} in {Task}-{Oriented} {Programming}},
   5         language = {en},
   6         school = {Radboud University},
   7         author = {Crooijmans, Sjoerd},
   8         month = jul,
   9         year = {2021},
  10         file = {Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:/home/mrl/.local/share/zotero/storage/98LY9YHH/Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:application/pdf},
  11 }
  12
  13 @inproceedings{plasmeijer_task-oriented_2012,
  14         address = {New York, NY, USA},
  15         series = {{PPDP} '12},
  16         title = {Task-{Oriented} {Programming} in a {Pure} {Functional} {Language}},
  17         isbn = {978-1-4503-1522-7},
  18         url = {https://doi.org/10.1145/2370776.2370801},
  19         doi = {10.1145/2370776.2370801},
  20         abstract = {Task-Oriented Programming (TOP) is a novel programming paradigm for the construction of distributed systems where users work together on the internet. When multiple users collaborate, they need to interact with each other frequently. TOP supports the definition of tasks that react to the progress made by others. With TOP, complex multi-user interactions can be programmed in a declarative style just by defining the tasks that have to be accomplished, thus eliminating the need to worry about the implementation detail that commonly frustrates the development of applications for this domain. TOP builds on four core concepts: tasks that represent computations or work to do which have an observable value that may change over time, data sharing enabling tasks to observe each other while the work is in progress, generic type driven generation of user interaction, and special combinators for sequential and parallel task composition. The semantics of these core concepts is defined in this paper. As an example we present the iTask3 framework, which embeds TOP in the functional programming language Clean.},
  21         booktitle = {Proceedings of the 14th {Symposium} on {Principles} and {Practice} of {Declarative} {Programming}},
  22         publisher = {Association for Computing Machinery},
  23         author = {Plasmeijer, Rinus and Lijnse, Bas and Michels, Steffen and Achten, Peter and Koopman, Pieter},
  24         year = {2012},
  25         note = {event-place: Leuven, Belgium},
  26         keywords = {clean, task-oriented programming},
  27         pages = {195--206},
  28         file = {103802.pdf:/home/mrl/.local/share/zotero/storage/ZE6A65AW/103802.pdf:application/pdf},
  29 }
  30
  31 @inproceedings{brus_clean_1987,
  32         address = {Berlin, Heidelberg},
  33         title = {Clean — {A} language for functional graph rewriting},
  34         isbn = {978-3-540-47879-9},
  35         abstract = {Clean is an experimental language for specifying functional computations in terms of graph rewriting. It is based on an extension of Term Rewriting Systems (TRS) in which the terms are replaced by graphs. Such a Graph Rewriting System (GRS) consists of a, possibly cyclic, directed graph, called the data graph and graph rewrite rules which specify how this data graph may be rewritten. Clean is designed to provide a firm base for functional programming. In particular, Clean is suitable as an intermediate language between functional languages and (parallel) target machine architectures. A sequential implementation of Clean on a conventional machine is described and its performance is compared with other systems. The results show that Clean can be efficiently implemented.},
  36         booktitle = {Functional {Programming} {Languages} and {Computer} {Architecture}},
  37         publisher = {Springer Berlin Heidelberg},
  38         author = {Brus, T. H. and van Eekelen, M. C. J. D. and van Leer, M. O. and Plasmeijer, M. J.},
  39         editor = {Kahn, Gilles},
  40         year = {1987},
  41         pages = {364--384},
  42         file = {brut87-Clean.ps.gz:/home/mrl/.local/share/zotero/storage/T2QATWIE/brut87-Clean.ps.gz:application/gzip},
  43 }
  44
  45 @misc{bolingbroke_constraint_2011,
  46         title = {Constraint {Kinds} for {GHC}},
  47         url = {http://blog.omega-prime.co.uk/2011/09/10/constraint-kinds-for-ghc/},
  48         urldate = {2021-06-09},
  49         journal = {:: (Bloggable a) ={\textgreater} a -{\textgreater} IO ()},
  50         author = {Bolingbroke, Max},
  51         month = sep,
  52         year = {2011},
  53         file = {Constraint Kinds for GHC:/home/mrl/.local/share/zotero/storage/R6RL79K7/constraint-kinds-for-ghc.html:text/html},
  54 }
  55
  56 @inproceedings{fegaras_revisiting_1996,
  57         address = {New York, NY, USA},
  58         series = {{POPL} '96},
  59         title = {Revisiting {Catamorphisms} over {Datatypes} with {Embedded} {Functions} (or, {Programs} from {Outer} {Space})},
  60         isbn = {0-89791-769-3},
  61         url = {https://doi.org/10.1145/237721.237792},
  62         doi = {10.1145/237721.237792},
  63         abstract = {We revisit the work of Paterson and of Meijer \& Hutton, which describes how to construct catamorphisms for recursive datatype definitions that embed contravariant occurrences of the type being defined. Their construction requires, for each catamorphism, the definition of an anamorphism that has an inverse-like relationship to that catamorphism. We present an alternative construction, which replaces the stringent requirement that an inverse anamorphism be defined for each catamorphism with a more lenient restriction. The resulting construction has a more efficient implementation than that of Paterson, Meijer, and Hutton and the relevant restriction can be enforced by a Hindley-Milner type inference algorithm. We provide numerous examples illustrating our method.},
  64         booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
  65         publisher = {Association for Computing Machinery},
  66         author = {Fegaras, Leonidas and Sheard, Tim},
  67         year = {1996},
  68         note = {event-place: St. Petersburg Beach, Florida, USA},
  69         pages = {284--294},
  70         file = {Fegaras and Sheard - 1996 - Revisiting Catamorphisms over Datatypes with Embed.pdf:/home/mrl/.local/share/zotero/storage/WCSRVWGC/Fegaras and Sheard - 1996 - Revisiting Catamorphisms over Datatypes with Embed.pdf:application/pdf},
  71 }
  72
  73 @inproceedings{pfenning_higher-order_1988,
  74         address = {New York, NY, USA},
  75         series = {{PLDI} '88},
  76         title = {Higher-{Order} {Abstract} {Syntax}},
  77         isbn = {0-89791-269-1},
  78         url = {https://doi.org/10.1145/53990.54010},
  79         doi = {10.1145/53990.54010},
  80         abstract = {We describe motivation, design, use, and implementation of higher-order abstract syntax as a central representation for programs, formulas, rules, and other syntactic objects in program manipulation and other formal systems where matching and substitution or unification are central operations. Higher-order abstract syntax incorporates name binding information in a uniform and language generic way. Thus it acts as a powerful link integrating diverse tools in such formal environments. We have implemented higher-order abstract syntax, a supporting matching and unification algorithm, and some clients in Common Lisp in the framework of the Ergo project at Carnegie Mellon University.},
  81         booktitle = {Proceedings of the {ACM} {SIGPLAN} 1988 {Conference} on {Programming} {Language} {Design} and {Implementation}},
  82         publisher = {Association for Computing Machinery},
  83         author = {Pfenning, F. and Elliott, C.},
  84         year = {1988},
  85         note = {event-place: Atlanta, Georgia, USA},
  86         pages = {199--208},
  87         file = {Pfenning and Elliott - 1988 - Higher-Order Abstract Syntax.pdf:/home/mrl/.local/share/zotero/storage/2HSRWURK/Pfenning and Elliott - 1988 - Higher-Order Abstract Syntax.pdf:application/pdf},
  88 }
  89
  90 @inproceedings{chlipala_parametric_2008,
  91         address = {New York, NY, USA},
  92         series = {{ICFP} '08},
  93         title = {Parametric {Higher}-{Order} {Abstract} {Syntax} for {Mechanized} {Semantics}},
  94         isbn = {978-1-59593-919-7},
  95         url = {https://doi.org/10.1145/1411204.1411226},
  96         doi = {10.1145/1411204.1411226},
  97         abstract = {We present parametric higher-order abstract syntax (PHOAS), a new approach to formalizing the syntax of programming languages in computer proof assistants based on type theory. Like higher-order abstract syntax (HOAS), PHOAS uses the meta language's binding constructs to represent the object language's binding constructs. Unlike HOAS, PHOAS types are definable in general-purpose type theories that support traditional functional programming, like Coq's Calculus of Inductive Constructions. We walk through how Coq can be used to develop certified, executable program transformations over several statically-typed functional programming languages formalized with PHOAS; that is, each transformation has a machine-checked proof of type preservation and semantic preservation. Our examples include CPS translation and closure conversion for simply-typed lambda calculus, CPS translation for System F, and translation from a language with ML-style pattern matching to a simpler language with no variable-arity binding constructs. By avoiding the syntactic hassle associated with first-order representation techniques, we achieve a very high degree of proof automation.},
  98         booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
  99         publisher = {Association for Computing Machinery},
 100         author = {Chlipala, Adam},
 101         year = {2008},
 102         note = {event-place: Victoria, BC, Canada},
 103         keywords = {compiler verification, dependent types, interactive proof assistants, type-theoretic semantics},
 104         pages = {143--156},
 105         file = {Chlipala - 2008 - Parametric Higher-Order Abstract Syntax for Mechan.pdf:/home/mrl/.local/share/zotero/storage/DZ33DAMU/Chlipala - 2008 - Parametric Higher-Order Abstract Syntax for Mechan.pdf:application/pdf},
 106 }
 107
 108 @incollection{reynolds_user-defined_1978,
 109         address = {New York, NY},
 110         title = {User-{Defined} {Types} and {Procedural} {Data} {Structures} as {Complementary} {Approaches} to {Data} {Abstraction}},
 111         isbn = {978-1-4612-6315-9},
 112         url = {https://doi.org/10.1007/978-1-4612-6315-9_22},
 113         abstract = {User-defined types (or modes) and procedural (or functional) data structures are complementary methods for data abstraction, each providing a capability lacked by the other. With user-defined types, all information about the representation of a particular kind of data is centralized in a type definition and hidden from the rest of the program. With procedural data structures, each part of the program which creates data can specify its own representation, independently of any representations used elsewhere for the same kind of data. However, this decentralization of the description of data is achieved at the cost of prohibiting primitive operations from accessing the representations of more than one data item. The contrast between these approaches is illustrated by a simple example.},
 114         booktitle = {Programming {Methodology}: {A} {Collection} of {Articles} by {Members} of {IFIP} {WG2}.3},
 115         publisher = {Springer New York},
 116         author = {Reynolds, John C.},
 117         editor = {Gries, David},
 118         year = {1978},
 119         doi = {10.1007/978-1-4612-6315-9_22},
 120         pages = {309--317},
 121         file = {Reynolds - 1978 - User-Defined Types and Procedural Data Structures .pdf:/home/mrl/.local/share/zotero/storage/ASXE73U2/Reynolds - 1978 - User-Defined Types and Procedural Data Structures .pdf:application/pdf},
 122 }
 123
 124 @misc{ghc_team_ghc_2021,
 125         title = {{GHC} {User}’s {Guide} {Documentation}},
 126         url = {https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf},
 127         language = {English},
 128         urldate = {2021-02-24},
 129         publisher = {Release},
 130         author = {GHC Team},
 131         year = {2021},
 132         file = {GHC Team - 2021 - GHC User’s Guide Documentation.pdf:/home/mrl/.local/share/zotero/storage/87ZT5VXL/GHC Team - 2021 - GHC User’s Guide Documentation.pdf:application/pdf},
 133 }
 134
 135 @misc{ghc_team_datadynamic_2021,
 136         title = {Data.{Dynamic}},
 137         url = {https://hackage.haskell.org/package/base-4.14.1.0/docs/Data-Dynamic.html},
 138         language = {English},
 139         urldate = {2021-02-24},
 140         publisher = {Release},
 141         author = {GHC Team},
 142         year = {2021},
 143 }
 144
 145 @inproceedings{jeuring_polytypic_1996,
 146         address = {Berlin, Heidelberg},
 147         title = {Polytypic programming},
 148         isbn = {978-3-540-70639-7},
 149         abstract = {Many functions have to be written over and over again for different datatypes, either because datatypes change during the development of programs, or because functions with similar functionality are needed on different datatypes. Examples of such functions are pretty printers, debuggers, equality functions, unifiers, pattern matchers, rewriting functions, etc. Such functions are called polytypic functions. A polytypic function is a function that is defined by induction on the structure of user-defined datatypes. This paper introduces polytypic functions, and shows how to construct and reason about polytypic functions. A larger example is studied in detail: polytypic functions for term rewriting and for determining whether a collection of rewrite rules is normalising.},
 150         booktitle = {Advanced {Functional} {Programming}},
 151         publisher = {Springer Berlin Heidelberg},
 152         author = {Jeuring, Johan and Jansson, Patrik},
 153         editor = {Launchbury, John and Meijer, Erik and Sheard, Tim},
 154         year = {1996},
 155         pages = {68--114},
 156         file = {Jeuring and Jansson - 1996 - Polytypic programming.pdf:/home/mrl/.local/share/zotero/storage/SLC4G2IT/Jeuring and Jansson - 1996 - Polytypic programming.pdf:application/pdf},
 157 }
 158
 159 @book{peyton_jones_haskell_2003,
 160         address = {Cambridge},
 161         title = {Haskell 98 language and libraries: the revised report},
 162         isbn = {0-521 826144},
 163         publisher = {Cambridge University Press},
 164         editor = {Peyton Jones, Simon},
 165         year = {2003},
 166         file = {Peyton Jones - 2003 - Haskell 98 language and libraries the revised rep.pdf:/home/mrl/.local/share/zotero/storage/UXEJT89I/Peyton Jones - 2003 - Haskell 98 language and libraries the revised rep.pdf:application/pdf},
 167 }
 168
 169 @inproceedings{laufer_combining_1994,
 170         title = {Combining type classes and existential types},
 171         booktitle = {Proceedings of the {Latin} {American} {Informatic} {Conference} ({PANEL})},
 172         publisher = {ITESM-CEM},
 173         author = {Läufer, Konstantin},
 174         year = {1994},
 175         note = {event-place: Monterrey, Mexico},
 176         file = {Läufer - COMBINING TYPE CLASSES AND EXISTENTIAL TYPES.pdf:/home/mrl/.local/share/zotero/storage/KR4P9EHS/Läufer - COMBINING TYPE CLASSES AND EXISTENTIAL TYPES.pdf:application/pdf},
 177 }
 178
 179 @techreport{hughes_restricted_1999,
 180         address = {Paris},
 181         title = {Restricted data types in {Haskell}},
 182         number = {UU-CS-1999-28},
 183         institution = {Department of Information and Computing Sciences, Utrecht University},
 184         author = {Hughes, John},
 185         year = {1999},
 186         pages = {16},
 187         file = {Hughes - 1999 - Restricted data types in Haskell.pdf:/home/mrl/.local/share/zotero/storage/7ZE2MYWE/Hughes - 1999 - Restricted data types in Haskell.pdf:application/pdf},
 188 }
 189
 190 @article{najd_trees_2017,
 191         title = {Trees that {Grow}},
 192         volume = {23},
 193         abstract = {We study the notion of extensibility in functional data types, as a new approach to the problem of decorating abstract syntax trees with additional information. We observed the need for such extensibility while redesigning the data types representing Haskell abstract syntax inside Glasgow Haskell Compiler (GHC). Specifically, we describe a programming idiom that exploits type-level functions to allow a particular form of extensibility. The approach scales to support existentials and generalised algebraic data types, and we can use pattern synonyms to make it convenient in practice.},
 194         number = {1},
 195         journal = {Journal of Universal Computer Science},
 196         author = {Najd, Shayan and Peyton Jones, Simon},
 197         month = jan,
 198         year = {2017},
 199         pages = {42--62},
 200         file = {Najd and Jones - 2017 - Trees that Grow.pdf:/home/mrl/.local/share/zotero/storage/HYQFTWZP/Najd and Jones - 2017 - Trees that Grow.pdf:application/pdf},
 201 }
 202
 203 @inproceedings{loh_open_2006,
 204         address = {New York, NY, USA},
 205         series = {{PPDP} '06},
 206         title = {Open {Data} {Types} and {Open} {Functions}},
 207         isbn = {1-59593-388-3},
 208         url = {https://doi.org/10.1145/1140335.1140352},
 209         doi = {10.1145/1140335.1140352},
 210         abstract = {The problem of supporting the modular extensibility of both data and functions in one programming language at the same time is known as the expression problem. Functional languages traditionally make it easy to add new functions, but extending data (adding new data constructors) requires modifying existing code. We present a semantically and syntactically lightweight variant of open data types and open functions as a solution to the expression problem in the Haskell language. Constructors of open data types and equations of open functions may appear scattered throughout a program with several modules. The intended semantics is as follows: the program should behave as if the data types and functions were closed, defined in one place. The order of function equations is determined by best-fit pattern matching, where a specific pattern takes precedence over an unspecific one. We show that our solution is applicable to the expression problem, generic programming, and exceptions. We sketch two implementations: a direct implementation of the semantics, and a scheme based on mutually recursive modules that permits separate compilation},
 211         booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {International} {Conference} on {Principles} and {Practice} of {Declarative} {Programming}},
 212         publisher = {Association for Computing Machinery},
 213         author = {Löh, Andres and Hinze, Ralf},
 214         year = {2006},
 215         note = {event-place: Venice, Italy},
 216         keywords = {functional programming, Haskell, expression problem, extensible data types, extensible exceptions, extensible functions, generic programming, mutually recursive modules},
 217         pages = {133--144},
 218         file = {OpenDatatypes.pdf:/home/mrl/.local/share/zotero/storage/NEP9GZ9N/OpenDatatypes.pdf:application/pdf},
 219 }
 220
 221 @inproceedings{hutton_fold_1998,
 222         address = {New York, NY, USA},
 223         series = {{ICFP} '98},
 224         title = {Fold and {Unfold} for {Program} {Semantics}},
 225         isbn = {1-58113-024-4},
 226         url = {https://doi.org/10.1145/289423.289457},
 227         doi = {10.1145/289423.289457},
 228         abstract = {In this paper we explain how recursion operators can be used to structure and reason about program semantics within a functional language. In particular, we show how the recursion operator fold can be used to structure denotational semantics, how the dual recursion operator unfold can be used to structure operational semantics, and how algebraic properties of these operators can be used to reason about program semantics. The techniques are explained with the aid of two main examples, the first concerning arithmetic expressions, and the second concerning Milner's concurrent language CCS. The aim of the paper is to give functional programmers new insights into recursion operators, program semantics, and the relationships between them.},
 229         booktitle = {Proceedings of the {Third} {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
 230         publisher = {Association for Computing Machinery},
 231         author = {Hutton, Graham},
 232         year = {1998},
 233         note = {event-place: Baltimore, Maryland, USA},
 234         pages = {280--288},
 235         file = {Hutton - 1998 - Fold and unfold for program semantics.pdf:/home/mrl/.local/share/zotero/storage/YEB9K2TP/Hutton - 1998 - Fold and unfold for program semantics.pdf:application/pdf},
 236 }
 237
 238 @article{abadi_dynamic_1991,
 239         title = {Dynamic {Typing} in a {Statically} {Typed} {Language}},
 240         volume = {13},
 241         issn = {0164-0925},
 242         url = {https://doi.org/10.1145/103135.103138},
 243         doi = {10.1145/103135.103138},
 244         abstract = {Statically typed programming languages allow earlier error checking, better enforcement of diciplined programming styles, and the generation of more efficient object code than languages where all type consistency checks are performed at run time. However, even in statically typed languages, there is often the need to deal with datawhose type cannot be determined at compile time. To handle such situations safely, we propose to add a type Dynamic whose values are pairs of a value v and a type tag T where v has the type denoted by T. Instances of Dynamic are built with an explicit tagging construct and inspected with a type safe typecase construct.This paper explores the syntax, operational semantics, and denotational semantics of a simple language that includes the type Dynamic. We give examples of how dynamically typed values can be used in programming. Then we discuss an operational semantics for our language and obtain a soundness theorem. We present two formulations of the denotational semantics of this language and relate them to the operational semantics. Finally, we consider the implications of polymorphism and some implementation issues.},
 245         number = {2},
 246         journal = {ACM Trans. Program. Lang. Syst.},
 247         author = {Abadi, Martín and Cardelli, Luca and Pierce, Benjamin and Plotkin, Gordon},
 248         month = apr,
 249         year = {1991},
 250         note = {Place: New York, NY, USA
 251 Publisher: Association for Computing Machinery},
 252         keywords = {theory},
 253         pages = {237--268},
 254         file = {Abadi et al. - 1991 - Dynamic typing in a statically typed language.pdf:/home/mrl/.local/share/zotero/storage/CJSBG6X7/Abadi et al. - 1991 - Dynamic typing in a statically typed language.pdf:application/pdf},
 255 }
 256
 257 @inproceedings{svenningsson_combining_2013,
 258         address = {Berlin, Heidelberg},
 259         title = {Combining {Deep} and {Shallow} {Embedding} for {EDSL}},
 260         isbn = {978-3-642-40447-4},
 261         doi = {10.1007/978-3-642-40447-4_2},
 262         abstract = {When compiling embedded languages it is natural to use an abstract syntax tree to represent programs. This is known as a deep embedding and it is a rather cumbersome technique compared to other forms of embedding, typically leading to more code and being harder to extend. In shallow embeddings, language constructs are mapped directly to their semantics which yields more flexible and succinct implementations. But shallow embeddings are not well-suited for compiling embedded languages. We present a technique to combine deep and shallow embedding in the context of compiling embedded languages in order to provide the benefits of both techniques. In particular it helps keeping the deep embedding small and it makes extending the embedded language much easier. Our technique also has some unexpected but welcome knock-on effects. It provides fusion of functions to remove intermediate results for free without any additional effort. It also helps to give the embedded language a more natural programming interface.},
 263         booktitle = {Trends in {Functional} {Programming}},
 264         publisher = {Springer Berlin Heidelberg},
 265         author = {Svenningsson, Josef and Axelsson, Emil},
 266         editor = {Loidl, Hans-Wolfgang and Peña, Ricardo},
 267         year = {2013},
 268         pages = {21--36},
 269         file = {svenningsson2013combining.pdf:/home/mrl/.local/share/zotero/storage/NFBGZCZT/svenningsson2013combining.pdf:application/pdf},
 270 }
 271
 272 @article{mitchell_abstract_1988,
 273         title = {Abstract {Types} {Have} {Existential} {Type}},
 274         volume = {10},
 275         issn = {0164-0925},
 276         url = {https://doi.org/10.1145/44501.45065},
 277         doi = {10.1145/44501.45065},
 278         abstract = {Abstract data type declarations appear in typed programming languages like Ada, Alphard, CLU and ML. This form of declaration binds a list of identifiers to a type with associated operations, a composite “value” we call a data algebra. We use a second-order typed lambda calculus SOL to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.},
 279         number = {3},
 280         journal = {ACM Trans. Program. Lang. Syst.},
 281         author = {Mitchell, John C. and Plotkin, Gordon D.},
 282         month = jul,
 283         year = {1988},
 284         note = {Place: New York, NY, USA
 285 Publisher: Association for Computing Machinery},
 286         pages = {470--502},
 287         file = {Mitchell and Plotkin - 1988 - Abstract types have existential type.pdf:/home/mrl/.local/share/zotero/storage/QXDE5H7C/Mitchell and Plotkin - 1988 - Abstract types have existential type.pdf:application/pdf},
 288 }
 289
 290 @inproceedings{steenvoorden_tophat_2019,
 291         address = {New York, NY, USA},
 292         series = {{PPDP} '19},
 293         title = {{TopHat}: {A} {Formal} {Foundation} for {Task}-{Oriented} {Programming}},
 294         isbn = {978-1-4503-7249-7},
 295         url = {https://doi.org/10.1145/3354166.3354182},
 296         doi = {10.1145/3354166.3354182},
 297         abstract = {Software that models how people work is omnipresent in today's society. Current languages and frameworks often focus on usability by non-programmers, sacrificing flexibility and high level abstraction. Task-oriented programming (TOP) is a programming paradigm that aims to provide the desired level of abstraction while still being expressive enough to describe real world collaboration. It prescribes a declarative programming style to specify multi-user workflows. Workflows can be higher-order. They communicate through typed values on a local and global level. Such specifications can be turned into interactive applications for different platforms, supporting collaboration during execution. TOP has been around for more than a decade, in the forms of iTasks and mTasks, which are tailored for real-world usability. So far, it has not been given a formalisation which is suitable for formal reasoning.In this paper we give a description of the TOP paradigm and then decompose its rich features into elementary language elements, which makes them suitable for formal treatment. We use the simply typed lambda-calculus, extended with pairs and references, as a base language. On top of this language, we develop TopHat, a language for modular interactive workflows. We describe TopHat by means of a layered semantics. These layers consist of multiple big-step evaluations on expressions, and two labelled transition systems, handling user inputs.With TopHat we prepare a way to formally reason about TOP languages and programs. This approach allows for comparison with other work in the field. We have implemented the semantic rules of TopHat in Haskell, and the task layer on top of the iTasks framework. This shows that our approach is feasible, and lets us demonstrate the concepts by means of illustrative case studies. TOP has been applied in projects with the Dutch coast guard, tax office, and navy. Our work matters because formal program verification is important for mission-critical software, especially for systems with concurrency.},
 298         booktitle = {Proceedings of the 21st {International} {Symposium} on {Principles} and {Practice} of {Declarative} {Programming}},
 299         publisher = {Association for Computing Machinery},
 300         author = {Steenvoorden, Tim and Naus, Nico and Klinik, Markus},
 301         year = {2019},
 302         note = {event-place: Porto, Portugal},
 303         file = {Steenvoorden et al. - 2019 - TopHat A Formal Foundation for Task-Oriented Prog.pdf:/home/mrl/.local/share/zotero/storage/W7HJ5MEF/Steenvoorden et al. - 2019 - TopHat A Formal Foundation for Task-Oriented Prog.pdf:application/pdf},
 304 }
 305
 306 @inproceedings{yorgey_giving_2012,
 307         address = {New York, NY, USA},
 308         series = {{TLDI} '12},
 309         title = {Giving {Haskell} a {Promotion}},
 310         isbn = {978-1-4503-1120-5},
 311         url = {https://doi.org/10.1145/2103786.2103795},
 312         doi = {10.1145/2103786.2103795},
 313         abstract = {Static type systems strive to be richly expressive while still being simple enough for programmers to use. We describe an experiment that enriches Haskell's kind system with two features promoted from its type system: data types and polymorphism. The new system has a very good power-to-weight ratio: it offers a significant improvement in expressiveness, but, by re-using concepts that programmers are already familiar with, the system is easy to understand and implement.},
 314         booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} {Workshop} on {Types} in {Language} {Design} and {Implementation}},
 315         publisher = {Association for Computing Machinery},
 316         author = {Yorgey, Brent A. and Weirich, Stephanie and Cretin, Julien and Peyton Jones, Simon and Vytiniotis, Dimitrios and Magalhães, José Pedro},
 317         year = {2012},
 318         note = {event-place: Philadelphia, Pennsylvania, USA},
 319         keywords = {haskell, kinds, polymorphism, promotion},
 320         pages = {53--66},
 321         file = {Yorgey et al. - 2012 - Giving Haskell a Promotion.pdf:/home/mrl/.local/share/zotero/storage/7GTDGQ3I/Yorgey et al. - 2012 - Giving Haskell a Promotion.pdf:application/pdf},
 322 }
 323
 324 @inproceedings{atkey_unembedding_2009,
 325         address = {New York, NY, USA},
 326         series = {Haskell '09},
 327         title = {Unembedding {Domain}-{Specific} {Languages}},
 328         isbn = {978-1-60558-508-6},
 329         url = {https://doi.org/10.1145/1596638.1596644},
 330         doi = {10.1145/1596638.1596644},
 331         abstract = {Higher-order abstract syntax provides a convenient way of embedding domain-specific languages, but is awkward to analyse and manipulate directly. We explore the boundaries of higher-order abstract syntax. Our key tool is the unembedding of embedded terms as de Bruijn terms, enabling intensional analysis. As part of our solution we present techniques for separating the definition of an embedded program from its interpretation, giving modular extensions of the embedded language, and different ways to encode the types of the embedded language.},
 332         booktitle = {Proceedings of the 2nd {ACM} {SIGPLAN} {Symposium} on {Haskell}},
 333         publisher = {Association for Computing Machinery},
 334         author = {Atkey, Robert and Lindley, Sam and Yallop, Jeremy},
 335         year = {2009},
 336         note = {event-place: Edinburgh, Scotland},
 337         keywords = {domain-specific languages, higher-order abstract syntax, type classes, unembedding},
 338         pages = {37--48},
 339         file = {Atkey et al. - 2009 - Unembedding Domain-Specific Languages.pdf:/home/mrl/.local/share/zotero/storage/GVFRIDUG/Atkey et al. - 2009 - Unembedding Domain-Specific Languages.pdf:application/pdf},
 340 }
 341
 342 @inproceedings{krishnamurthi_synthesizing_1998,
 343         address = {Berlin, Heidelberg},
 344         title = {Synthesizing object-oriented and functional design to promote re-use},
 345         isbn = {978-3-540-69064-1},
 346         abstract = {Many problems require recursively specified types of data and a collection of tools that operate on those data. Over time, these problems evolve so that the programmer must extend the toolkit or extend the types and adjust the existing tools accordingly. Ideally, this should be done without modifying existing code. Unfortunately, the prevailing program design strategies do not support both forms of extensibility: functional programming accommodates the addition of tools, while object-oriented programming supports either adding new tools or extending the data set, but not both. In this paper, we present a composite design pattern that synthesizes the best of both approaches and in the process resolves the tension between the two design strategies. We also show how this protocol suggests a new set of linguistic facilities for languages that support class systems.},
 347         booktitle = {{ECOOP}'98 — {Object}-{Oriented} {Programming}},
 348         publisher = {Springer Berlin Heidelberg},
 349         author = {Krishnamurthi, Shriram and Felleisen, Matthias and Friedman, Daniel P.},
 350         editor = {Jul, Eric},
 351         year = {1998},
 352         note = {event-place: Brussels, Belgium},
 353         pages = {91--113},
 354         file = {Krishnamurthi et al. - 1998 - Synthesizing object-oriented and functional design.pdf:/home/mrl/.local/share/zotero/storage/AMMULPPT/Krishnamurthi et al. - 1998 - Synthesizing object-oriented and functional design.pdf:application/pdf},
 355 }
 356
 357 @incollection{gibbons_functional_2015,
 358         address = {Cham},
 359         title = {Functional {Programming} for {Domain}-{Specific} {Languages}},
 360         isbn = {978-3-319-15940-9},
 361         url = {https://doi.org/10.1007/978-3-319-15940-9_1},
 362         abstract = {Domain-specific languages are a popular application area for functional programming; and conversely, functional programming is a popular implementation vehicle for domain-specific languages—at least, for embedded ones. Why is this? The appeal of embedded domain-specific languages is greatly enhanced by the presence of convenient lightweight tools for defining, implementing, and optimising new languages; such tools represent one of functional programming's strengths. In these lectures we discuss functional programming techniques for embedded domain-specific languages; we focus especially on algebraic datatypes and higher-order functions, and their influence on deep and shallow embeddings.},
 363         booktitle = {Central {European} {Functional} {Programming} {School}: 5th {Summer} {School}, {CEFP} 2013, {Cluj}-{Napoca}, {Romania}, {July} 8-20, 2013, {Revised} {Selected} {Papers}},
 364         publisher = {Springer International Publishing},
 365         author = {Gibbons, Jeremy},
 366         editor = {Zsók, Viktória and Horváth, Zoltán and Csató, Lehel},
 367         year = {2015},
 368         doi = {10.1007/978-3-319-15940-9_1},
 369         pages = {1--28},
 370         file = {Gibbons - 2015 - Functional Programming for Domain-Specific Languag.pdf:/home/mrl/.local/share/zotero/storage/ARUBLFU6/Gibbons - 2015 - Functional Programming for Domain-Specific Languag.pdf:application/pdf},
 371 }
 372
 373 @incollection{lubbers_writing_2019,
 374         address = {Cham},
 375         title = {Writing {Internet} of {Things} applications with {Task} {Oriented} {Programming}},
 376         abstract = {The Internet of Things (IOT) is growing fast. In 2018, there was approximately one connected device per person on earth and the number has been growing ever since. The devices interact with the environment via diﬀerent modalities at the same time using sensors and actuators making the programs parallel. Yet, writing this type of programs is diﬃcult because the devices have little computation power and memory, the platforms are heterogeneous and the languages are low level. Task Oriented Programming (TOP) is a novel declarative programming language paradigm that is used to express coordination of work, collaboration of users and systems, the distribution of shared data and the human computer interaction. The mTask language is a specialized, yet full-ﬂedged, multi-backend TOP language for IOT devices. With the bytecode interpretation backend and the integration with iTasks, tasks can be executed on the device dynamically. This means that —according to the current state of aﬀairs— tasks can be tailor-made at run time, compiled to device-agnostic bytecode and shipped to the device for interpretation. Tasks sent to the device are fully integrated in iTasks to allow every form of interaction with the tasks such as observation of the task value and interaction with Shared Data Sources (SDSs). The application is —server and devices— are programmed in a single language, albeit using two embedded Domain Speciﬁc Languages (EDSLs).},
 377         language = {en},
 378         booktitle = {Central {European} {Functional} {Programming} {School}: 8th {Summer} {School}, {CEFP} 2019, {Budapest}, {Hungary}, {July} 17–21, 2019, {Revised} {Selected} {Papers}},
 379         publisher = {Springer International Publishing},
 380         author = {Lubbers, Mart and Koopman, Pieter and Plasmeijer, Rinus},
 381         year = {2019},
 382         pages = {51},
 383         file = {Lubbers - Writing Internet of Things applications with Task .pdf:/home/mrl/.local/share/zotero/storage/ILZIBYW5/Lubbers - Writing Internet of Things applications with Task .pdf:application/pdf},
 384 }
 385
 386 @mastersthesis{veen_van_der_mutable_2020,
 387         address = {Nijmegen},
 388         title = {Mutable {Collection} {Types} in {Shallow} {Embedded} {DSLs}},
 389         language = {en},
 390         school = {Radboud University},
 391         author = {Veen, van der, Erin},
 392         month = jun,
 393         year = {2020},
 394         file = {thesis_final.pdf:/home/mrl/.local/share/zotero/storage/Y9QWGGB9/thesis_final.pdf:application/pdf},
 395 }
 396
 397 @phdthesis{alimarine_generic_2005,
 398         address = {Nijmegen},
 399         type = {{PhD}},
 400         title = {Generic {Functional} {Programming}},
 401         language = {en},
 402         school = {Radboud University},
 403         author = {Alimarine, Artem},
 404         year = {2005},
 405         file = {Alimarine - Generic Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/PDTS3SGX/Alimarine - Generic Functional Programming.pdf:application/pdf},
 406 }
 407
 408 @phdthesis{boer_de_secure_2020,
 409         address = {Nijmegen},
 410         type = {Bachelor's {Thesis}},
 411         title = {Secure {Communication} {Channels} for the {mTask} {System}.},
 412         language = {en},
 413         school = {Radboud University},
 414         author = {Boer, de, Michel},
 415         month = jun,
 416         year = {2020},
 417         file = {Boer, de - 2020 - Secure Communication Channels for the mTask System.pdf:/home/mrl/.local/share/zotero/storage/C46E3FBF/Boer, de - 2020 - Secure Communication Channels for the mTask System.pdf:application/pdf},
 418 }
 419
 420 @inproceedings{barendregt_towards_1987,
 421         title = {Towards an intermediate language for graph rewriting},
 422         volume = {1},
 423         booktitle = {{PARLE}, {Parallel} {Architectures} and {Languages} {Europe}},
 424         publisher = {Springer Verlag},
 425         author = {Barendregt, HP and van Eekelen, MCJD and Glauert, JRW and Kennaway, JR and Plasmeijer, MJ and Sleep, MR},
 426         year = {1987},
 427         pages = {159--174},
 428         file = {barh87-Lean.ps.gz:/home/mrl/.local/share/zotero/storage/63FBHND7/barh87-Lean.ps.gz:application/gzip},
 429 }
 430
 431 @incollection{wang_maintaining_2018,
 432         address = {Cham},
 433         title = {Maintaining {Separation} of {Concerns} {Through} {Task} {Oriented} {Software} {Development}},
 434         volume = {10788},
 435         isbn = {978-3-319-89718-9 978-3-319-89719-6},
 436         url = {http://link.springer.com/10.1007/978-3-319-89719-6_2},
 437         abstract = {Task Oriented Programming is a programming paradigm that enhances ‘classic’ functional programming with means to express the coordination of work among people and computer systems, the distribution and control of data sources, and the human-machine interfaces. To make the creation process of such applications feasible, it is important to have separation of concerns. In this paper we demonstrate how this is achieved within the Task Oriented Software Development process and illustrate the approach by means of a case study.},
 438         language = {en},
 439         urldate = {2019-01-14},
 440         booktitle = {Trends in {Functional} {Programming}},
 441         publisher = {Springer International Publishing},
 442         author = {Stutterheim, Jurriën and Achten, Peter and Plasmeijer, Rinus},
 443         editor = {Wang, Meng and Owens, Scott},
 444         year = {2018},
 445         doi = {10.1007/978-3-319-89719-6},
 446         pages = {19--38},
 447         file = {Stutterheim et al. - 2018 - Maintaining Separation of Concerns Through Task Or.pdf:/home/mrl/.local/share/zotero/storage/4GXJEM2U/Stutterheim et al. - 2018 - Maintaining Separation of Concerns Through Task Or.pdf:application/pdf},
 448 }
 449
 450 @article{barendsen_uniqueness_1996,
 451         title = {Uniqueness typing for functional languages with graph rewriting semantics},
 452         volume = {6},
 453         number = {6},
 454         journal = {Mathematical structures in computer science},
 455         author = {Barendsen, Erik and Smetsers, Sjaak},
 456         year = {1996},
 457         pages = {579--612},
 458         file = {Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:/home/mrl/.local/share/zotero/storage/BPRC6KJK/Barendsen and Smetsers - 1996 - Uniqueness typing for functional languages with gr.pdf:application/pdf},
 459 }
 460
 461 @inproceedings{lijnse_itasks_2009,
 462         title = {{iTasks} 2: {iTasks} for {End}-users},
 463         booktitle = {International {Symposium} on {Implementation} and {Application} of {Functional} {Languages}},
 464         publisher = {Springer},
 465         author = {Lijnse, Bas and Plasmeijer, Rinus},
 466         year = {2009},
 467         pages = {36--54},
 468         file = {Lijnse and Plasmeijer - 2009 - iTasks 2 iTasks for End-users.pdf:/home/mrl/.local/share/zotero/storage/KACEWKXY/Lijnse and Plasmeijer - 2009 - iTasks 2 iTasks for End-users.pdf:application/pdf},
 469 }
 470
 471 @mastersthesis{bohm_asynchronous_2019,
 472         address = {Nijmegen},
 473         title = {Asynchronous {Actions} in a {Synchronous} {World}},
 474         abstract = {This thesis introduces a system for asynchronous communication in the iTasks framework. The
 475 framework is written in Clean, a pure, lazy, functional language. Tasks need to be able to access
 476 data in the system and retrieve data from all kinds of data sources. The share system allows
 477 tasks to read arbitrary data sources and provides a simple interface that allows composition of
 478 different data sources. This system allows tasks to share and store data in an efficient, re-usable
 479 way.
 480 A disadvantage of the share system is that it does not allow asynchronous evaluation. When
 481 one task is using a share, other tasks have to wait for the full evaluation of this share before they
 482 can be evaluated. This has the effect that users in the iTasks framework must wait on other
 483 users. This results in poor user experience.
 484 We implement a share system which, by way of share rewriting, allows asynchronous evalua-
 485 tion. The system can be used to communicate with arbitrary services on the internet, as well as
 486 to communicate between different iTasks servers in a distributed context.
 487 We show how asynchronous shares are implemented and what the limitations are. We also
 488 show multiple practical examples of using asynchronous shares. The new system can be effectively
 489 used to consume services on the internet. It fits nicely into existing iTasks programs and requires
 490 few changes in existing programs.},
 491         language = {en},
 492         school = {Radboud University},
 493         author = {Böhm, Haye},
 494         month = jan,
 495         year = {2019},
 496         file = {Bohm - Asynchronous Actions in a Synchronous World.pdf:/home/mrl/.local/share/zotero/storage/D3IYPAM5/Bohm - Asynchronous Actions in a Synchronous World.pdf:application/pdf},
 497 }
 498
 499 @inproceedings{hentschel_supersensors:_2016,
 500         address = {Vienna, Austria},
 501         title = {Supersensors: {Raspberry} {Pi} {Devices} for {Smart} {Campus} {Infrastructure}},
 502         isbn = {978-1-5090-4052-0},
 503         shorttitle = {Supersensors},
 504         url = {http://ieeexplore.ieee.org/document/7575844/},
 505         doi = {10.1109/FiCloud.2016.16},
 506         abstract = {We describe an approach for developing a campuswide sensor network using commodity single board computers. We sketch various use cases for environmental sensor data, for different university stakeholders. Our key premise is that supersensors—sensors with signiﬁcant compute capability—enable more ﬂexible data collection, processing and reaction. In this paper, we describe the initial prototype deployment of our supersensor system in a single department at the University of Glasgow.},
 507         language = {en},
 508         urldate = {2019-09-04},
 509         booktitle = {2016 {IEEE} 4th {International} {Conference} on {Future} {Internet} of {Things} and {Cloud} ({FiCloud})},
 510         publisher = {IEEE},
 511         author = {Hentschel, Kristian and Jacob, Dejice and Singer, Jeremy and Chalmers, Matthew},
 512         month = aug,
 513         year = {2016},
 514         pages = {58--62},
 515         file = {Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:/home/mrl/.local/share/zotero/storage/ATK53FN2/Hentschel et al. - 2016 - Supersensors Raspberry Pi Devices for Smart Campu.pdf:application/pdf},
 516 }
 517
 518 @inproceedings{feijs_multi-tasking_2013,
 519         address = {Wuxi, China},
 520         title = {Multi-tasking and {Arduino} : why and how?},
 521         isbn = {978-90-386-3462-3},
 522         abstract = {In this article I argue that it is important to develop experiential prototypes which have multi-tasking capabilities. At the same time I show that for embedded prototype software based on the popular Arduino platform this is not too difficult. The approach is explained and illustrated using technical examples – practical and hands-on, down to the code level. At the same time a few helpful notations for designing and documenting the software are introduced and illustrated by the same examples. Finally a few case studies of the technical approach are listed.},
 523         language = {English},
 524         booktitle = {Design and semantics of form and movement. 8th {International} {Conference} on {Design} and {Semantics} of {Form} and {Movement} ({DeSForM} 2013)},
 525         author = {Feijs, Loe},
 526         editor = {Chen, L. L. and Djajadiningrat, T. and Feijs, L. M. G. and Fraser, S. and Hu, J. and Kyffin, S. and Steffen, D.},
 527         year = {2013},
 528         pages = {119--127},
 529         file = {Feijs - 2013 - Multi-tasking and Arduino why and how.pdf:/home/mrl/.local/share/zotero/storage/8A3Q8LHA/Feijs - 2013 - Multi-tasking and Arduino why and how.pdf:application/pdf},
 530 }
 531
 532 @misc{achten_clean_2007,
 533         title = {Clean for {Haskell98} {Programmers}},
 534         url = {https://www.mbsd.cs.ru.nl/publications/papers/2007/achp2007-CleanHaskellQuickGuide.pdf},
 535         language = {en},
 536         author = {Achten, Peter},
 537         month = jul,
 538         year = {2007},
 539         file = {Achten - Clean for Haskell98 Programmers.pdf:/home/mrl/.local/share/zotero/storage/69WWSGLF/Achten - Clean for Haskell98 Programmers.pdf:application/pdf},
 540 }
 541
 542 @inproceedings{baccelli_reprogramming_2018,
 543         title = {Reprogramming {Low}-end {IoT} {Devices} from the {Cloud}},
 544         booktitle = {2018 3rd {Cloudification} of the {Internet} of {Things} ({CIoT})},
 545         publisher = {IEEE},
 546         author = {Baccelli, Emmanuel and Doerr, Joerg and Jallouli, Ons and Kikuchi, Shinji and Morgenstern, Andreas and Padilla, Francisco Acosta and Schleiser, Kaspar and Thomas, Ian},
 547         year = {2018},
 548         pages = {1--6},
 549         file = {Baccelli et al. - 2018 - Reprogramming Low-end IoT Devices from the Cloud.pdf:/home/mrl/.local/share/zotero/storage/M6LX5ZJN/Baccelli et al. - 2018 - Reprogramming Low-end IoT Devices from the Cloud.pdf:application/pdf},
 550 }
 551
 552 @mastersthesis{piers_task-oriented_2016,
 553         address = {Nijmegen},
 554         title = {Task-{Oriented} {Programming} for developing non-distributed interruptible embedded systems},
 555         language = {en},
 556         school = {Radboud University},
 557         author = {Piers, Jasper},
 558         year = {2016},
 559         file = {Piers - Task-Oriented Programming for developing non-distr.pdf:/home/mrl/.local/share/zotero/storage/X8BZM9D4/Piers - Task-Oriented Programming for developing non-distr.pdf:application/pdf},
 560 }
 561
 562 @inproceedings{baccelli_scripting_2018,
 563         title = {Scripting {Over}-{The}-{Air}: {Towards} {Containers} on {Low}-end {Devices} in the {Internet} of {Things}},
 564         booktitle = {{IEEE} {PerCom} 2018},
 565         author = {Baccelli, Emmanuel and Doerr, Joerg and Kikuchi, Shinji and Padilla, Francisco and Schleiser, Kaspar and Thomas, Ian},
 566         year = {2018},
 567         file = {Baccelli et al. - Scripting Over-The-Air Towards Containers on Low-.pdf:/home/mrl/.local/share/zotero/storage/98UTMFAC/Baccelli et al. - Scripting Over-The-Air Towards Containers on Low-.pdf:application/pdf},
 568 }
 569
 570 @mastersthesis{amazonas_cabral_de_andrade_developing_2018,
 571         address = {Nijmegen},
 572         title = {Developing {Real} {Life}, {Task} {Oriented} {Applications} for the {Internet} of {Things}},
 573         shorttitle = {Developing {Real} {Life}, {TOP} {Applications} for the {IOT}},
 574         language = {en},
 575         school = {Radboud University},
 576         author = {Amazonas Cabral De Andrade, Matheus},
 577         year = {2018},
 578         file = {Lubbers - prof. dr. dr.h.c. ir. M.J. Plasmeijer.pdf:/home/mrl/.local/share/zotero/storage/JXPEWS85/Lubbers - prof. dr. dr.h.c. ir. M.J. Plasmeijer.pdf:application/pdf},
 579 }
 580
 581 @article{swierstra_data_2008,
 582         title = {Data types à la carte},
 583         volume = {18},
 584         doi = {10.1017/S0956796808006758},
 585         number = {4},
 586         journal = {Journal of functional programming},
 587         author = {Swierstra, Wouter},
 588         year = {2008},
 589         pages = {423--436},
 590         file = {swierstra2008.pdf:/home/mrl/.local/share/zotero/storage/BEQKBXWP/swierstra2008.pdf:application/pdf},
 591 }
 592
 593 @article{groningen_exchanging_2010,
 594         title = {Exchanging sources between {Clean} and {Haskell}: {A} double-edged front end for the {Clean} compiler},
 595         volume = {45},
 596         shorttitle = {Exchanging sources between {Clean} and {Haskell}},
 597         number = {11},
 598         journal = {ACM Sigplan Notices},
 599         author = {Groningen, John van and Noort, Thomas van and Achten, Peter and Koopman, Pieter and Plasmeijer, Rinus},
 600         year = {2010},
 601         pages = {49--60},
 602         file = {groj10-Haskell_front_end_Clean.pdf:/home/mrl/.local/share/zotero/storage/WVZWX8WT/groj10-Haskell_front_end_Clean.pdf:application/pdf},
 603 }
 604
 605 @article{plasmeijer_itasks:_2007,
 606         title = {{iTasks}: executable specifications of interactive work flow systems for the web},
 607         volume = {42},
 608         number = {9},
 609         journal = {ACM SIGPLAN Notices},
 610         author = {Plasmeijer, Rinus and Achten, Peter and Koopman, Pieter},
 611         year = {2007},
 612         pages = {141--152},
 613         file = {plar2007-ICFP07-iTasks.pdf:/home/mrl/.local/share/zotero/storage/N8EUZP7D/plar2007-ICFP07-iTasks.pdf:application/pdf},
 614 }
 615
 616 @incollection{plasmeijer_shallow_2016,
 617         address = {Cham},
 618         series = {Lecture {Notes} in {Computer} {Science}},
 619         title = {A {Shallow} {Embedded} {Type} {Safe} {Extendable} {DSL} for the {Arduino}},
 620         volume = {9547},
 621         isbn = {978-3-319-39110-6},
 622         url = {http://link.springer.com/10.1007/978-3-319-39110-6},
 623         urldate = {2017-02-22},
 624         booktitle = {Trends in {Functional} {Programming}},
 625         publisher = {Springer International Publishing},
 626         author = {Plasmeijer, Rinus and Koopman, Pieter},
 627         year = {2016},
 628         doi = {10.1007/978-3-319-39110-6},
 629         file = {chp%3A10.1007%2F978-3-319-39110-6_6.pdf:/home/mrl/.local/share/zotero/storage/TJVP6FHF/chp%3A10.1007%2F978-3-319-39110-6_6.pdf:application/pdf},
 630 }
 631
 632 @inproceedings{cheney_lightweight_2002,
 633         title = {A lightweight implementation of generics and dynamics},
 634         url = {http://dl.acm.org/citation.cfm?id=581698},
 635         doi = {10.1145/581690.581698},
 636         urldate = {2017-05-15},
 637         booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} workshop on {Haskell}},
 638         publisher = {ACM},
 639         author = {Cheney, James and Hinze, Ralf},
 640         year = {2002},
 641         note = {event-place: Pittsburgh Pennsylvania, USA},
 642         keywords = {dynamic typing, generic programming, type representations},
 643         pages = {90--104},
 644         file = {Cheney and Hinze - 2002 - A lightweight implementation of generics and dynam.pdf:/home/mrl/.local/share/zotero/storage/FZ6EGJRJ/Cheney and Hinze - 2002 - A lightweight implementation of generics and dynam.pdf:application/pdf;HW02.pdf:/home/mrl/.local/share/zotero/storage/A8Z49NK6/HW02.pdf:application/pdf},
 645 }
 646
 647 @article{lilis_survey_2019,
 648         title = {A {Survey} of {Metaprogramming} {Languages}},
 649         volume = {52},
 650         issn = {0360-0300},
 651         url = {https://doi.org/10.1145/3354584},
 652         doi = {10.1145/3354584},
 653         abstract = {Metaprogramming is the process of writing computer programs that treat programs as data, enabling them to analyze or transform existing programs or generate new ones. While the concept of metaprogramming has existed for several decades, activities focusing on metaprogramming have been increasing rapidly over the past few years, with most languages offering some metaprogramming support and the amount of metacode being developed growing exponentially. In this article, we introduce a taxonomy of metaprogramming languages and present a survey of metaprogramming languages and systems based on the taxonomy. Our classification is based on the metaprogramming model adopted by the language, the phase of the metaprogram evaluation, the metaprogram source location, and the relation between the metalanguage and the object language.},
 654         number = {6},
 655         journal = {ACM Comput. Surv.},
 656         author = {Lilis, Yannis and Savidis, Anthony},
 657         month = oct,
 658         year = {2019},
 659         note = {Place: New York, NY, USA
 660 Publisher: Association for Computing Machinery},
 661         keywords = {aspect-oriented programming, generative programming, macro systems, meta-object protocols, Metaprogramming, multistage languages, reflection},
 662         file = {Lilis and Savidis - 2019 - A Survey of Metaprogramming Languages.pdf:/home/mrl/.local/share/zotero/storage/9MS6TUNR/Lilis and Savidis - 2019 - A Survey of Metaprogramming Languages.pdf:application/pdf},
 663 }
 664
 665 @inproceedings{mainland_why_2007,
 666         address = {New York, NY, USA},
 667         series = {Haskell '07},
 668         title = {Why {It}'s {Nice} to {Be} {Quoted}: {Quasiquoting} for {Haskell}},
 669         isbn = {978-1-59593-674-5},
 670         url = {https://doi.org/10.1145/1291201.1291211},
 671         doi = {10.1145/1291201.1291211},
 672         abstract = {Quasiquoting allows programmers to use domain specific syntax to construct program fragments. By providing concrete syntax for complex data types, programs become easier to read, easier to write, and easier to reason about and maintain. Haskell is an excellent host language for embedded domain specific languages, and quasiquoting ideally complements the language features that make Haskell perform so well in this area. Unfortunately, until now no Haskell compiler has provided support for quasiquoting. We present an implementation in GHC and demonstrate that by leveraging existing compiler capabilities, building a full quasiquoter requires little more work than writing a parser. Furthermore, we provide a compile-time guarantee that all quasiquoted data is type-correct.},
 673         booktitle = {Proceedings of the {ACM} {SIGPLAN} {Workshop} on {Haskell} {Workshop}},
 674         publisher = {Association for Computing Machinery},
 675         author = {Mainland, Geoffrey},
 676         year = {2007},
 677         note = {event-place: Freiburg, Germany},
 678         keywords = {meta programming, quasiquoting},
 679         pages = {73--82},
 680         file = {Mainland - 2007 - Why It's Nice to Be Quoted Quasiquoting for Haske.pdf:/home/mrl/.local/share/zotero/storage/PSJ59GY2/Mainland - 2007 - Why It's Nice to Be Quoted Quasiquoting for Haske.pdf:application/pdf},
 681 }
 682
 683 @article{tratt_domain_2008,
 684         title = {Domain {Specific} {Language} {Implementation} via {Compile}-{Time} {Meta}-{Programming}},
 685         volume = {30},
 686         issn = {0164-0925},
 687         url = {https://doi.org/10.1145/1391956.1391958},
 688         doi = {10.1145/1391956.1391958},
 689         abstract = {Domain specific languages (DSLs) are mini-languages that are increasingly seen as being a valuable tool for software developers and non-developers alike. DSLs must currently be created in an ad-hoc fashion, often leading to high development costs and implementations of variable quality. In this article, I show how expressive DSLs can be hygienically embedded in the Converge programming language using its compile-time meta-programming facility, the concept of DSL blocks, and specialised error reporting techniques. By making use of pre-existing facilities, and following a simple methodology, DSL implementation costs can be significantly reduced whilst leading to higher quality DSL implementations.},
 690         number = {6},
 691         journal = {ACM Trans. Program. Lang. Syst.},
 692         author = {Tratt, Laurence},
 693         month = oct,
 694         year = {2008},
 695         note = {Place: New York, NY, USA
 696 Publisher: Association for Computing Machinery},
 697         keywords = {domain specific languages, compile-time meta-programming, Syntax extension},
 698         file = {Tratt - 2008 - Domain Specific Language Implementation via Compil.pdf:/home/mrl/.local/share/zotero/storage/HHGYJK4H/Tratt - 2008 - Domain Specific Language Implementation via Compil.pdf:application/pdf},
 699 }
 700
 701 @inproceedings{kariotis_making_2008,
 702         address = {New York, NY, USA},
 703         series = {Haskell '08},
 704         title = {Making {Monads} {First}-{Class} with {Template} {Haskell}},
 705         isbn = {978-1-60558-064-7},
 706         url = {https://doi.org/10.1145/1411286.1411300},
 707         doi = {10.1145/1411286.1411300},
 708         abstract = {Monads as an organizing principle for programming and semantics are notoriously difficult to grasp, yet they are a central and powerful abstraction in Haskell. This paper introduces a domain-specific language, MonadLab, that simplifies the construction of monads, and describes its implementation in Template Haskell. MonadLab makes monad construction truly first class, meaning that arcane theoretical issues with respect to monad transformers are completely hidden from the programmer. The motivation behind the design of MonadLab is to make monadic programming in Haskell simpler while providing a tool for non-Haskell experts that will assist them in understanding this powerful abstraction.},
 709         booktitle = {Proceedings of the {First} {ACM} {SIGPLAN} {Symposium} on {Haskell}},
 710         publisher = {Association for Computing Machinery},
 711         author = {Kariotis, Pericles S. and Procter, Adam M. and Harrison, William L.},
 712         year = {2008},
 713         note = {event-place: Victoria, BC, Canada},
 714         keywords = {domain-specific languages, monads, staged programming},
 715         pages = {99--110},
 716         file = {Kariotis et al. - 2008 - Making Monads First-Class with Template Haskell.pdf:/home/mrl/.local/share/zotero/storage/ZLX24WE8/Kariotis et al. - 2008 - Making Monads First-Class with Template Haskell.pdf:application/pdf},
 717 }
 718
 719 @inproceedings{gill_haskell_2009,
 720         address = {Berlin, Heidelberg},
 721         title = {A {Haskell} {Hosted} {DSL} for {Writing} {Transformation} {Systems}},
 722         isbn = {978-3-642-03034-5},
 723         abstract = {KURE is a Haskell hosted Domain Specific Language (DSL) for writing transformation systems based on rewrite strategies. When writing transformation systems, a significant amount of engineering effort goes into setting up plumbing to make sure that specific rewrite rules can fire. Systems like Stratego and Strafunski provide most of this plumbing as infrastructure, allowing the DSL user to focus on the rewrite rules. KURE is a strongly typed strategy control language in the tradition of Stratego and Strafunski. It is intended for writing reasonably efficient rewrite systems, makes use of type families to provide a delimited generic mechanism for tree rewriting, and provides support for efficient identity rewrite detection.},
 724         booktitle = {Domain-{Specific} {Languages}},
 725         publisher = {Springer Berlin Heidelberg},
 726         author = {Gill, Andy},
 727         editor = {Taha, Walid Mohamed},
 728         year = {2009},
 729         pages = {285--309},
 730         file = {Gill2009_Chapter_AHaskellHostedDSLForWritingTra.pdf:/home/mrl/.local/share/zotero/storage/I9RJNDYR/Gill2009_Chapter_AHaskellHostedDSLForWritingTra.pdf:application/pdf},
 731 }
 732
 733 @book{peyton_jones_implementation_1987,
 734         address = {Hertfordshire},
 735         title = {The {Implementation} of {Functional} {Programming} {Languages}},
 736         url = {https://www.microsoft.com/en-us/research/publication/the-implementation-of-functional-programming-languages/},
 737         abstract = {My 1987 book is now out of print, but it is available here in its entirety in PDF form, in one of two formats: single-page portrait double-page landscape Both are fully searchable, thanks to OCR and Norman Ramsey. Errata Section 5.2.4, p87. We need an extra rule match us [] E = E This accounts for the possibility that in the constructor rule (Section 5.2.4) there may be some non-nullary constructors for which there are no equations. P168, line 2, "VAR" should be "TVAR".},
 738         publisher = {Prentice Hall},
 739         author = {Peyton Jones, Simon},
 740         month = jan,
 741         year = {1987},
 742         file = {Peyton Jones - 1987 - The Implementation of Functional Programming Langu.pdf:/home/mrl/.local/share/zotero/storage/9RIR6KGD/Peyton Jones - 1987 - The Implementation of Functional Programming Langu.pdf:application/pdf},
 743 }
 744
 745 @inproceedings{sheard_template_2002,
 746         address = {New York, NY, USA},
 747         series = {Haskell '02},
 748         title = {Template {Meta}-{Programming} for {Haskell}},
 749         isbn = {1-58113-605-6},
 750         url = {https://doi.org/10.1145/581690.581691},
 751         doi = {10.1145/581690.581691},
 752         abstract = {We propose a new extension to the purely functional programming language Haskell that supports compile-time meta-programming. The purpose of the system is to support the algorithmic construction of programs at compile-time.The ability to generate code at compile time allows the programmer to implement such features as polytypic programs, macro-like expansion, user directed optimization (such as inlining), and the generation of supporting data structures and functions from existing data structures and functions.Our design is being implemented in the Glasgow Haskell Compiler, ghc.},
 753         booktitle = {Proceedings of the 2002 {ACM} {SIGPLAN} {Workshop} on {Haskell}},
 754         publisher = {Association for Computing Machinery},
 755         author = {Sheard, Tim and Jones, Simon Peyton},
 756         year = {2002},
 757         note = {event-place: Pittsburgh, Pennsylvania},
 758         keywords = {meta programming, templates},
 759         pages = {1--16},
 760         file = {Sheard and Jones - 2002 - Template Meta-Programming for Haskell.pdf:/home/mrl/.local/share/zotero/storage/2GSK6DSF/Sheard and Jones - 2002 - Template Meta-Programming for Haskell.pdf:application/pdf},
 761 }
 762
 763 @inproceedings{seefried_optimising_2004,
 764         address = {Berlin, Heidelberg},
 765         title = {Optimising {Embedded} {DSLs} {Using} {Template} {Haskell}},
 766         isbn = {978-3-540-30175-2},
 767         abstract = {Embedded domain specific languages (EDSLs) provide a specialised language for a particular application area while harnessing the infrastructure of an existing general purpose programming language. The reduction in implementation costs that results from this approach comes at a price: the EDSL often compiles to inefficient code since the host language's compiler only optimises at the level of host language constructs. The paper presents an approach to solving this problem based on compile-time meta-programming which retains the simplicity of the embedded approach. We use PanTHeon, our implementation of an existing EDSL for image synthesis to demonstrate the benefits and drawbacks of this approach. Furthermore, we suggest potential improvements to Template Haskell, the meta-programming framework we are using, which would greatly improve its applicability to this kind of task.},
 768         booktitle = {Generative {Programming} and {Component} {Engineering}},
 769         publisher = {Springer Berlin Heidelberg},
 770         author = {Seefried, Sean and Chakravarty, Manuel and Keller, Gabriele},
 771         editor = {Karsai, Gabor and Visser, Eelco},
 772         year = {2004},
 773         pages = {186--205},
 774         file = {Seefried et al. - 2004 - Optimising Embedded DSLs Using Template Haskell.pdf:/home/mrl/.local/share/zotero/storage/ZRKQ9AH6/Seefried et al. - 2004 - Optimising Embedded DSLs Using Template Haskell.pdf:application/pdf},
 775 }
 776
 777 @article{hammond_automatic_2003,
 778         title = {{AUTOMATIC} {SKELETONS} {IN} {TEMPLATE} {HASKELL}},
 779         volume = {13},
 780         url = {https://doi.org/10.1142/S0129626403001380},
 781         doi = {10.1142/S0129626403001380},
 782         abstract = {This paper uses Template Haskell to automatically select appropriate skeleton implementations in the Eden parallel dialect of Haskell. The approach allows implementation parameters to be statically tuned according to architectural cost models based on source analyses. This permits us to target a range of parallel architecture classes from a single source specification. A major advantage of the approach is that cost models are user-definable and can be readily extended to new data or computation structures etc.},
 783         number = {03},
 784         journal = {Parallel Processing Letters},
 785         author = {Hammond, Kevin and Berthold, Jost and Loogen, Rita},
 786         year = {2003},
 787         pages = {413--424},
 788         file = {Hammond et al. - 2003 - AUTOMATIC SKELETONS IN TEMPLATE HASKELL.pdf:/home/mrl/.local/share/zotero/storage/HBQ8UXY3/Hammond et al. - 2003 - AUTOMATIC SKELETONS IN TEMPLATE HASKELL.pdf:application/pdf},
 789 }
 790
 791 @inproceedings{adams_template_2012,
 792         address = {New York, NY, USA},
 793         series = {Haskell '12},
 794         title = {Template {Your} {Boilerplate}: {Using} {Template} {Haskell} for {Efficient} {Generic} {Programming}},
 795         isbn = {978-1-4503-1574-6},
 796         url = {https://doi.org/10.1145/2364506.2364509},
 797         doi = {10.1145/2364506.2364509},
 798         abstract = {Generic programming allows the concise expression of algorithms that would otherwise require large amounts of handwritten code. A number of such systems have been developed over the years, but a common drawback of these systems is poor runtime performance relative to handwritten, non-generic code. Generic-programming systems vary significantly in this regard, but few consistently match the performance of handwritten code. This poses a dilemma for developers. Generic-programming systems offer concision but cost performance. Handwritten code offers performance but costs concision.This paper explores the use of Template Haskell to achieve the best of both worlds. It presents a generic-programming system for Haskell that provides both the concision of other generic-programming systems and the efficiency of handwritten code. Our system gives the programmer a high-level, generic-programming interface, but uses Template Haskell to generate efficient, non-generic code that outperforms existing generic-programming systems for Haskell.This paper presents the results of benchmarking our system against both handwritten code and several other generic-programming systems. In these benchmarks, our system matches the performance of handwritten code while other systems average anywhere from two to twenty times slower.},
 799         booktitle = {Proceedings of the 2012 {Haskell} {Symposium}},
 800         publisher = {Association for Computing Machinery},
 801         author = {Adams, Michael D. and DuBuisson, Thomas M.},
 802         year = {2012},
 803         note = {event-place: Copenhagen, Denmark},
 804         keywords = {generic programming, scrap your boilerplate, template haskell},
 805         pages = {13--24},
 806         file = {Adams and DuBuisson - 2012 - Template Your Boilerplate Using Template Haskell .pdf:/home/mrl/.local/share/zotero/storage/ANAHWLB5/Adams and DuBuisson - 2012 - Template Your Boilerplate Using Template Haskell .pdf:application/pdf},
 807 }
 808
 809 @inproceedings{norell_prototyping_2004,
 810         address = {Berlin, Heidelberg},
 811         title = {Prototyping {Generic} {Programming} in {Template} {Haskell}},
 812         isbn = {978-3-540-27764-4},
 813         abstract = {Generic Programming deals with the construction of programs that can be applied to many different datatypes. This is achieved by parameterizing the generic programs by the structure of the datatypes on which they are to be applied. Programs that can be defined generically range from simple map functions through pretty printers to complex XML tools.},
 814         booktitle = {Mathematics of {Program} {Construction}},
 815         publisher = {Springer Berlin Heidelberg},
 816         author = {Norell, Ulf and Jansson, Patrik},
 817         editor = {Kozen, Dexter},
 818         year = {2004},
 819         pages = {314--333},
 820         file = {Norell and Jansson - 2004 - Prototyping Generic Programming in Template Haskel.pdf:/home/mrl/.local/share/zotero/storage/S3EXD65Z/Norell and Jansson - 2004 - Prototyping Generic Programming in Template Haskel.pdf:application/pdf},
 821 }
 822
 823 @incollection{odonnell_embedding_2004,
 824         address = {Berlin, Heidelberg},
 825         title = {Embedding a {Hardware} {Description} {Language} in {Template} {Haskell}},
 826         isbn = {978-3-540-25935-0},
 827         url = {https://doi.org/10.1007/978-3-540-25935-0_9},
 828         abstract = {Hydra is a domain-specific language for designing digital circuits, which is implemented by embedding within Haskell. Many features required for hardware specification fit well within functional languages, leading in many cases to a perfect embedding. There are some situations, including netlist generation and software logic probes, where the DSL does not fit exactly within the host functional language. A new solution to these problems is based on program transformations performed automatically by metaprograms in Template Haskell.},
 829         booktitle = {Domain-{Specific} {Program} {Generation}: {International} {Seminar}, {Dagstuhl} {Castle}, {Germany}, {March} 23-28, 2003. {Revised} {Papers}},
 830         publisher = {Springer Berlin Heidelberg},
 831         author = {O'Donnell, John T.},
 832         editor = {Lengauer, Christian and Batory, Don and Consel, Charles and Odersky, Martin},
 833         year = {2004},
 834         doi = {10.1007/978-3-540-25935-0_9},
 835         pages = {143--164},
 836         file = {O'Donnell - 2004 - Embedding a Hardware Description Language in Templ.pdf:/home/mrl/.local/share/zotero/storage/Z2XT7SM3/O'Donnell - 2004 - Embedding a Hardware Description Language in Templ.pdf:application/pdf},
 837 }
 838
 839 @misc{lynagh_unrolling_2003,
 840         title = {Unrolling and {Simplifying} {Expressions} with {Template} {Haskell}},
 841         url = {http://web.comlab.ox.ac.uk/oucl/work/ian.lynagh/papers/},
 842         urldate = {2021-09-07},
 843         author = {Lynagh, Ian},
 844         month = may,
 845         year = {2003},
 846         file = {10.1.1.5.9813.pdf:/home/mrl/.local/share/zotero/storage/G4AFM8XZ/10.1.1.5.9813.pdf:application/pdf},
 847 }
 848
 849 @article{elliott_compiling_2003,
 850         title = {Compiling embedded languages},
 851         volume = {13},
 852         doi = {10.1017/S0956796802004574},
 853         number = {3},
 854         journal = {Journal of Functional Programming},
 855         author = {Elliott, Conal and Finne, Sigbjørn and de Moor, Oege},
 856         year = {2003},
 857         note = {Publisher: Cambridge University Press},
 858         pages = {455--481},
 859         file = {Elliott et al. - 2003 - Compiling embedded languages.pdf:/home/mrl/.local/share/zotero/storage/3X4Z6AKB/Elliott et al. - 2003 - Compiling embedded languages.pdf:application/pdf},
 860 }
 861
 862 @incollection{czarnecki_dsl_2004,
 863         address = {Berlin, Heidelberg},
 864         title = {{DSL} {Implementation} in {MetaOCaml}, {Template} {Haskell}, and {C}++},
 865         isbn = {978-3-540-25935-0},
 866         url = {https://doi.org/10.1007/978-3-540-25935-0_4},
 867         abstract = {A wide range of domain-specific languages (DSLs) has been implemented successfully by embedding them in general purpose languages. This paper reviews embedding, and summarizes how two alternative techniques – staged interpreters and templates – can be used to overcome the limitations of embedding. Both techniques involve a form of generative programming. The paper reviews and compares three programming languages that have special support for generative programming. Two of these languages (MetaOCaml and Template Haskell) are research languages, while the third (C++) is already in wide industrial use. The paper identifies several dimensions that can serve as a basis for comparing generative languages.},
 868         booktitle = {Domain-{Specific} {Program} {Generation}: {International} {Seminar}, {Dagstuhl} {Castle}, {Germany}, {March} 23-28, 2003. {Revised} {Papers}},
 869         publisher = {Springer Berlin Heidelberg},
 870         author = {Czarnecki, Krzysztof and O'Donnell, John T. and Striegnitz, Jörg and Taha, Walid},
 871         editor = {Lengauer, Christian and Batory, Don and Consel, Charles and Odersky, Martin},
 872         year = {2004},
 873         doi = {10.1007/978-3-540-25935-0_4},
 874         pages = {51--72},
 875         file = {Czarnecki et al. - 2004 - DSL Implementation in MetaOCaml, Template Haskell,.pdf:/home/mrl/.local/share/zotero/storage/U6E3325Q/Czarnecki et al. - 2004 - DSL Implementation in MetaOCaml, Template Haskell,.pdf:application/pdf},
 876 }
 877
 878 @inproceedings{sheard_accomplishments_2001,
 879         address = {Berlin, Heidelberg},
 880         title = {Accomplishments and {Research} {Challenges} in {Meta}-programming},
 881         isbn = {978-3-540-44806-8},
 882         abstract = {In the last ten years the study of meta-programming systems, as formal systems worthy of study in their own right, has vastly accelerated. In that time a lot has been accomplished, yet much remains to be done. In this invited talk I wish to review recent accomplishments and future research challenges in hopes that this will spur interest in meta-programming in general and lead to new and better meta-programming systems.},
 883         booktitle = {Semantics, {Applications}, and {Implementation} of {Program} {Generation}},
 884         publisher = {Springer Berlin Heidelberg},
 885         author = {Sheard, Tim},
 886         editor = {Taha, Walid},
 887         year = {2001},
 888         pages = {2--44},
 889         file = {Sheard - 2001 - Accomplishments and Research Challenges in Meta-pr.pdf:/home/mrl/.local/share/zotero/storage/M7NT6USA/Sheard - 2001 - Accomplishments and Research Challenges in Meta-pr.pdf:application/pdf},
 890 }
 891
 892 @inproceedings{kohlbecker_hygienic_1986,
 893         address = {New York, NY, USA},
 894         series = {{LFP} '86},
 895         title = {Hygienic {Macro} {Expansion}},
 896         isbn = {0-89791-200-4},
 897         url = {https://doi.org/10.1145/319838.319859},
 898         doi = {10.1145/319838.319859},
 899         booktitle = {Proceedings of the 1986 {ACM} {Conference} on {LISP} and {Functional} {Programming}},
 900         publisher = {Association for Computing Machinery},
 901         author = {Kohlbecker, Eugene and Friedman, Daniel P. and Felleisen, Matthias and Duba, Bruce},
 902         year = {1986},
 903         note = {event-place: Cambridge, Massachusetts, USA},
 904         pages = {151--161},
 905         file = {Kohlbecker et al. - 1986 - Hygienic Macro Expansion.pdf:/home/mrl/.local/share/zotero/storage/MFH642JU/Kohlbecker et al. - 1986 - Hygienic Macro Expansion.pdf:application/pdf},
 906 }
 907
 908 @inproceedings{lammel_scrap_2003,
 909         address = {New York, NY, USA},
 910         series = {{TLDI} '03},
 911         title = {Scrap {Your} {Boilerplate}: {A} {Practical} {Design} {Pattern} for {Generic} {Programming}},
 912         isbn = {1-58113-649-8},
 913         url = {https://doi.org/10.1145/604174.604179},
 914         doi = {10.1145/604174.604179},
 915         abstract = {We describe a design pattern for writing programs that traverse data structures built from rich mutually-recursive data types. Such programs often have a great deal of "boilerplate" code that simply walks the structure, hiding a small amount of "real" code that constitutes the reason for the traversal.Our technique allows most of this boilerplate to be written once and for all, or even generated mechanically, leaving the programmer free to concentrate on the important part of the algorithm. These generic programs are much more adaptive when faced with data structure evolution because they contain many fewer lines of type-specific code.Our approach is simple to understand, reasonably efficient, and it handles all the data types found in conventional functional programming languages. It makes essential use of rank-2 polymorphism, an extension found in some implementations of Haskell. Further it relies on a simple type-safe cast operator.},
 916         booktitle = {Proceedings of the 2003 {ACM} {SIGPLAN} {International} {Workshop} on {Types} in {Languages} {Design} and {Implementation}},
 917         publisher = {Association for Computing Machinery},
 918         author = {Lämmel, Ralf and Jones, Simon Peyton},
 919         year = {2003},
 920         note = {event-place: New Orleans, Louisiana, USA},
 921         keywords = {generic programming, rank-2 types, traversal, type cast},
 922         pages = {26--37},
 923         file = {Lämmel and Jones - 2003 - Scrap Your Boilerplate A Practical Design Pattern.pdf:/home/mrl/.local/share/zotero/storage/P2PJYYY3/Lämmel and Jones - 2003 - Scrap Your Boilerplate A Practical Design Pattern.pdf:application/pdf},
 924 }
 925
 926 @inproceedings{bawden_quasiquotation_1999,
 927         address = {Aarhus, Denmark},
 928         series = {{BRICS} {Notes} {Series}},
 929         title = {Quasiquotation in {Lisp}},
 930         volume = {NS-99-1},
 931         doi = {10.1.1.22.1290},
 932         booktitle = {O. {Danvy}, {Ed}., {University} of {Aarhus}, {Dept}. of {Computer} {Science}},
 933         publisher = {BRICS},
 934         author = {Bawden, Alan},
 935         year = {1999},
 936         pages = {88--99},
 937         file = {Bawden - 1999 - Quasiquotation in Lisp.pdf:/home/mrl/.local/share/zotero/storage/CIFANZAW/Bawden - 1999 - Quasiquotation in Lisp.pdf:application/pdf},
 938 }
 939
 940 @inproceedings{clifton-everest_embedding_2014,
 941         address = {Cham},
 942         title = {Embedding {Foreign} {Code}},
 943         isbn = {978-3-319-04132-2},
 944         abstract = {Special purpose embedded languages facilitate generating high-performance code from purely functional high-level code; for example, we want to program highly parallel GPUs without the usual high barrier to entry and the time-consuming development process. We previously demonstrated the feasibility of a skeleton-based, generative approach to compiling such embedded languages.},
 945         booktitle = {Practical {Aspects} of {Declarative} {Languages}},
 946         publisher = {Springer International Publishing},
 947         author = {Clifton-Everest, Robert and McDonell, Trevor L. and Chakravarty, Manuel M. T. and Keller, Gabriele},
 948         editor = {Flatt, Matthew and Guo, Hai-Feng},
 949         year = {2014},
 950         pages = {136--151},
 951         file = {Clifton-Everest et al. - 2014 - Embedding Foreign Code.pdf:/home/mrl/.local/share/zotero/storage/JTJGK5BX/Clifton-Everest et al. - 2014 - Embedding Foreign Code.pdf:application/pdf},
 952 }
 953
 954 @inproceedings{shioda_libdsl_2014,
 955         address = {New York, NY, USA},
 956         series = {{GPCE} 2014},
 957         title = {{LibDSL}: {A} {Library} for {Developing} {Embedded} {Domain} {Specific} {Languages} in d via {Template} {Metaprogramming}},
 958         isbn = {978-1-4503-3161-6},
 959         url = {https://doi.org/10.1145/2658761.2658770},
 960         doi = {10.1145/2658761.2658770},
 961         abstract = {This paper presents a library called LibDSL that helps the implementer of an embedded domain specific language (EDSL) effectively develop it in D language. The LibDSL library accepts as input some kinds of “specifications” of the EDSL that the implementer is going to develop and a D program within which an EDSL source program written by the user is embedded. It produces the front-end code of an LALR parser for the EDSL program and back-end code of the execution engine. LibDSL is able to produce two kinds of execution engines, namely compiler-based and interpreter-based engines, either of which the user can properly choose depending on whether an EDSL program is known at compile time or not. We have implemented the LibDSL system by using template metaprogramming and other advanced facilities such as compile-time function execution of D language. EDSL programs developed by means of LibDSL have a nice integrativeness with the host language.},
 962         booktitle = {Proceedings of the 2014 {International} {Conference} on {Generative} {Programming}: {Concepts} and {Experiences}},
 963         publisher = {Association for Computing Machinery},
 964         author = {Shioda, Masato and Iwasaki, Hideya and Sato, Shigeyuki},
 965         year = {2014},
 966         note = {event-place: Västerås, Sweden},
 967         keywords = {Metaprogramming, D language, Embedded domain specific languages, Library},
 968         pages = {63--72},
 969         file = {Shioda et al. - 2014 - LibDSL A Library for Developing Embedded Domain S.pdf:/home/mrl/.local/share/zotero/storage/3WFYJPFR/Shioda et al. - 2014 - LibDSL A Library for Developing Embedded Domain S.pdf:application/pdf},
 970 }
 971
 972 @inproceedings{duregard_embedded_2011,
 973         address = {New York, NY, USA},
 974         series = {Haskell '11},
 975         title = {Embedded {Parser} {Generators}},
 976         isbn = {978-1-4503-0860-1},
 977         url = {https://doi.org/10.1145/2034675.2034689},
 978         doi = {10.1145/2034675.2034689},
 979         abstract = {We present a novel method of embedding context-free grammars in Haskell, and to automatically generate parsers and pretty-printers from them. We have implemented this method in a library called BNFC-meta (from the BNF Converter, which it is built on). The library builds compiler front ends using metaprogramming instead of conventional code generation. Parsers are built from labelled BNF grammars that are defined directly in Haskell modules. Our solution combines features of parser generators (static grammar checks, a highly specialised grammar DSL) and adds several features that are otherwise exclusive to combinatory libraries such as the ability to reuse, parameterise and generate grammars inside Haskell.To allow writing grammars in concrete syntax, BNFC-meta provides a quasi-quoter that can parse grammars (embedded in Haskell files) at compile time and use metaprogramming to replace them with their abstract syntax. We also generate quasi-quoters so that the languages we define with BNFC-meta can be embedded in the same way. With a minimal change to the grammar, we support adding anti-quotation to the generated quasi-quoters, which allows users of the defined language to mix concrete and abstract syntax almost seamlessly. Unlike previous methods of achieving anti-quotation, the method used by BNFC-meta is simple, efficient and avoids polluting the abstract syntax types.},
 980         booktitle = {Proceedings of the 4th {ACM} {Symposium} on {Haskell}},
 981         publisher = {Association for Computing Machinery},
 982         author = {Duregård, Jonas and Jansson, Patrik},
 983         year = {2011},
 984         note = {event-place: Tokyo, Japan},
 985         keywords = {domain specific languages, metaprogramming},
 986         pages = {107--117},
 987         file = {Duregård and Jansson - 2011 - Embedded Parser Generators.pdf:/home/mrl/.local/share/zotero/storage/H5A8TPWV/Duregård and Jansson - 2011 - Embedded Parser Generators.pdf:application/pdf},
 988 }
 989
 990 @inproceedings{eisenberg_promoting_2014,
 991         address = {New York, NY, USA},
 992         series = {Haskell '14},
 993         title = {Promoting {Functions} to {Type} {Families} in {Haskell}},
 994         isbn = {978-1-4503-3041-1},
 995         url = {https://doi.org/10.1145/2633357.2633361},
 996         doi = {10.1145/2633357.2633361},
 997         abstract = {Haskell, as implemented in the Glasgow Haskell Compiler (GHC), is enriched with many extensions that support type-level programming, such as promoted datatypes, kind polymorphism, and type families. Yet, the expressiveness of the type-level language remains limited. It is missing many features present at the term level, including case expressions, anonymous functions, partially-applied functions, and let expressions. In this paper, we present an algorithm - with a proof of correctness - to encode these term-level constructs at the type level. Our approach is automated and capable of promoting a wide array of functions to type families. We also highlight and discuss those term-level features that are not promotable. In so doing, we offer a critique on GHC's existing type system, showing what it is already capable of and where it may want improvement.We believe that delineating the mismatch between GHC's term level and its type level is a key step toward supporting dependently typed programming.},
 998         booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} {Symposium} on {Haskell}},
 999         publisher = {Association for Computing Machinery},
1000         author = {Eisenberg, Richard A. and Stolarek, Jan},
1001         year = {2014},
1002         note = {event-place: Gothenburg, Sweden},
1003         keywords = {Haskell, defunctionalization, type-level programming},
1004         pages = {95--106},
1005         file = {Eisenberg and Stolarek - 2014 - Promoting Functions to Type Families in Haskell.pdf:/home/mrl/.local/share/zotero/storage/PQXGBM6M/Eisenberg and Stolarek - 2014 - Promoting Functions to Type Families in Haskell.pdf:application/pdf},
1006 }
1007
1008 @inproceedings{viera_staged_2018,
1009         address = {New York, NY, USA},
1010         series = {{IFL} 2018},
1011         title = {A {Staged} {Embedding} of {Attribute} {Grammars} in {Haskell}},
1012         isbn = {978-1-4503-7143-8},
1013         url = {https://doi.org/10.1145/3310232.3310235},
1014         doi = {10.1145/3310232.3310235},
1015         abstract = {In this paper, we present an embedding of attribute grammars in Haskell, that is both modular and type-safe, while providing the user with domain specific error messages.Our approach involves to delay part of the safety checks to runtime. When a grammar is correct, we are able to extract a function that can be run without expecting any runtime error related to the EDSL.},
1016         booktitle = {Proceedings of the 30th {Symposium} on {Implementation} and {Application} of {Functional} {Languages}},
1017         publisher = {Association for Computing Machinery},
1018         author = {Viera, Marcos and Balestrieri, Florent and Pardo, Alberto},
1019         year = {2018},
1020         note = {event-place: Lowell, MA, USA},
1021         keywords = {Haskell, EDSL, Attribute Grammars, Dynamics, Staging},
1022         pages = {95--106},
1023         file = {Viera et al. - 2018 - A Staged Embedding of Attribute Grammars in Haskel.pdf:/home/mrl/.local/share/zotero/storage/53D4HT9C/Viera et al. - 2018 - A Staged Embedding of Attribute Grammars in Haskel.pdf:application/pdf},
1024 }
1025
1026 @incollection{kiselyov_typed_2012,
1027         address = {Berlin, Heidelberg},
1028         title = {Typed {Tagless} {Final} {Interpreters}},
1029         isbn = {978-3-642-32202-0},
1030         url = {https://doi.org/10.1007/978-3-642-32202-0_3},
1031         abstract = {The so-called `typed tagless final' approach of [6] has collected and polished a number of techniques for representing typed higher-order languages in a typed metalanguage, along with type-preserving interpretation, compilation and partial evaluation. The approach is an alternative to the traditional, or `initial' encoding of an object language as a (generalized) algebraic data type. Both approaches permit multiple interpretations of an expression, to evaluate it, pretty-print, etc. The final encoding represents all and only typed object terms without resorting to generalized algebraic data types, dependent or other fancy types. The final encoding lets us add new language forms and interpretations without breaking the existing terms and interpreters.},
1032         booktitle = {Generic and {Indexed} {Programming}: {International} {Spring} {School}, {SSGIP} 2010, {Oxford}, {UK}, {March} 22-26, 2010, {Revised} {Lectures}},
1033         publisher = {Springer Berlin Heidelberg},
1034         author = {Kiselyov, Oleg},
1035         editor = {Gibbons, Jeremy},
1036         year = {2012},
1037         doi = {10.1007/978-3-642-32202-0_3},
1038         pages = {130--174},
1039         file = {Kiselyov - 2012 - Typed Tagless Final Interpreters.pdf:/home/mrl/.local/share/zotero/storage/9NBYZLRP/Kiselyov - 2012 - Typed Tagless Final Interpreters.pdf:application/pdf},
1040 }
1041
1042 @article{laufer_type_1996,
1043         title = {Type classes with existential types},
1044         volume = {6},
1045         doi = {10.1017/S0956796800001817},
1046         number = {3},
1047         journal = {Journal of Functional Programming},
1048         author = {Läufer, Konstantin},
1049         year = {1996},
1050         note = {Publisher: Cambridge University Press},
1051         pages = {485--518},
1052         file = {Läufer - 1996 - Type classes with existential types.pdf:/home/mrl/.local/share/zotero/storage/FG73PZJE/Läufer - 1996 - Type classes with existential types.pdf:application/pdf},
1053 }
1054
1055 @incollection{hinze_fun_2003,
1056         address = {Palgrave},
1057         series = {Cornerstones of {Computing}},
1058         title = {Fun {With} {Phantom} {Types}},
1059         isbn = {978-0-333-99285-2},
1060         booktitle = {The {Fun} of {Programming}},
1061         publisher = {Bloomsbury Publishing},
1062         author = {Hinze, Ralf},
1063         editor = {Gibbons, Jeremy and de Moor, Oege},
1064         year = {2003},
1065         pages = {245--262},
1066 }
1067
1068 @inproceedings{boulton_experience_1992,
1069         address = {North-Holland},
1070         title = {Experience with embedding hardware description languages in {HOL}},
1071         volume = {10},
1072         isbn = {0-444-89686-4},
1073         abstract = {The semantics of hardware description languages can be represented in higher order logic. This provides a formal de nition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the HOL theorem-proving assistant. Three languages are being investigated: ELLA, Silage and VHDL. The approaches taken for these languages are compared and current progress on building semantically-based theorem-proving tools is discussed.},
1074         language = {en},
1075         booktitle = {{IFIP} {TC10}/{WG}},
1076         publisher = {Elsevier},
1077         author = {Boulton, Richard and Gordon, Andrew and Gordon, Mike and Harrison, John and Herbert, John and Tassel, John Van},
1078         editor = {Stavridou, Victoria and Melham, Thomas F. and Boute, Raymond T.},
1079         year = {1992},
1080         note = {event-place: Nijmegen, NL},
1081         pages = {129--156},
1082         file = {Boulton et al. - Experience with embedding hardware description lan.pdf:/home/mrl/.local/share/zotero/storage/USAAA6WM/Boulton et al. - Experience with embedding hardware description lan.pdf:application/pdf},
1083 }
1084
1085 @inproceedings{terei_safe_2012,
1086         address = {New York, NY, USA},
1087         series = {Haskell '12},
1088         title = {Safe {Haskell}},
1089         isbn = {978-1-4503-1574-6},
1090         url = {https://doi.org/10.1145/2364506.2364524},
1091         doi = {10.1145/2364506.2364524},
1092         abstract = {Though Haskell is predominantly type-safe, implementations contain a few loopholes through which code can bypass typing and module encapsulation. This paper presents Safe Haskell, a language extension that closes these loopholes. Safe Haskell makes it possible to confine and safely execute untrusted, possibly malicious code. By strictly enforcing types, Safe Haskell allows a variety of different policies from API sandboxing to information-flow control to be implemented easily as monads. Safe Haskell is aimed to be as unobtrusive as possible. It enforces properties that programmers tend to meet already by convention. We describe the design of Safe Haskell and an implementation (currently shipping with GHC) that infers safety for code that lies in a safe subset of the language. We use Safe Haskell to implement an online Haskell interpreter that can securely execute arbitrary untrusted code with no overhead. The use of Safe Haskell greatly simplifies this task and allows the use of a large body of existing code and tools.},
1093         booktitle = {Proceedings of the 2012 {Haskell} {Symposium}},
1094         publisher = {Association for Computing Machinery},
1095         author = {Terei, David and Marlow, Simon and Peyton Jones, Simon and Mazières, David},
1096         year = {2012},
1097         note = {event-place: Copenhagen, Denmark},
1098         keywords = {haskell, security, type safety},
1099         pages = {137--148},
1100         file = {2364506.2364524.pdf:/home/mrl/.local/share/zotero/storage/5SMB272R/2364506.2364524.pdf:application/pdf},
1101 }
1102
1103 @techreport{leijen_parsec_2001,
1104         address = {Utrecht},
1105         title = {Parsec: {Direct} {Style} {Monadic} {Parser} {Combinators} {For} {The} {Real} {World}},
1106         language = {en},
1107         number = {UU-CS-2001-27},
1108         institution = {Universiteit Utrecht},
1109         author = {Leijen, Daan and Meijer, Erik},
1110         year = {2001},
1111         pages = {22},
1112         file = {Leijen - Parsec Direct Style Monadic Parser Combinators Fo.pdf:/home/mrl/.local/share/zotero/storage/J78G3FZ2/Leijen - Parsec Direct Style Monadic Parser Combinators Fo.pdf:application/pdf},
1113 }
1114
1115 @inproceedings{gibbons_folding_2014,
1116         address = {New York, NY, USA},
1117         series = {{ICFP} '14},
1118         title = {Folding {Domain}-{Specific} {Languages}: {Deep} and {Shallow} {Embeddings} ({Functional} {Pearl})},
1119         isbn = {978-1-4503-2873-9},
1120         url = {https://doi.org/10.1145/2628136.2628138},
1121         doi = {10.1145/2628136.2628138},
1122         abstract = {A domain-specific language can be implemented by embedding within a general-purpose host language. This embedding may be deep or shallow, depending on whether terms in the language construct syntactic or semantic representations. The deep and shallow styles are closely related, and intimately connected to folds; in this paper, we explore that connection.},
1123         booktitle = {Proceedings of the 19th {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
1124         publisher = {Association for Computing Machinery},
1125         author = {Gibbons, Jeremy and Wu, Nicolas},
1126         year = {2014},
1127         note = {event-place: Gothenburg, Sweden},
1128         keywords = {domain-specific languages, deep and shallow embedding, folds},
1129         pages = {339--347},
1130         file = {Gibbons and Wu - 2014 - Folding Domain-Specific Languages Deep and Shallo.pdf:/home/mrl/.local/share/zotero/storage/6WNWSLFJ/Gibbons and Wu - 2014 - Folding Domain-Specific Languages Deep and Shallo.pdf:application/pdf},
1131 }
1132
1133 @inproceedings{oliveira_typecase_2005,
1134         address = {New York, NY, USA},
1135         series = {Haskell '05},
1136         title = {{TypeCase}: {A} {Design} {Pattern} for {Type}-{Indexed} {Functions}},
1137         isbn = {1-59593-071-X},
1138         url = {https://doi.org/10.1145/1088348.1088358},
1139         doi = {10.1145/1088348.1088358},
1140         abstract = {A type-indexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides collections of open type-indexed functions, in which the indexing family can be extended by defining a new type class instance but the collection of functions is fixed. The purpose of this paper is to present TypeCase: a design pattern that allows the definition of closed type-indexed functions, in which the index family is fixed but the collection of functions is extensible. It is inspired by Cheney and Hinze's work on lightweight approaches to generic programming. We generalise their techniques as a design pattern. Furthermore, we show that type-indexed functions with type-indexed types, and consequently generic functions with generic types, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches.},
1141         booktitle = {Proceedings of the 2005 {ACM} {SIGPLAN} {Workshop} on {Haskell}},
1142         publisher = {Association for Computing Machinery},
1143         author = {Oliveira, Bruno C. d. S. and Gibbons, Jeremy},
1144         year = {2005},
1145         note = {event-place: Tallinn, Estonia},
1146         keywords = {generic programming, type classes, type-indexed functions},
1147         pages = {98--109},
1148         file = {Oliveira and Gibbons - 2005 - TypeCase A Design Pattern for Type-Indexed Functi.pdf:/home/mrl/.local/share/zotero/storage/RBKEZKHN/Oliveira and Gibbons - 2005 - TypeCase A Design Pattern for Type-Indexed Functi.pdf:application/pdf},
1149 }
1150
1151 @inproceedings{odersky_putting_1996,
1152         address = {New York, NY, USA},
1153         series = {{POPL} '96},
1154         title = {Putting {Type} {Annotations} to {Work}},
1155         isbn = {0-89791-769-3},
1156         url = {https://doi.org/10.1145/237721.237729},
1157         doi = {10.1145/237721.237729},
1158         abstract = {We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.},
1159         booktitle = {Proceedings of the 23rd {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
1160         publisher = {Association for Computing Machinery},
1161         author = {Odersky, Martin and Läufer, Konstantin},
1162         year = {1996},
1163         note = {event-place: St. Petersburg Beach, Florida, USA},
1164         pages = {54--67},
1165         file = {Odersky and Läufer - 1996 - Putting Type Annotations to Work.pdf:/home/mrl/.local/share/zotero/storage/WC37TU5H/Odersky and Läufer - 1996 - Putting Type Annotations to Work.pdf:application/pdf},
1166 }
1167
1168 @inproceedings{najd_everything_2016,
1169         address = {New York, NY, USA},
1170         series = {{PEPM} '16},
1171         title = {Everything {Old} is {New} {Again}: {Quoted} {Domain}-{Specific} {Languages}},
1172         isbn = {978-1-4503-4097-7},
1173         url = {https://doi.org/10.1145/2847538.2847541},
1174         doi = {10.1145/2847538.2847541},
1175         abstract = {We describe a new approach to implementing Domain-Specific Languages(DSLs), called Quoted DSLs (QDSLs), that is inspired by two old ideas:quasi-quotation, from McCarthy's Lisp of 1960, and the subformula principle of normal proofs, from Gentzen's natural deduction of 1935. QDSLs reuse facilities provided for the host language, since host and quoted terms share the same syntax, type system, and normalisation rules. QDSL terms are normalised to a canonical form, inspired by the subformula principle, which guarantees that one can use higher-order types in the source while guaranteeing first-order types in the target, and enables using types to guide fusion. We test our ideas by re-implementing Feldspar, which was originally implemented as an Embedded DSL (EDSL), as a QDSL; and we compare the QDSL and EDSL variants. The two variants produce identical code.},
1176         booktitle = {Proceedings of the 2016 {ACM} {SIGPLAN} {Workshop} on {Partial} {Evaluation} and {Program} {Manipulation}},
1177         publisher = {Association for Computing Machinery},
1178         author = {Najd, Shayan and Lindley, Sam and Svenningsson, Josef and Wadler, Philip},
1179         year = {2016},
1180         note = {event-place: St. Petersburg, FL, USA},
1181         keywords = {EDSL, domain-specific language, DSL, embedded language, normalisation, QDSL, quotation, subformula principle},
1182         pages = {25--36},
1183         file = {Najd et al. - 2016 - Everything Old is New Again Quoted Domain-Specifi.pdf:/home/mrl/.local/share/zotero/storage/NZJW5ZVF/Najd et al. - 2016 - Everything Old is New Again Quoted Domain-Specifi.pdf:application/pdf},
1184 }
1185
1186 @article{carette_finally_2009,
1187         title = {Finally tagless, partially evaluated: {Tagless} staged interpreters for simpler typed languages},
1188         volume = {19},
1189         doi = {10.1017/S0956796809007205},
1190         number = {5},
1191         journal = {Journal of Functional Programming},
1192         author = {Carette, Jacques and Kiselyov, Oleg and Shan, Chung-Chieh},
1193         year = {2009},
1194         note = {Publisher: Cambridge University Press},
1195         pages = {509--543},
1196         file = {CARETTE et al. - 2009 - Finally tagless, partially evaluated Tagless stag.pdf:/home/mrl/.local/share/zotero/storage/T8C8VMHP/CARETTE et al. - 2009 - Finally tagless, partially evaluated Tagless stag.pdf:application/pdf},
1197 }
1198
1199 @inproceedings{leijen_domain_2000,
1200         address = {New York, NY, USA},
1201         series = {{DSL} '99},
1202         title = {Domain {Specific} {Embedded} {Compilers}},
1203         isbn = {1-58113-255-7},
1204         url = {https://doi.org/10.1145/331960.331977},
1205         doi = {10.1145/331960.331977},
1206         abstract = {Domain-specific embedded languages (DSELs) expressed in higher-order, typed (HOT) languages provide a composable framework for domain-specific abstractions. Such a framework is of greater utility than a collection of stand-alone domain-specific languages. Usually, embedded domain specific languages are build on top of a set of domain specific primitive functions that are ultimately implemented using some form of foreign function call. We sketch a general design pattern/or embedding client-server style services into Haskell using a domain specific embedded compiler for the server's source language. In particular we apply this idea to implement Haskell/DB, a domain specific embdedded compiler that dynamically generates of SQL queries from monad comprehensions, which are then executed on an arbitrary ODBC database server.},
1207         booktitle = {Proceedings of the 2nd {Conference} on {Domain}-{Specific} {Languages}},
1208         publisher = {Association for Computing Machinery},
1209         author = {Leijen, Daan and Meijer, Erik},
1210         year = {2000},
1211         note = {event-place: Austin, Texas, USA},
1212         pages = {109--122},
1213         file = {Leijen and Meijer - 2000 - Domain Specific Embedded Compilers.pdf:/home/mrl/.local/share/zotero/storage/YHPF2VZ6/Leijen and Meijer - 2000 - Domain Specific Embedded Compilers.pdf:application/pdf},
1214 }
1215
1216 @incollection{koopman_simulation_2018,
1217         address = {Cham},
1218         title = {Simulation of a {Task}-{Based} {Embedded} {Domain} {Specific} {Language} for the {Internet} of {Things}},
1219         language = {en},
1220         booktitle = {Central {European} {Functional} {Programming} {School}: 7th {Summer} {School}, {CEFP} 2018, {Košice}, {Slovakia}, {January} 22–26, 2018, {Revised} {Selected} {Papers}},
1221         publisher = {Springer International Publishing},
1222         author = {Koopman, Pieter and Lubbers, Mart and Plasmeijer, Rinus},
1223         year = {2018},
1224         pages = {51},
1225 }
1226
1227 @techreport{plasmeijer_clean_2021,
1228         address = {Nijmegen},
1229         title = {Clean {Language} {Report} version 3.1},
1230         urldate = {2021-12-22},
1231         institution = {Institute for Computing and Information Sciences},
1232         author = {Plasmeijer, Rinus and van Eekelen, Marko and van Groningen, John},
1233         month = dec,
1234         year = {2021},
1235         pages = {127},
1236         file = {CleanLanguageReport.pdf:/home/mrl/.local/share/zotero/storage/I2SDRIH6/CleanLanguageReport.pdf:application/pdf},
1237 }
1238
1239 @inproceedings{nocker_concurrent_1991,
1240         address = {Berlin, Heidelberg},
1241         title = {Concurrent clean},
1242         isbn = {978-3-540-47472-2},
1243         abstract = {Concurrent Clean is an experimental, lazy, higher-order parallel functional programming language based on term graph rewriting. An important difference with other languages is that in Clean graphs are manipulated and not terms. This can be used by the programmer to control communication and sharing of computation. Cyclic structures can be defined. Concurrent Clean furthermore allows to control the (parallel) order of evaluation to make efficient evaluation possible. With help of sequential annotations the default lazy evaluation can be locally changed into eager evaluation. The language enables the definition of partially strict data structures which make a whole new class of algorithms feasible in a functional language. A powerful and fast strictness analyser is incorporated in the system. The quality of the code generated by the Clean compiler has been greatly improved such that it is one of the best code generators for a lazy functional language. Two very powerful parallel annotations enable the programmer to define concurrent functional programs with arbitrary process topologies. Concurrent Clean is set up in such a way that the efficiency achieved for the sequential case can largely be maintained for a parallel implementation on loosely coupled parallel machine architectures.},
1244         booktitle = {{PARLE} '91 {Parallel} {Architectures} and {Languages} {Europe}},
1245         publisher = {Springer Berlin Heidelberg},
1246         author = {Nöcker, E. G. J. M. H. and Smetsers, J. E. W. and van Eekelen, M. C. J. D. and Plasmeijer, M. J.},
1247         editor = {Aarts, Emile H. L. and van Leeuwen, Jan and Rem, Martin},
1248         year = {1991},
1249         pages = {202--219},
1250         file = {Nöcker et al. - 1991 - Concurrent clean.pdf:/home/mrl/.local/share/zotero/storage/XHTNR7BR/Nöcker et al. - 1991 - Concurrent clean.pdf:application/pdf},
1251 }
1252
1253 @incollection{mernik_extensible_2013,
1254         address = {Hershey, PA, USA},
1255         title = {Extensible {Languages}: {Blurring} the {Distinction} between {DSL} and {GPL}},
1256         isbn = {978-1-4666-2092-6},
1257         url = {https://services.igi-global.com/resolvedoi/resolve.aspx?doi=10.4018/978-1-4666-2092-6.ch001},
1258         abstract = {Out of a concern for focus and concision, domain-specific languages (DSLs) are usually very different from general purpose programming languages (GPLs), both at the syntactic and the semantic levels. One approach to DSL implementation is to write a full language infrastructure, including parser, interpreter, or even compiler. Another approach however, is to ground the DSL into an extensible GPL, giving you control over its own syntax and semantics. The DSL may then be designed merely as an extension to the original GPL, and its implementation may boil down to expressing only the differences with it. The task of DSL implementation is hence considerably eased. The purpose of this chapter is to provide a tour of the features that make a GPL extensible, and to demonstrate how, in this context, the distinction between DSL and GPL can blur, sometimes to the point of complete disappearance.},
1259         booktitle = {Formal and {Practical} {Aspects} of {Domain}-{Specific} {Languages}: {Recent} {Developments}},
1260         publisher = {IGI Global},
1261         author = {Verna, Didier},
1262         editor = {Mernik, Marjan},
1263         year = {2013},
1264         doi = {10.4018/978-1-4666-2092-6.ch001},
1265         pages = {1--31},
1266 }
1267
1268 @inproceedings{hudak_modular_1998,
1269         title = {Modular domain specific languages and tools},
1270         doi = {10.1109/ICSR.1998.685738},
1271         booktitle = {Proceedings. {Fifth} {International} {Conference} on {Software} {Reuse} ({Cat}. {No}.{98TB100203})},
1272         author = {Hudak, P.},
1273         year = {1998},
1274         pages = {134--142},
1275         file = {Hudak - 1998 - Modular domain specific languages and tools.pdf:/home/mrl/.local/share/zotero/storage/JX7KZ2ST/Hudak - 1998 - Modular domain specific languages and tools.pdf:application/pdf},
1276 }
1277
1278 @book{fowler_domain_2010,
1279         edition = {1st},
1280         title = {Domain {Specific} {Languages}},
1281         isbn = {0-321-71294-3},
1282         abstract = {Designed as a wide-ranging guide to Domain Specific Languages (DSLs) and how to approach building them, this book covers a variety of different techniques available for DSLs. The goal is to provide readers with enough information to make an informed choice about whether or not to use a DSL and what kinds of DSL techniques to employ. Part I is a 150-page narrative overview that gives you a broad understanding of general principles. The reference material in Parts II through VI provides the details and examples you willneed to get started using the various techniques discussed. Both internal and external DSL topics are covered, in addition to alternative computational models and code generation. Although the general principles and patterns presented can be used with whatever programming language you happen to be using, most of the examples are in Java or C\#.},
1283         publisher = {Addison-Wesley Professional},
1284         author = {Fowler, Martin},
1285         year = {2010},
1286         file = {Fowler - 2010 - Domain-specific languages.pdf:/home/mrl/.local/share/zotero/storage/YYMYXTZ5/Fowler - 2010 - Domain-specific languages.pdf:application/pdf},
1287 }
1288
1289 @misc{peter_t_lewis_speech_1985,
1290         address = {Washington, D.C.},
1291         type = {Speech},
1292         title = {Speech},
1293         url = {http://www.chetansharma.com/correcting-the-iot-history/},
1294         author = {{Peter T. Lewis}},
1295         month = sep,
1296         year = {1985},
1297         annote = {By connecting devices such as traffic signal control boxes, underground gas station tanks and home refrigerators to supervisory control systems, modems, auto-dialers and cellular phones, we can transmit status of these devices to cell sites, then pipe that data through the Internet and address it to people near and far that need that information.  I predict that not only humans, but machines and other things will interactively communicate via the Internet.  The Internet of Things, or IoT, is the integration of people, processes and technology with connectable devices and sensors to enable remote monitoring, status, manipulation and evaluation of trends of such devices.  When all these technologies and voluminous amounts of Things are interfaced together -- namely, devices/machines, supervisory controllers, cellular and the Internet, there is nothing we cannot connect to and communicate with.  What I am calling the Internet of Things will be far reaching.},
1298 }
1299
1300 @article{weiser_computer_1991,
1301         title = {The {Computer} for the 21 st {Century}},
1302         volume = {265},
1303         language = {en},
1304         number = {3},
1305         journal = {Scientific American},
1306         author = {Weiser, Mark},
1307         month = sep,
1308         year = {1991},
1309         pages = {94--105},
1310         file = {Weiser - 1991 - The Computer for the 21 st Century.pdf:/home/mrl/.local/share/zotero/storage/N5456M2M/Weiser - 1991 - The Computer for the 21 st Century.pdf:application/pdf},
1311 }
1312
1313 @misc{evans_internet_2011,
1314         title = {The {Internet} of {Things}: {How} the {Next} {Evolution} of the {Internet} {Is} {Changing} {Everything}},
1315         url = {https://www.cisco.com/c/dam/en_us/about/ac79/docs/innov/IoT_IBSG_0411FINAL.pdf},
1316         language = {en},
1317         publisher = {Cisco Internet Business Solutions Group (IBSG)},
1318         author = {Evans, Dave},
1319         month = apr,
1320         year = {2011},
1321         file = {Evans - 2011 - How the Next Evolution of the Internet Is Changing.pdf:/home/mrl/.local/share/zotero/storage/32YXCM6P/Evans - 2011 - How the Next Evolution of the Internet Is Changing.pdf:application/pdf},
1322 }
1323
1324 @inproceedings{ireland_classification_2009,
1325         address = {Cancun, Mexico},
1326         title = {A {Classification} of {Object}-{Relational} {Impedance} {Mismatch}},
1327         isbn = {978-0-7695-3550-0},
1328         doi = {10.1109/DBKDA.2009.11},
1329         booktitle = {First {International} {Conference} on {Advances} in {Databases}, {Knowledge}, and {Data} {Applications}},
1330         publisher = {IEEE},
1331         author = {Ireland, Christopher and Bowers, David and Newton, Michael and Waugh, Kevin},
1332         year = {2009},
1333         pages = {36--43},
1334 }
1335
1336 @incollection{koopman_type-safe_2019,
1337         address = {Cham},
1338         title = {Type-{Safe} {Functions} and {Tasks} in a {Shallow} {Embedded} {DSL} for {Microprocessors}},
1339         isbn = {978-3-030-28346-9},
1340         url = {https://doi.org/10.1007/978-3-030-28346-9_8},
1341         abstract = {The Internet of Things, IoT, brings us large amounts of connected computing devices that are equipped with dedicated sensors and actuators. These computing devices are typically driven by a cheap microprocessor system with a relatively slow processor and a very limited amount of memory. Due to the special input-output capabilities of IoT devices and their connections it is very attractive to execute (parts of) programs on these microcomputers.},
1342         booktitle = {Central {European} {Functional} {Programming} {School}: 6th {Summer} {School}, {CEFP} 2015, {Budapest}, {Hungary}, {July} 6–10, 2015, {Revised} {Selected} {Papers}},
1343         publisher = {Springer International Publishing},
1344         author = {Koopman, Pieter and Plasmeijer, Rinus},
1345         editor = {Zsók, Viktória and Porkoláb, Zoltán and Horváth, Zoltán},
1346         year = {2019},
1347         doi = {10.1007/978-3-030-28346-9_8},
1348         pages = {283--340},
1349         file = {Koopman and Plasmeijer - 2019 - Type-Safe Functions and Tasks in a Shallow Embedde.pdf:/home/mrl/.local/share/zotero/storage/UY2DY4EJ/Koopman and Plasmeijer - 2019 - Type-Safe Functions and Tasks in a Shallow Embedde.pdf:application/pdf},
1350 }
1351
1352 @techreport{cheney_first-class_2003,
1353         title = {First-class phantom types},
1354         url = {https://ecommons.cornell.edu/handle/1813/5614},
1355         number = {TR2003-1901},
1356         urldate = {2017-05-15},
1357         institution = {Cornell University},
1358         author = {Cheney, James and Hinze, Ralf},
1359         year = {2003},
1360         file = {Cheney and Hinze - 2003 - First-class phantom types.pdf:/home/mrl/.local/share/zotero/storage/IBKGCFG2/Cheney and Hinze - 2003 - First-class phantom types.pdf:application/pdf},
1361 }
1362
1363 @inproceedings{baars_typing_2002,
1364         address = {New York, NY, USA},
1365         series = {{ICFP} '02},
1366         title = {Typing {Dynamic} {Typing}},
1367         isbn = {1-58113-487-8},
1368         url = {https://doi.org/10.1145/581478.581494},
1369         doi = {10.1145/581478.581494},
1370         abstract = {Even when programming in a statically typed language we every now and then encounter statically untypable values; such values result from interpreting values or from communicating with the outside world. To cope with this problem most languages include some form of dynamic types. It may be that the core language has been explicitly extended with such a type, or that one is allowed to live dangerously by using functions like unsafeCoerce. We show how, by a careful use of existentially and universally quantified types, one may achievem the same effect, without extending the language with new or unsafe features. The techniques explained are universally applicable, provided the core language is expressive enough; this is the case for the common implementations of Haskell. The techniques are used in the description of a type checking compiler that, starting from an expression term, constructs a typed function representing the semantics of that expression. In this function the overhead associated with the type checking is only once being paid for; in this sense we have thus achieved static type checking.},
1371         booktitle = {Proceedings of the {Seventh} {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
1372         publisher = {Association for Computing Machinery},
1373         author = {Baars, Arthur I. and Swierstra, S. Doaitse},
1374         year = {2002},
1375         note = {event-place: Pittsburgh, PA, USA},
1376         keywords = {coercions, dynamic typing, Haskell, Leibnitz' rule, quantified types, static typing, type equality, typed interpreters},
1377         pages = {157--166},
1378         file = {Baars and Swierstra - 2002 - Typing dynamic typing.pdf:/home/mrl/.local/share/zotero/storage/QSGVSTM4/Baars and Swierstra - 2002 - Typing dynamic typing.pdf:application/pdf},
1379 }
1380
1381 @inproceedings{young_adding_2021,
1382         address = {Berlin, Heidelberg},
1383         title = {On {Adding} {Pattern} {Matching} to {Haskell}-{Based} {Deeply} {Embedded} {Domain} {Specific} {Languages}},
1384         isbn = {978-3-030-67437-3},
1385         url = {https://doi.org/10.1007/978-3-030-67438-0_2},
1386         doi = {10.1007/978-3-030-67438-0_2},
1387         abstract = {Capturing control flow is the Achilles heel of Haskell-based deeply embedded domain specific languages. Rather than use the builtin control flow mechanisms, artificial control flow combinators are used instead. However, capturing traditional control flow in a deeply embedded domain specific language would support the writing of programs in a natural style by allowing the programmer to use the constructs that are already builtin to the base language, such as pattern matching and recursion. In this paper, we expand the capabilities of Haskell-based deep embeddings with a compiler extension for reifying conditionals and pattern matching. With this new support, the subset of Haskell that we use for expressing deeply embedded domain specific languages can be cleaner, Haskell-idiomatic, and more declarative in nature.},
1388         booktitle = {Practical {Aspects} of {Declarative} {Languages}: 23rd {International} {Symposium}, {PADL} 2021, {Copenhagen}, {Denmark}, {January} 18-19, 2021, {Proceedings}},
1389         publisher = {Springer-Verlag},
1390         author = {Young, David and Grebe, Mark and Gill, Andy},
1391         year = {2021},
1392         note = {event-place: Copenhagen, Denmark},
1393         pages = {20--36},
1394 }
1395
1396 @incollection{hinze_generic_2003,
1397         address = {Berlin, Heidelberg},
1398         title = {Generic {Haskell}: {Practice} and {Theory}},
1399         isbn = {978-3-540-45191-4},
1400         url = {https://doi.org/10.1007/978-3-540-45191-4_1},
1401         abstract = {Generic Haskell is an extension of Haskell that supports the construction of generic programs. These lecture notes describe the basic constructs of Generic Haskell and highlight the underlying theory.},
1402         booktitle = {Generic {Programming}: {Advanced} {Lectures}},
1403         publisher = {Springer Berlin Heidelberg},
1404         author = {Hinze, Ralf and Jeuring, Johan},
1405         editor = {Backhouse, Roland and Gibbons, Jeremy},
1406         year = {2003},
1407         doi = {10.1007/978-3-540-45191-4_1},
1408         pages = {1--56},
1409         file = {Hinze and Jeuring - Generic Haskell practice and theory.pdf:/home/mrl/.local/share/zotero/storage/QDRNI5VB/Hinze and Jeuring - Generic Haskell practice and theory.pdf:application/pdf},
1410 }
1411
1412 @inproceedings{torrano_strictness_2005,
1413         address = {Bristol, UK},
1414         series = {Trends in {Functional} {Programming}},
1415         title = {Strictness {Analysis} and let-to-case {Transformation} using {Template} {Haskell}},
1416         volume = {6},
1417         isbn = {978-1-84150-176-5},
1418         booktitle = {Revised {Selected} {Papers} from the {Sixth} {Symposium} on {Trends} in {Functional} {Programming}, {TFP} 2005, {Tallinn}, {Estonia}, 23-24 {September} 2005},
1419         publisher = {Intellect},
1420         author = {Torrano, Carmen and Segura, Clara},
1421         editor = {Eekelen, Marko C. J. D. van},
1422         year = {2005},
1423         note = {event-place: Talinn, Estonia},
1424         pages = {429--442},
1425         file = {Torrano and Segura - Strictness Analysis and let-to-case Transformation.pdf:/home/mrl/.local/share/zotero/storage/RIYW9WFT/Torrano and Segura - Strictness Analysis and let-to-case Transformation.pdf:application/pdf},
1426 }
1427
1428 @inproceedings{polak_automatic_2006,
1429         address = {Bristol, UK},
1430         series = {Trends in {Functional} {Programming}},
1431         title = {Automatic {Graphical} {User} {Interface} {Form} {Generation} {Using} {Template} {Haskell}},
1432         volume = {7},
1433         isbn = {978-1-84150-188-8},
1434         booktitle = {Revised {Selected} {Papers} from the {Seventh} {Symposium} on {Trends} in {Functional} {Programming}, {TFP} 2006, {Nottingham}, {United} {Kingdom}, 19-21 {April} 2006},
1435         publisher = {Intellect},
1436         author = {Polak, Gracjan and Jarosz, Janusz},
1437         editor = {Nilsson, Henrik},
1438         year = {2006},
1439         note = {event-place: Nottingham, UK},
1440         pages = {1--11},
1441         file = {Polak and Jarosz - Automatic Graphical User Interface Form Generation.pdf:/home/mrl/.local/share/zotero/storage/8VK3D8JQ/Polak and Jarosz - Automatic Graphical User Interface Form Generation.pdf:application/pdf},
1442 }
1443
1444 @phdthesis{antonova_mtask_2022,
1445         address = {Nijmegen},
1446         type = {Bachelor's {Thesis}},
1447         title = {{mTask} {Semantics} and its {Comparison} to {TopHat}},
1448         language = {en},
1449         school = {Radboud University},
1450         author = {Antonova, Elina},
1451         year = {2022},
1452         file = {Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:/home/mrl/.local/share/zotero/storage/YIEQ97KK/Crooijmans - 2021 - Reducing the Power Consumption of IoT Devices in T.pdf:application/pdf},
1453 }
1454
1455 @misc{wadler_expression_1998,
1456         title = {The expression problem},
1457         url = {https://homepages.inf.ed.ac.uk/wadler/papers/expression/expression.txt},
1458         language = {en},
1459         urldate = {2021-02-24},
1460         author = {Wadler, Philip},
1461         month = nov,
1462         year = {1998},
1463         note = {e-mail message, accessed on 2021-02-24},
1464         annote = {
1465
1466 },
1467 }
1468
1469 @misc{margaret_deuter_rhapsody_2015,
1470         address = {Oxford},
1471         edition = {Ninth edition},
1472         title = {Rhapsody},
1473         journal = {Oxford Advanced Learner's Dictionary of Current English},
1474         publisher = {Oxford University Press},
1475         author = {{A S Hornby}},
1476         editor = {{Margaret Deuter} and {Jennifer Bradbery} and {Joanna Turnbull}},
1477         year = {2015},
1478 }
1479
1480 @misc{wikipedia_contributors_rhapsody_2022,
1481         title = {Rhapsody (music) — {Wikipedia}, {The} {Free} {Encyclopedia}},
1482         url = {https://en.wikipedia.org/w/index.php?title=Rhapsody_(music)\&oldid=1068385257},
1483         urldate = {2022-09-06},
1484         journal = {Wikipedia},
1485         author = {{Wikipedia contributors}},
1486         year = {2022},
1487         note = {accessed on: 2022-09-06},
1488         annote = {[Online; accessed 6-September-2022]},
1489 }
1490
1491 @incollection{backus_introduction_1990,
1492         address = {USA},
1493         title = {An {Introduction} to the {Programming} {Language} {FL}},
1494         isbn = {0-201-17236-4},
1495         booktitle = {Research {Topics} in {Functional} {Programming}},
1496         publisher = {Addison-Wesley Longman Publishing Co., Inc.},
1497         author = {Backus, John and Williams, John H. and Wimmers, Edward L.},
1498         year = {1990},
1499         pages = {219--247},
1500 }
1501
1502 @article{achten_ins_1995,
1503         title = {The ins and outs of {Clean} {I}/{O}},
1504         volume = {5},
1505         doi = {10.1017/S0956796800001258},
1506         number = {1},
1507         journal = {Journal of Functional Programming},
1508         author = {Achten, Peter and Plasmeijer, Rinus},
1509         year = {1995},
1510         note = {Publisher: Cambridge University Press},
1511         pages = {81--110},
1512 }
1513
1514 @inproceedings{peyton_jones_imperative_1993,
1515         address = {New York, NY, USA},
1516         series = {{POPL} '93},
1517         title = {Imperative {Functional} {Programming}},
1518         isbn = {0-89791-560-7},
1519         url = {https://doi.org/10.1145/158511.158524},
1520         doi = {10.1145/158511.158524},
1521         abstract = {We present a new model, based on monads, for performing input/output in a non-strict, purely functional language. It is composable, extensible, efficient, requires no extensions to the type system, and extends smoothly to incorporate mixed-language working and in-place array updates.},
1522         booktitle = {Proceedings of the 20th {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
1523         publisher = {Association for Computing Machinery},
1524         author = {Peyton Jones, Simon L. and Wadler, Philip},
1525         year = {1993},
1526         note = {event-place: Charleston, South Carolina, USA},
1527         pages = {71--84},
1528         file = {Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:/home/mrl/.local/share/zotero/storage/9DQ5V3N3/Peyton Jones and Wadler - 1993 - Imperative Functional Programming.pdf:application/pdf},
1529 }
1530
1531 @inproceedings{achten_high_1993,
1532         address = {London},
1533         title = {High {Level} {Specification} of {I}/{O} in {Functional} {Languages}},
1534         isbn = {978-1-4471-3215-8},
1535         abstract = {The interface with the outside world has always been one of the weakest points of functional languages. It is not easy to incorporate I/O without being allowed to do side-effects. Furthermore, functional languages allow redexes to be evaluated in any order while I/O generally has to be performed in a very specific order. In this paper we present a new solution for the I/O problem which we have incorporated in the language Concurrent Clean. Concurrent Clean offers a linear type system called Unique Types. It makes it possible to define functions with side-effects without violating the functional semantics. Now it is possible to change any object in the world in the way we wanted: e.g. arrays can be updated in-situ, arbitrary file manipulation is possible. We have used this powerful tool among others to create a library for window based I/O. Using an explicit environment passing scheme provides a high-level and elegant functional specification method for I/O, called Event I/O. Now the specification of I/O has become one of the strengths of functional languages: interactive programs written in Concurrent Clean are concise, easy to write and comprehend as well as efficient. The presented solution can in principle be applied for any other functional language as well provided that it actually uses graph rewriting semantics in the implementation.},
1536         booktitle = {Functional {Programming}, {Glasgow} 1992},
1537         publisher = {Springer London},
1538         author = {Achten, Peter and van Groningen, John and Plasmeijer, Rinus},
1539         editor = {Launchbury, John and Sansom, Patrick},
1540         year = {1993},
1541         pages = {1--17},
1542         file = {Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:/home/mrl/.local/share/zotero/storage/4QVH7AYC/Achten et al. - 1993 - High Level Specification of IO in Functional Lang.pdf:application/pdf},
1543 }
1544
1545 @inproceedings{pickering_staged_2020,
1546         address = {New York, NY, USA},
1547         series = {Haskell 2020},
1548         title = {Staged {Sums} of {Products}},
1549         isbn = {978-1-4503-8050-8},
1550         url = {https://doi.org/10.1145/3406088.3409021},
1551         doi = {10.1145/3406088.3409021},
1552         abstract = {Generic programming libraries have historically traded efficiency in return for convenience, and the generics-sop library is no exception. It offers a simple, uniform, representation of all datatypes precisely as a sum of products, making it easy to write generic functions. We show how to finally make generics-sop fast through the use of staging with Typed Template Haskell.},
1553         booktitle = {Proceedings of the 13th {ACM} {SIGPLAN} {International} {Symposium} on {Haskell}},
1554         publisher = {Association for Computing Machinery},
1555         author = {Pickering, Matthew and Löh, Andres and Wu, Nicolas},
1556         year = {2020},
1557         note = {event-place: Virtual Event, USA},
1558         keywords = {generic programming, staging},
1559         pages = {122--135},
1560         file = {Pickering et al. - 2020 - Staged Sums of Products.pdf:/home/mrl/.local/share/zotero/storage/Q6ZWX4YP/Pickering et al. - 2020 - Staged Sums of Products.pdf:application/pdf},
1561 }
1562
1563 @article{xie_staging_2022,
1564         title = {Staging with {Class}: {A} {Specification} for {Typed} {Template} {Haskell}},
1565         volume = {6},
1566         url = {https://doi.org/10.1145/3498723},
1567         doi = {10.1145/3498723},
1568         abstract = {Multi-stage programming using typed code quotation is an established technique for writing optimizing code generators with strong type-safety guarantees. Unfortunately, quotation in Haskell interacts poorly with type classes, making it difficult to write robust multi-stage programs. We study this unsound interaction and propose a resolution, staged type class constraints, which we formalize in a source calculus λ⇒ that elaborates into an explicit core calculus F. We show type soundness of both calculi, establishing that well-typed, well-staged source programs always elaborate to well-typed, well-staged core programs, and prove beta and eta rules for code quotations. Our design allows programmers to incorporate type classes into multi-stage programs with confidence. Although motivated by Haskell, it is also suitable as a foundation for other languages that support both overloading and quotation.},
1569         number = {POPL},
1570         journal = {Proc. ACM Program. Lang.},
1571         author = {Xie, Ningning and Pickering, Matthew and Löh, Andres and Wu, Nicolas and Yallop, Jeremy and Wang, Meng},
1572         month = jan,
1573         year = {2022},
1574         note = {Place: New York, NY, USA
1575 Publisher: Association for Computing Machinery},
1576         keywords = {Staging, Type Classes, Typed Template Haskell},
1577         file = {Xie et al. - 2022 - Staging with Class A Specification for Typed Temp.pdf:/home/mrl/.local/share/zotero/storage/QGDB5YHR/Xie et al. - 2022 - Staging with Class A Specification for Typed Temp.pdf:application/pdf},
1578 }
1579
1580 @article{rhiger_type-safe_2009,
1581         title = {Type-safe pattern combinators},
1582         volume = {19},
1583         doi = {10.1017/S0956796808007089},
1584         number = {2},
1585         journal = {Journal of Functional Programming},
1586         author = {Rhiger, Morten},
1587         year = {2009},
1588         note = {Publisher: Cambridge University Press},
1589         pages = {145--156},
1590         file = {RHIGER - 2009 - Type-safe pattern combinators.pdf:/home/mrl/.local/share/zotero/storage/D4N7PGBS/RHIGER - 2009 - Type-safe pattern combinators.pdf:application/pdf},
1591 }
1592
1593 @inproceedings{de_vries_true_2014,
1594         address = {New York, NY, USA},
1595         series = {{WGP} '14},
1596         title = {True {Sums} of {Products}},
1597         isbn = {978-1-4503-3042-8},
1598         url = {https://doi.org/10.1145/2633628.2633634},
1599         doi = {10.1145/2633628.2633634},
1600         abstract = {We introduce the sum-of-products (SOP) view for datatype-generic programming (in Haskell). While many of the libraries that are commonly in use today represent datatypes as arbitrary combinations of binary sums and products, SOP reflects the structure of datatypes more faithfully: each datatype is a single n-ary sum, where each component of the sum is a single n-ary product. This representation turns out to be expressible accurately in GHC with today's extensions. The resulting list-like structure of datatypes allows for the definition of powerful high-level traversal combinators, which in turn encourage the definition of generic functions in a compositional and concise style. A major plus of the SOP view is that it allows to separate function-specific metadata from the main structural representation and recombining this information later.},
1601         booktitle = {Proceedings of the 10th {ACM} {SIGPLAN} {Workshop} on {Generic} {Programming}},
1602         publisher = {Association for Computing Machinery},
1603         author = {de Vries, Edsko and Löh, Andres},
1604         year = {2014},
1605         note = {event-place: Gothenburg, Sweden},
1606         keywords = {lenses, datatype-generic programming, generic views, json, metadata, sums of products, universes},
1607         pages = {83--94},
1608         file = {de Vries and Löh - 2014 - True Sums of Products.pdf:/home/mrl/.local/share/zotero/storage/QHT5IPQA/de Vries and Löh - 2014 - True Sums of Products.pdf:application/pdf},
1609 }
1610
1611 @article{willis_staged_2020,
1612         title = {Staged {Selective} {Parser} {Combinators}},
1613         volume = {4},
1614         url = {https://doi.org/10.1145/3409002},
1615         doi = {10.1145/3409002},
1616         abstract = {Parser combinators are a middle ground between the fine control of hand-rolled parsers and the high-level almost grammar-like appearance of parsers created via parser generators. They also promote a cleaner, compositional design for parsers. Historically, however, they cannot match the performance of their counterparts. This paper describes how to compile parser combinators into parsers of hand-written quality. This is done by leveraging the static information present in the grammar by representing it as a tree. However, in order to exploit this information, it will be necessary to drop support for monadic computation since this generates dynamic structure. Selective functors can help recover lost functionality in the absence of monads, and the parser tree can be partially evaluated with staging. This is implemented in a library called Parsley.},
1617         number = {ICFP},
1618         journal = {Proc. ACM Program. Lang.},
1619         author = {Willis, Jamie and Wu, Nicolas and Pickering, Matthew},
1620         month = aug,
1621         year = {2020},
1622         note = {Place: New York, NY, USA
1623 Publisher: Association for Computing Machinery},
1624         keywords = {combinators, meta-programming, parsers},
1625         file = {Willis et al. - 2020 - Staged Selective Parser Combinators.pdf:/home/mrl/.local/share/zotero/storage/RCD842QK/Willis et al. - 2020 - Staged Selective Parser Combinators.pdf:application/pdf},
1626 }
1627
1628 @inproceedings{pickering_multi-stage_2019,
1629         address = {New York, NY, USA},
1630         series = {Haskell 2019},
1631         title = {Multi-{Stage} {Programs} in {Context}},
1632         isbn = {978-1-4503-6813-1},
1633         url = {https://doi.org/10.1145/3331545.3342597},
1634         doi = {10.1145/3331545.3342597},
1635         abstract = {Cross-stage persistence is an essential aspect of multi-stage programming that allows a value defined in one stage to be available in another. However, difficulty arises when implicit information held in types, type classes and implicit parameters needs to be persisted. Without a careful treatment of such implicit information—which are pervasive in Haskell—subtle yet avoidable bugs lurk beneath the surface. This paper demonstrates that in multi-stage programming care must be taken when representing quoted terms so that important implicit information is kept in context and not discarded. The approach is formalised with a type-system, and an implementation in GHC is presented that fixes problems of the previous incarnation.},
1636         booktitle = {Proceedings of the 12th {ACM} {SIGPLAN} {International} {Symposium} on {Haskell}},
1637         publisher = {Association for Computing Machinery},
1638         author = {Pickering, Matthew and Wu, Nicolas and Kiss, Csongor},
1639         year = {2019},
1640         note = {event-place: Berlin, Germany},
1641         keywords = {metaprogramming, staging, implicits},
1642         pages = {71--84},
1643         file = {Pickering et al. - 2019 - Multi-Stage Programs in Context.pdf:/home/mrl/.local/share/zotero/storage/3EW7FM44/Pickering et al. - 2019 - Multi-Stage Programs in Context.pdf:application/pdf},
1644 }
1645
1646 @article{pickering_specification_2021,
1647         title = {A {Specification} for {Typed} {Template} {Haskell}},
1648         volume = {abs/2112.03653},
1649         url = {https://arxiv.org/abs/2112.03653},
1650         doi = {10.48550/arXiv.2112.03653},
1651         journal = {CoRR},
1652         author = {Pickering, Matthew and Löh, Andres and Wu, Nicolas},
1653         year = {2021},
1654         note = {arXiv: 2112.03653},
1655         file = {Pickering et al. - 2021 - A Specification for Typed Template Haskell.pdf:/home/mrl/.local/share/zotero/storage/YBTN4DLK/Pickering et al. - 2021 - A Specification for Typed Template Haskell.pdf:application/pdf},
1656 }
1657
1658 @inproceedings{folmer_high-level_2022,
1659         address = {Cham},
1660         title = {High-{Level} {Synthesis} of {Digital} {Circuits} from {Template} {Haskell} and {SDF}-{AP}},
1661         isbn = {978-3-031-15074-6},
1662         abstract = {Functional languages as input specifications for HLS-tools allow to specify data dependencies but do not contain a notion of time nor execution order. In this paper, we propose a method to add this notion to the functional description using the dataflow model SDF-AP. SDF-AP consists of patterns that express consumption and production that we can use to enforce resource usage. We created an HLS-tool that can synthesize parallel hardware, both data and control path, based on the repetition, expressed in Higher-Order Functions, combined with specified SDF-AP patterns.},
1663         booktitle = {Embedded {Computer} {Systems}: {Architectures}, {Modeling}, and {Simulation}},
1664         publisher = {Springer International Publishing},
1665         author = {Folmer, H. H. and Groote, R. de and Bekooij, M. J. G.},
1666         editor = {Orailoglu, Alex and Reichenbach, Marc and Jung, Matthias},
1667         year = {2022},
1668         pages = {3--27},
1669         file = {Folmer et al. - 2022 - High-Level Synthesis of Digital Circuits from Temp.pdf:/home/mrl/.local/share/zotero/storage/5JSW6MAL/Folmer et al. - 2022 - High-Level Synthesis of Digital Circuits from Temp.pdf:application/pdf},
1670 }
1671
1672 @article{materzok_generating_2022,
1673         title = {Generating {Circuits} with {Generators}},
1674         volume = {6},
1675         url = {https://doi.org/10.1145/3549821},
1676         doi = {10.1145/3549821},
1677         abstract = {The most widely used languages and methods used for designing digital hardware fall into two rough categories. One of them, register transfer level (RTL), requires specifying each and every component in the designed circuit. This gives the designer full control, but burdens the designer with many trivial details. The other, the high-level synthesis (HLS) method, allows the designer to abstract the details of hardware away and focus on the problem being solved. This method however cannot be used for a class of hardware design problems because the circuit's clock is also abstracted away. We present YieldFSM, a hardware description language that uses the generator abstraction to represent clock-level timing in a digital circuit. It represents a middle ground between the RTL and HLS approaches: the abstraction level is higher than in RTL, but thanks to explicit information about clock-level timing, it can be used in applications where RTL is traditionally used. We also present the YieldFSM compiler, which uses methods developed by the functional programming community – including continuation-passsing style translation and defunctionalization – to translate YieldFSM programs to Mealy machines. It is implemented using Template Haskell and the Clash functional hardware description language. We show that this approach leads to short and conceptually simple hardware descriptions.},
1678         number = {ICFP},
1679         journal = {Proc. ACM Program. Lang.},
1680         author = {Materzok, Marek},
1681         month = aug,
1682         year = {2022},
1683         note = {Place: New York, NY, USA
1684 Publisher: Association for Computing Machinery},
1685         keywords = {circuit synthesis, generators, hardware description languages},
1686         file = {Materzok - 2022 - Generating Circuits with Generators.pdf:/home/mrl/.local/share/zotero/storage/LH4Q8J73/Materzok - 2022 - Generating Circuits with Generators.pdf:application/pdf},
1687 }
1688
1689 @article{egi_embedding_2022,
1690         title = {Embedding {Non}-linear {Pattern} {Matching} with {Backtracking} for {Non}-free {Data} {Types} into {Haskell}},
1691         volume = {40},
1692         issn = {1882-7055},
1693         url = {https://doi.org/10.1007/s00354-022-00177-z},
1694         doi = {10.1007/s00354-022-00177-z},
1695         abstract = {Pattern matching is an important language construct for data abstraction. Many pattern-match extensions have been developed for extending the range of data types to which pattern matching is applicable. Among them, the pattern-match system proposed by Egi and Nishiwaki features practical pattern matching for non-free data types by providing a user-customizable non-linear pattern-match facility with backtracking. However, they implemented their proposal only in dynamically typed programming languages, and there were no proposals that allow programmers to benefit from both static type systems and expressive pattern matching. This paper proposes a method for implementing this pattern-match facility by meta-programming in Haskell. There are two technical challenges: (i) we need to design a set of typing rules for the pattern-match facility; (ii) we need to embed these typing rules in Haskell to make types of the pattern-match expressions inferable by the Haskell type system. We propose a set of typing rules and show that several GHC extensions, such as multi-parameter type classes, datatype promotion, GADTs, existential types, and view patterns, play essential roles for embedding these typing rules into Haskell. The implementation has already been distributed as a Haskell library miniEgison via Hackage.},
1696         number = {2},
1697         journal = {New Generation Computing},
1698         author = {Egi, Satoshi and Kawata, Akira and Kori, Mayuko and Ogawa, Hiromi},
1699         month = jul,
1700         year = {2022},
1701         pages = {481--506},
1702         file = {Egi et al. - 2022 - Embedding Non-linear Pattern Matching with Backtra.pdf:/home/mrl/.local/share/zotero/storage/PXT9L9Z4/Egi et al. - 2022 - Embedding Non-linear Pattern Matching with Backtra.pdf:application/pdf},
1703 }
1704
1705 @inproceedings{blanchette_liquid_2022,
1706         address = {New York, NY, USA},
1707         series = {Haskell 2022},
1708         title = {Liquid {Proof} {Macros}},
1709         isbn = {978-1-4503-9438-3},
1710         url = {https://doi.org/10.1145/3546189.3549921},
1711         doi = {10.1145/3546189.3549921},
1712         abstract = {Liquid Haskell is a popular verifier for Haskell programs, leveraging the power of SMT solvers to ease users' burden of proof. However, this power does not come without a price: convincing Liquid Haskell that a program is correct often necessitates giving hints to the underlying solver, which can be a tedious and verbose process that sometimes requires intricate knowledge of Liquid Haskell's inner workings. In this paper, we present Liquid Proof Macros, an extensible metaprogramming technique and framework for simplifying the development of Liquid Haskell proofs. We describe how to leverage Template Haskell to generate Liquid Haskell proof terms, via a tactic-inspired DSL interface for more concise and user-friendly proofs, and we demonstrate the capabilities of this framework by automating a wide variety of proofs from an existing Liquid Haskell benchmark.},
1713         booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} {International} {Haskell} {Symposium}},
1714         publisher = {Association for Computing Machinery},
1715         author = {Blanchette, Henry and Vazou, Niki and Lampropoulos, Leonidas},
1716         year = {2022},
1717         note = {event-place: Ljubljana, Slovenia},
1718         keywords = {Liquid Haskell, Proof Macros, Tactics},
1719         pages = {27--38},
1720         file = {Blanchette et al. - 2022 - Liquid Proof Macros.pdf:/home/mrl/.local/share/zotero/storage/YXPCWQNI/Blanchette et al. - 2022 - Liquid Proof Macros.pdf:application/pdf},
1721 }
1722
1723 @phdthesis{baaij_digital_2015,
1724         address = {Netherlands},
1725         type = {{PhD} {Thesis}},
1726         title = {Digital circuit in {C}\${\textbackslash}lambda\${aSH}: functional specifications and type-directed synthesis},
1727         abstract = {Over the last three decades, the number of transistors used in microchips has increased by three orders of magnitude, from millions to billions. The productivity of the designers, however, lags behind. Managing to implement complex algorithms, while keeping non-functional properties within desired bounds, and thoroughly verifying the design against its specification, are the main difficulties in circuit design. As a motivation for our work we make a qualitative analysis of the tools available to circuit designers. Here we see that progress has been slow, and that the same techniques have been used for over 20 years. We claim that functional languages can be used to raise the abstraction level in circuit design. Especially higher-order functional languages, where functions are first-class and can be manipulated by other functions, offer a single abstraction mechanism that can capture many design patterns. This thesis explores the idea of using the functional language Haskell directly as a hardware specification language, and move beyond the limitations of embedded languages. Additionally, we can use normal functions from existing Haskell libraries to model the behaviour of our circuits. This thesis describes the inner workings of our CλaSH compiler, which translates the aforementioned circuit descriptions written in Haskell to low-level descriptions in VHDL. The challenge then becomes the reduction of the higher-level abstractions in the descriptions to a form where synthesis is feasible. This thesis describes a term rewrite system (with bound variables) to achieve this reduction. We prove that this term rewrite system always reduces a polymorphic, higher-order circuit description to a synthesisable variant. Even when descriptions use high-level abstractions, the CλaSH compiler can synthesize efficient circuits. Case studies show that circuits designed in Haskell, and synthesized with the C?aSH compiler, are on par with hand-written VHDL, in both area and gate propagation delay. This thesis thus shows the merits of using a modern functional language for circuit design. The advanced type system and higher-order functions allow us to design circuits that have the desired property of being correct-by-construction. Finally, our synthesis approach enables us to derive efficient circuits from descriptions that use high-level abstractions.},
1728         language = {Undefined},
1729         school = {University of Twente},
1730         author = {Baaij, C. P. R.},
1731         month = jan,
1732         year = {2015},
1733         doi = {10.3990/1.9789036538039},
1734         note = {ISBN: 978-90-365-3803-9},
1735         keywords = {Haskell, Digital Circuits, EC Grant Agreement nr.: FP7/248465, EC Grant Agreement nr.: FP7/610686, EWI-23939, FPGA, Functional Programming, Hardware, IR-93962, Lambda calculus, METIS-308711, Rewrite Systems},
1736         annote = {eemcs-eprint-23939 },
1737         file = {Baaij - 2015 - Digital circuit in CλaSH functional specification.pdf:/home/mrl/.local/share/zotero/storage/MYJ33ISL/Baaij - 2015 - Digital circuit in CλaSH functional specification.pdf:application/pdf},
1738 }
1739
1740 @inproceedings{mcdonell_embedded_2022,
1741         address = {New York, NY, USA},
1742         series = {Haskell 2022},
1743         title = {Embedded {Pattern} {Matching}},
1744         isbn = {978-1-4503-9438-3},
1745         url = {https://doi.org/10.1145/3546189.3549917},
1746         doi = {10.1145/3546189.3549917},
1747         abstract = {Haskell is a popular choice for hosting deeply embedded languages. A recurring challenge for these embeddings is how to seamlessly integrate user defined algebraic data types. In particular, one important, convenient, and expressive feature for creating and inspecting data—pattern matching—is not directly available on embedded terms. We present a novel technique, embedded pattern matching, which enables a natural and user friendly embedding of user defined algebraic data types into the embedded language, and allows programmers to pattern match on terms in the embedded language in much the same way they would in the host language.},
1748         booktitle = {Proceedings of the 15th {ACM} {SIGPLAN} {International} {Haskell} {Symposium}},
1749         publisher = {Association for Computing Machinery},
1750         author = {McDonell, Trevor L. and Meredith, Joshua D. and Keller, Gabriele},
1751         year = {2022},
1752         note = {event-place: Ljubljana, Slovenia},
1753         keywords = {Haskell, algebraic data types, embedded languages, pattern matching},
1754         pages = {123--136},
1755         file = {2108.13114.pdf:/home/mrl/.local/share/zotero/storage/AJAT8AXI/2108.13114.pdf:application/pdf},
1756 }
1757
1758 @phdthesis{krishnamurthi_linguistic_2001,
1759         address = {Houston, USA},
1760         type = {{PhD} {Thesis}},
1761         title = {Linguistic reuse},
1762         school = {Rice University},
1763         author = {Krishnamurthi, Shriram},
1764         year = {2001},
1765         file = {Krishnamurthi - 2001 - Linguistic reuse.PDF:/home/mrl/.local/share/zotero/storage/LSKHFPIS/Krishnamurthi - 2001 - Linguistic reuse.PDF:application/pdf},
1766 }
1767
1768 @misc{ashton_internet_1999,
1769         address = {London, UK},
1770         type = {Presentation},
1771         title = {Internet of {Things}},
1772         author = {Ashton, Kevin},
1773         year = {1999},
1774 }
1775
1776 @article{ashton_that_2009,
1777         title = {That ‘{Internet} of {Things}’ {Thing}},
1778         volume = {22},
1779         number = {7},
1780         journal = {RFID journal},
1781         author = {Ashton, Kevin},
1782         year = {2009},
1783         note = {Publisher: Hauppauge, New York},
1784         pages = {97--114},
1785         file = {Ashton - 2009 - That ‘Internet of Things’ Thing.pdf:/home/mrl/.local/share/zotero/storage/SJ33G6VR/Ashton - 2009 - That ‘Internet of Things’ Thing.pdf:application/pdf},
1786 }
1787
1788 @phdthesis{van_gemert_task_2022,
1789         address = {Nijmegen},
1790         type = {Bachelor's {Thesis}},
1791         title = {Task {Oriented} {Programming} in {LUA}},
1792         language = {en},
1793         school = {Radboud University},
1794         author = {van Gemert, Dante},
1795         year = {2022},
1796         file = {van Gemert - 2022 - Task Oriented Programming in LUA.pdf:/home/mrl/.local/share/zotero/storage/UQHAWT83/van Gemert - 2022 - Task Oriented Programming in LUA.pdf:application/pdf},
1797 }
1798
1799 @misc{lijnse_toppyt_2022,
1800         title = {Toppyt},
1801         url = {https://gitlab.com/baslijnse/toppyt},
1802         urldate = {2022-10-07},
1803         author = {Lijnse, Bas},
1804         year = {2022},
1805 }