Skip to Main content Skip to Navigation
Conference papers

The W-calculus: A Synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms

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.
Complete list of metadata
Contributor : Claire Medrala Connect in order to contact the contributor
Submitted on : Thursday, August 19, 2021 - 4:13:26 PM
Last modification on : Tuesday, January 11, 2022 - 11:16:07 AM
Long-term archiving on: : Saturday, November 20, 2021 - 6:02:17 PM


Explicit agreement for this submission



Emilio Jesús Gallego Arias, Pierre Jouvelot, Sylvain Ribstein, Dorian Desblancs. The W-calculus: A Synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms. FARM 2021 - 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design, Aug 2021, Virtual, South Korea. ⟨10.1145/3471872.3472970⟩. ⟨hal-03322174⟩



Les métriques sont temporairement indisponibles