Reifying and Translating a Monadic Fragment of Gallina
We present ongoing work on verified compilation of imperative functional code in Coq, relying on the CompCert C compiler and using a reflective approach. Here we focus on the reflection of a monadic fragment of Gallina, corresponding to a first-order imperative language with primitive recursion, in a deeply embedded extensible language that we call DEC2 and which can be translated to the CompCert C front-end. DEC2 has an operational interpreter based on small-step semantics, and a denotational interpreter based on its reflective translation into Gallina. In particular, here we will focus on the technique used in proving the adequacy of reflection, by constructing the two interpreters together with a proof of their extensional equality.
Sat 19 JanDisplayed time zone: Belfast change
14:00 - 15:30
|Reification of Shallow-Embedded DSLs in Coq with Automated Verification
|Reifying and Translating a Monadic Fragment of Gallina
|Session with the Coq Development Team