点击次数：

所属单位：计算机科学与技术学院/人工智能学院/软件学院

发表刊物：Front. Comput. Sci.

摘要：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. © 2018, Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature.

ISSN号：2095-2228

是否译文：否

发表时间：2019-08-01

合写作者：Bodeveix, Jean-Paul,Filali, Mamoun

通讯作者：杨志斌