Connecting Isabelle/C with Isabelle/Clean

Level: L3, M1, M2

Contact: Burkhart Wolff

Summary. Isabelle/C is a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. Our framework provides an abstract interface for verification back-ends to be plugged-in independently. The purpose of this stage is to develop a translation from C11-AST's generated in Isabelle/C to a semantic backend called Clean, a simple execution model for an imperative target language.

Read the detailed internship proposal.