The W-calculus: A Synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année :

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

(1, 2, 3, 4) , (5, 6) , (5) , (7)
1
2
3
4
5
6
7

Résumé

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.
Fichier principal
Vignette du fichier
A-755-v2.pdf (710.66 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03322174 , version 1 (19-08-2021)
hal-03322174 , version 2 (06-07-2022)

Identifiants

Citer

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-03322174v2⟩
266 Consultations
320 Téléchargements

Altmetric

Partager

Gmail Facebook Twitter LinkedIn More