Room 206 (2nd floor, badged access)
17 janvier 2019 - 14h00
Reifying and translating a monadic fragment of Gallina
par Paolo Torrini de Verimag / PACSS
Abstract: 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.
This talk will be given at the CoqPL workshop on the 19th January
