157 lines
14 KiB
BibTeX
157 lines
14 KiB
BibTeX
@inproceedings{arias2021,
|
|
title = {The {{W-calculus}}: {{A Synchronous Framework}} for the {{Verified Modelling}} of {{Digital Signal Processing Algorithms}}},
|
|
author = {Arias, Emilio Jesús Gallego and Jouvelot, Pierre and Ribstein, Sylvain and Desblancs, Dorian},
|
|
year = {2021},
|
|
booktitle = {Proceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design},
|
|
volume = {12},
|
|
pages = {35--46},
|
|
publisher = {Association for Computing Machinery},
|
|
location = {New York, NY, USA},
|
|
doi = {10.1145/3471872.3472970},
|
|
url = {https://hal-mines-paristech.archives-ouvertes.fr/hal-03322174},
|
|
urldate = {2021-08-30},
|
|
abstract = {We introduce the W-calculus, an extension of the call-byvalue λ-calculus with synchronous semantics, designed to be flexible enough to capture different implementation forms of Digital Signal Processing algorithms, while permitting a direct embedding into the Coq proof assistant for mechanized formal verification. In particular, we are interested in the different implementations of classical DSP algorithms such as audio filters and resonators, and their associated high-level properties such as Linear Time-invariance. We describe the syntax and denotational semantics of the W-calculus, providing a Coq implementation. As a first application of the mechanized semantics, we prove that every program expressed in a restricted syntactic subset of W is linear time-invariant, by means of a characterization of the property using logical relations. This first semantics, while convenient for mechanized reasoning, is still not useful in practice as it requires re-computation of previous steps. To improve on that, we develop an imperative version of the semantics that avoids recomputation of prior stream states. We empirically evaluate the performance of the imperative semantics using a staged interpreter written in OCaml, which, for an input program in W , produces a specialized OCaml program, which is then fed to the optimizing OCaml compiler. The approach provides a convenient path from the high-level semantical description to low-level efficient code. Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.},
|
|
keywords = {Digital Signal Processing,Formal Verification,Linear Time-invariance,Programming Language Semantics,Synchronous Programming},
|
|
file = {/Users/tomoya/Downloads/3472970-vor.pdf;/Users/tomoya/Zotero/storage/C48ATPES/full-text.pdf}
|
|
}
|
|
|
|
@inproceedings{gaster2018,
|
|
title = {{{OUTSIDE THE BLOCK SYNDICATE}}: {{TRANSLATING FAUST}}'{{S ALGEBRA OF BLOCKS TO THE ARROWS FRAMEWORK}}},
|
|
booktitle = {Proceedings of the 1st {{International Faust Conference}}},
|
|
author = {Gaster, Benedict R and Renney, Nathan and Mitchell, Tom},
|
|
year = {2018},
|
|
location = {Mainz,Germany},
|
|
abstract = {Folklore has it that Faust's algebra of blocks can be represented in Hughes' algebra of Arrows. In this paper we formalise this understanding, showing that blocks can indeed be encoded with Causal Commutative Arrows. Whilst an interesting finding in itself, we believe that this formal translation opens up new avenues of research. For instance, recent work in functional reactive programming on well typed clocks, could provide an alternative to the dependent type approach proposed for multi-rate Faust.},
|
|
file = {/Users/tomoya/Zotero/storage/6X7SPZEM/full-text.pdf}
|
|
}
|
|
|
|
@inproceedings{graf2010,
|
|
title = {Term {{Rewriting Extension}} for the {{Faust Programming Language}}},
|
|
booktitle = {International {{Linux Audio Conference}}},
|
|
author = {Gräf, Albert},
|
|
year = {2010},
|
|
url = {https://hal.archives-ouvertes.fr/hal-03162973 https://hal.archives-ouvertes.fr/hal-03162973/document},
|
|
abstract = {This paper discusses a term rewriting extension for the functional signal processing language Faust. The extension equips Faust with a hygienic macro processing facility. Faust macros can be used to define complicated, parameterized block diagrams, and perform arbitrary symbolic manipulations of block diagrams. Thus they make it easier to create elaborate signal processor specifications involving many complicated components.},
|
|
keywords = {Digital signal processing,Faust,functional programming,macro processing,term rewriting},
|
|
file = {/Users/tomoya/Zotero/storage/KXEWFSGX/full-text.pdf}
|
|
}
|
|
|
|
@inproceedings{matsuura2021a,
|
|
title = {Mimium: A Self-Extensible Programming Language for Sound and Music},
|
|
shorttitle = {Mimium},
|
|
booktitle = {Proceedings of the 9th {{ACM SIGPLAN International Workshop}} on {{Functional Art}}, {{Music}}, {{Modelling}}, and {{Design}}},
|
|
author = {Matsuura, Tomoya and Jo, Kazuhiro},
|
|
year = {2021},
|
|
month = aug,
|
|
series = {{{FARM}} 2021},
|
|
pages = {1--12},
|
|
publisher = {Association for Computing Machinery},
|
|
address = {New York, NY, USA},
|
|
doi = {10.1145/3471872.3472969},
|
|
urldate = {2024-07-09},
|
|
abstract = {We propose a programming language for music named mimium, which combines temporal-discrete control and signal processing in a single language. mimium has an intuitive imperative syntax and can use stateful functions as Unit Generator in the same way as ordinary function definitions and applications. Furthermore, the runtime performance is made equivalent to that of lower-level languages by compiling the code through the LLVM compiler infrastructure. By using the strategy of adding a minimum number of features for sound to the design and implementation of a general-purpose functional language, mimium is expected to lower the learning cost for users, simplify the implementation of compilers, and increase the self-extensibility of the language. In this paper, we present the basic language specification, semantics for simple task scheduling, the semantics for stateful functions, and the compilation process. mimium has certain specifications that have not been achieved in existing languages. Future works suggested include extending the compiler functionality to combine task scheduling with the functional paradigm and introducing multi-stage computation for parametric replication of stateful functions.},
|
|
isbn = {978-1-4503-8613-5},
|
|
file = {/Users/tomoya/Zotero/storage/TDBLJQTL/Matsuura and Jo - 2021 - mimium a self-extensible programming language for.pdf}
|
|
}
|
|
|
|
|
|
@article{norilo2015,
|
|
title = {Kronos: {{A Declarative Metaprogramming Language}} for {{Digital Signal Processing}}},
|
|
author = {Norilo, Vesa},
|
|
year = {2015},
|
|
journal = {Computer Music Journal},
|
|
volume = {39},
|
|
number = {4},
|
|
pages = {30--48},
|
|
doi = {10.1162/COMJ_a_00330},
|
|
url = {https://dl.acm.org/doi/abs/10.1162/COMJ_a_00330},
|
|
abstract = {Kronos is a signal-processing programming language based on the principles of semifunctional reactive systems. It is aimed at efficient signal processing at the elementary level, and built to scale towards higher-level tasks by utilizing the powerful programming paradigms of "metaprogramming" and reactive multirate systems. The Kronos language features expressive source code as well as a streamlined, efficient runtime. The programming model presented is adaptable for both sample-stream and event processing, offering a cleanly functional programming paradigm for a wide range of musical signal-processing problems, exemplified herein by a selection and discussion of code examples.},
|
|
file = {/Users/tomoya/Zotero/storage/THAKVEM6/m-api-574ff3be-cfe2-7867-406a-df50770bf1cb.pdf}
|
|
}
|
|
|
|
@article{Orlarey2004,
|
|
title = {Syntactical and Semantical Aspects of {{Faust}}},
|
|
author = {Orlarey, Yann and Fober, Dominique and Letz, Stephane},
|
|
year = {2004},
|
|
journal = {Soft Computing},
|
|
volume = {8},
|
|
number = {9},
|
|
pages = {623--632},
|
|
issn = {14327643},
|
|
doi = {10.1007/s00500-004-0388-1},
|
|
isbn = {0050000403},
|
|
keywords = {Compiler,Dataflow,Functional programming,Real-time,Signal processing},
|
|
file = {/Users/tomoya/Zotero/storage/YZVBLW85/Orlarey, Fober, Letz_2004_Syntactical and semantical aspects of Faust.pdf}
|
|
}
|
|
|
|
@article{ierusalimschy2005,
|
|
title = {The {{Implementation}} of {{Lua}} 5.0},
|
|
author = {Ierusalimschy, Roberto and de Figueiredo, Luiz Henrique and Celes, Waldemar},
|
|
year = {2005},
|
|
month = jul,
|
|
journal = {JUCS - Journal of Universal Computer Science},
|
|
volume = {11},
|
|
number = {7},
|
|
pages = {1159--1176},
|
|
publisher = {Journal of Universal Computer Science},
|
|
issn = {0948-6968},
|
|
doi = {10.3217/jucs-011-07-1159},
|
|
urldate = {2024-07-09},
|
|
abstract = {We discuss the main novelties of the implementation of Lua 5.0: its register-based virtual machine, the new algorithm for optimizing tables used as arrays, the implementation of closures, and the addition of coroutines.},
|
|
copyright = {2005 Roberto Ierusalimschy, Luiz Henrique de Figueiredo, Waldemar Celes},
|
|
language = {en},
|
|
file = {/Users/tomoya/Zotero/storage/GQRQSVPC/Ierusalimschy et al. - 2005 - The Implementation of Lua 5.0.pdf}
|
|
}
|
|
|
|
@book{nystrom2021,
|
|
title = {{Crafting Interpreters}},
|
|
author = {Nystrom, Robert},
|
|
year = {2021},
|
|
month = jul,
|
|
publisher = {Genever Benning},
|
|
address = {Daryaganj Delhi},
|
|
abstract = {Despite using them every day, most software engineers know little about how programming languages are designed and implemented. For many, their only experience with that corner of computer science was a terrifying "compilers" class that they suffered through in undergrad and tried to blot from their memory as soon as they had scribbled their last NFA to DFA conversion on the final exam.That fearsome reputation belies a field that is rich with useful techniques and not so difficult as some of its practitioners might have you believe. A better understanding of how programming languages are built will make you a stronger software engineer and teach you concepts and data structures you'll use the rest of your coding days. You might even have fun.This book teaches you everything you need to know to implement a full-featured, efficient scripting language. You'll learn both high-level concepts around parsing and semantics and gritty details like bytecode representation and garbage collection. Your brain will light up with new ideas, and your hands will get dirty and calloused.Starting from main(), you will build a language that features rich syntax, dynamic typing, garbage collection, lexical scope, first-class functions, closures, classes, and inheritance. All packed into a few thousand lines of clean, fast code that you thoroughly understand because you wrote each one yourself.},
|
|
isbn = {978-0-9905829-3-9}
|
|
}
|
|
@article{Taha1997,
|
|
title = {Multi-{{Stage Programming}} with {{Explicit Annotations}}},
|
|
author = {Taha, Walid and Sheard, Tim},
|
|
year = {1997},
|
|
month = dec,
|
|
journal = {SIGPLAN Notices (ACM Special Interest Group on Programming Languages)},
|
|
volume = {32},
|
|
number = {12},
|
|
pages = {203--214},
|
|
publisher = {Association for Computing Machinery (ACM)},
|
|
issn = {03621340},
|
|
doi = {10.1145/258994.259019},
|
|
urldate = {2021-05-12},
|
|
abstract = {We introduce MetaML, a statically-typed multi-stage programming language extending Nielson and Nielson's two stage notation to an arbitrary number of stages. MetaML extends previous work by introducing four distinct staging annotations which generalize those published previously [25, 12, 7, 6] We give a static semantics in which type checking is done once and for all before the first stage, and a dynamic semantics which introduces a new concept of cross-stage persistence, which requires that variables available in any stage are also available in all future stages. We illustrate that staging is a manual form of binding time analysis. We explain why, even in the presence of automatic binding time analysis, explicit annotations are useful, especially for programs with more than two stages. A thesis of this paper is that multi-stage languages are useful as programming languages in their own right, and should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. To illustrate this we provide a simple three stage example, and an extended two-stage example elaborating a number of practical issues.},
|
|
file = {/Users/tomoya/Zotero/storage/KFYY25CM/Taha, Sheard - 1997 - Multi-Stage Programming with Explicit Annotations.pdf;/Users/tomoya/Zotero/storage/X3DDM6HN/full-text.pdf}
|
|
}
|
|
|
|
@inproceedings{kiselyov2014a,
|
|
title = {The {{Design}} and {{Implementation}} of {{BER~MetaOCaml}}},
|
|
booktitle = {{Proceedings of the 12th International Symposium on Functional and Logic Programming}},
|
|
author = {Kiselyov, Oleg},
|
|
editor = {Codish, Michael and Sumii, Eijiro},
|
|
year = {2014},
|
|
pages = {86--102},
|
|
publisher = {Springer International Publishing},
|
|
address = {Cham},
|
|
doi = {10.1007/978-3-319-07151-0_6},
|
|
abstract = {MetaOCaml is a superset of OCaml extending it with the data type for program code and operations for constructing and executing such typed code values. It has been used for compiling domain-specific languages and automating tedious and error-prone specializations of high-performance computational kernels. By statically ensuring that the generated code compiles and letting us quickly run it, MetaOCaml makes writing generators less daunting and more productive.},
|
|
isbn = {978-3-319-07151-0},
|
|
language = {en}
|
|
}
|
|
@article{jouvelotDependentVectorTypes2011,
|
|
title = {Dependent Vector Types for Data Structuring in Multirate {{Faust}}},
|
|
author = {Jouvelot, Pierre and Orlarey, Yann},
|
|
year = {2011},
|
|
journal = {Computer Languages, Systems \& Structures},
|
|
volume = {37},
|
|
number = {3},
|
|
pages = {113--131},
|
|
publisher = {Elsevier}
|
|
}
|