Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sat 19 Jan 2019 14:25 - 14:50 at Sala VI - Contributed Talks 3 & Coq Developers Chair(s): Qinxiang Cao

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.

Abstract (coqpl19-final14.pdf)350KiB
Reifying and translating a monadic fragment of Gallina (slides) (coqpl19slides.pdf)248KiB

Sat 19 Jan

14:00 - 15:30: CoqPL - Contributed Talks 3 & Coq Developers at Sala VI
Chair(s): Qinxiang CaoShanghai Jiao Tong University
CoqPL-201914:00 - 14:25
Vadim ZalivaCarnegie Mellon University, USA, Matthieu SozeauInria
File Attached
CoqPL-201914:25 - 14:50
File Attached
CoqPL-201914:50 - 15:30