Personnes présentes

• Thibaut Balabonski
• Frédéric Boulanger
• Safouan Taha
• Benoit Valiron
• Burkhart Wolff

Presentators

• Burkhart Wolff

Summary:

Bu presented Clean that is a simple C11-like language together with an abstract monads-based semantics. It is implemented within Isabelle/HOL and it handles WP reasoning.

State of the art

• IMP2 developed by Peter Lammich and Simon Wimmer is an extension of the IMP language coming with the Isabelle distribution and the Concrete Semantics tutorial. IMP2 is a C-like language combined with a VCG. Even small, IMP2 has a concrete syntax where the Clean language only comes with an abstract syntax in the sense that it fully adopts a shallow embedding within Isabelle/HOL.
• Autocorres gives means to configure a translator of C code into Isabelle/HOL. Precise parameters on the targeted processor and the memory architecture must be tuned when generating such a translator. Autocorres is a complete framework but it is a heavy one.

Clean language

Clean (pronounced as: “C lean” or “Céline” [selin]) is a minimalistic imperative language with C-like control-flow operators. It comprises:

• C-like control flow with break and return.
• global variables.
• function calls (seen as Monad-executions) with side-effects, recursion and local variables.
• cartouche syntax

Clean semantics

Clean is based on a shallow embedding into State Exception Monads theory. The state-space is fully HOL-typed and uses an incremental construction based on extensible records. This incremental construction handles sequences of variable/function declarations and enables incremental verification.

Clean will be submitted to the AFP very soon.