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

[Nathaniel Yazdani]

Reminder that this is happening tomorrow!

On Wed, Nov 27, 2019 at 4:57 AM Nathaniel Yazdani
<yazdani.n at husky.neu.edu> wrote:
>
> 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.