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

https://hal-mines-paristech.archives-ouvertes.fr/hal-03322174
Contributor : Claire Medrala <>
Submitted on : Thursday, August 19, 2021 - 4:13:26 PM
Last modification on : Thursday, September 2, 2021 - 3:27:45 AM

File

A-755.pdf
Explicit agreement for this submission

Identifiers

Citation

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⟩

Share

Metrics

Record views

135

Files downloads

55