Skip to Main content Skip to Navigation

Le langage CoLiS : syntaxe, sémantique et outillage

Abstract : This report presents the design choices of the CoLiS language, conceived within the ANR project of the same name. We present the syntax of the language, both in an abstract and in a concrete form, then we give typing rules, and finally its operational semantics. We describe a tool that implements various operations applicable on CoLiS programs, mainly an interpreter and a translator to the shell language. Operational semantics is defined formally within Why3, with which a formal proof of correction of the interpreter is performed. Finally, we present some tooling for the execution of test campaigns for non-regression and the detection of inconsistencies between direct interpretation and translation to the shell.
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download
Contributor : Claude Marché <>
Submitted on : Wednesday, October 11, 2017 - 7:01:44 AM
Last modification on : Thursday, July 8, 2021 - 3:49:47 AM
Long-term archiving on: : Friday, January 12, 2018 - 12:54:22 PM


Files produced by the author(s)


  • HAL Id : hal-01614488, version 1


Ilham Dami, Claude Marché. Le langage CoLiS : syntaxe, sémantique et outillage. [Rapport Technique] RT-0491, Inria Saclay Ile de France. 2017, pp.1-22. ⟨hal-01614488⟩



Record views


Files downloads