[Pl-seminar] Seminar 12/3: Zoe Paraskevopoulou: "CertiCoq: Current and Future Directions"

[Nathaniel Yazdani]

NUPRL Seminar Presents

Zoe Paraskevopoulou
Princeton University

10:00AM to 11:30AM
Tuesday, December 3rd, 2019
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

CertiCoq: Current and Future Directions

Abstract

In this talk, I will give a high-level overview of CertiCoq, a verified compiler
from Coq to C, focusing on my research on CertiCoq's backend. The backend of
CertiCoq is based on a micro-pass compiler architecture: each stage in its
pipeline performs a simple task, yet they combine to generate efficient code.
The micro-pass design along with our proof framework based on logical relations
greatly facilities modular reasoning and proof reuse. Furthermore, I will show
how this logical relation framework can be extended to provide correctness
guarantees for programs compiled separately with CertiCoq, using perhaps
different sets of optimizations. Lastly, I will discuss future research
directions with CertiCoq, such as provably correct interoperation of Coq and C
using the Verified Software Toolchain.

Bio

Zoe Paraskevopoulou is a 5th year PhD student at Princeton University,
working with professor Andrew Appel. Prior to that she obtained her master's
degree from École normale supérieure Paris-Saclay and her undergraduate degree
from National Technical University of Athens. She has done several internships
at institutes such as INRIA Paris, Max Planck Institute of Software Systems,
Microsoft Research and Facebook.