[talks] Zoe Paraskevopoulou will present her general exam on Monday, October 24, 2016 at 9:30am in CS 402. (updated reading list)

[Nicki Gotsis]

Please see updated reading list below: 

Zoe Paraskevopoulou will present her general exam on Monday, October 24, 2016 at 9:30am in CS 402. The members of her committee are Andrew Appel (adviser), David Walker, and Zachary Kincaid. 

Everyone is invited to attend her talk, and those faculty wishing to remain for the oral exam following are welcome to do so. Abstract and reading list are below: 

Formal Verification of Closure Conversion 

CertiCoq is a formally verified compiler for dependently typed functional 
languages that aims to bridge the gap between certified high-level programs and 
their translation to a low-level machine language. In this talk I will describe 
the process of implementing and proving correct, using machine checked proofs, 
the closure conversion phase of CertiCoq. The main transformation is preceded by 
a lambda lifting phase, that can be seen as an unboxing optimization for closure 
environments, and followed by a hoisting transformation, which flattens the 
structure of function definitions. As opposed to previous closure conversion 
implementations, our implementation decouples the lambda lifting phase from the 
closure conversion phase, allowing us to achieve a more modular design which is 
more amenable to formal verification. I will explain the implementation of the 
three phases as well as the proof techniques that were used to prove their 
correctness. Finally, I will focus on the challenges involved in the composition 
of the correctness proofs of the three phases. 


Reading List 
—————— 
* Closure conversion 
** Zhong Shao and Andrew Appel, "Efficient and safe-for-space closure conversion" 
** Amal Ahmed and Matthias Blume, "Typed Closure Conversion Preserves Observational Equivalence" 
** Morrisett et al., "From System F to Typed Assembly Language" 

* Compiler correctness 
** Nick Benton and Chung-Kil Hur, "Biorthogonality, Step-Indexing and Compiler Correctness" 
** Yong Kiam Tan et al., "A New Verified Compiler Backend for CakeML" (This is the new CakeML paper appearing in ICFP 2016) 
** Georg Neis et al., "Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language" 

* Extending Coq with effects 
** Aleksandar Nanevski e al., "Ynot : Reasoning with the Awkward Squad" 

* Parametricity and Relational Reasoning 
** John Reynolds, "Types, Abstraction and Parametric Polymorphism" 
** Philip Wadler, "Theorems for free!" 
** Andrew Appel and David McAllester, "An Indexed Model of Recursive Types for Foundational Proof-Carrying Code" 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20161017/f5235155/attachment-0001.html>