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

[Amal Ahmed]

Starting now.

Sent from my iPhone

> On Dec 2, 2019, at 2:17 PM, Nathaniel Yazdani <yazdani.n at husky.neu.edu> wrote:
> 
> 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.
> 
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar