Towards a simple and safe Objective Caml compiling framework for the synchronous language SIGNAL |
| |
Authors: | Zhibin YANG Jean-Paul BODEVEIX Mamoun FILALI |
| |
Affiliation: | 1. School of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 211106, China2. State Key Laboratory of Software Development Environment, Beijing 100191, China3. Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing 211106, China4. IRIT-CNRS, Université de Toulouse, Toulouse 31062, France |
| |
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. |
| |
Keywords: | synchronous languages SIGNAL Synchronous Clocked Guarded Actions (S-CGA) Objective Caml functional programming |
|
| 点击此处可从《Frontiers of Computer Science》浏览原始摘要信息 |
|
点击此处可从《Frontiers of Computer Science》下载全文 |
|