Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL

Abstract : This paper presents a simple and safe compiler, called MinSIGNAL, from a subset of the synchronous dataflow language SIGNAL to C, as well as its existing enhancements. The compiler follows a modular architecture, and can be seen as a sequence of source-to-source transformations applied to an intermediate representation which is named Synchronous Clocked Guarded Actions (S-CGA) and translation to sequential imperative code. Objective Caml (OCaml) is used for the implementation of MinSIGNAL. As a modern functional language, OCaml is adapted to symbolic computation and so, particularly suitable for compiler design and implementation of formal analysis tools. In particular, the safety of its type checking allows to skip some verification that would be mandatory with other languages. Additionally, this work is a basis for the formal verification of the compilation of SIGNAL with a theorem prover such as Coq.
Complete list of metadatas

Cited literature [49 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-02419464
Contributor : Open Archive Toulouse Archive Ouverte (oatao) <>
Submitted on : Thursday, December 19, 2019 - 2:52:35 PM
Last modification on : Monday, January 13, 2020 - 1:19:17 AM

File

yang_24993.pdf
Files produced by the author(s)

Identifiers

Citation

Zhibin Yang, Jean-Paul Bodeveix, Mamoun Filali. Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL. Frontiers of Computer Science, Springer Verlag, 2019, 13 (4), pp.715-734. ⟨10.1007/s11704-017-6485-y⟩. ⟨hal-02419464⟩

Share

Metrics

Record views

21

Files downloads

16