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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

14:00 - 15:30: Contributed Talks 3 & Coq DevelopersCoqPL at Sala VI
Chair(s): Qinxiang CaoShanghai Jiao Tong University
14:00 - 14:25
Reification of Shallow-Embedded DSLs in Coq with Automated Verification
Vadim ZalivaCarnegie Mellon University, USA, Matthieu SozeauInria
File Attached
14:25 - 14:50
Reifying and Translating a Monadic Fragment of Gallina
File Attached
14:50 - 15:30
Session with the Coq Development Team