OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

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

Yang, Zhibin and Bodeveix, Jean-Paul and Filali, Mamoun Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL. (2019) Frontiers of Computer Science, 13 (4). 715-734. ISSN 2095-2228

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader

Official URL: https://doi.org/10.1007/s11704-017-6485-y


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.

Item Type:Article
Additional Information:https://link.springer.com/article/10.1007/s11704-017-6485-y
HAL Id:hal-02419464
Audience (journal):International peer-reviewed journal
Uncontrolled Keywords:
Institution:French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE)
Other partners > Nanjing University of Aeronautics and Astronautics – NUAA (CHINA)
Other partners > Nanjing University - NJU (CHINA)
Laboratory name:
Deposited On:02 Dec 2019 13:20

Repository Staff Only: item control page