<html><body><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div data-marker="__QUOTED_TEXT__"><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div>Please see updated reading list below:<br></div><div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><br><div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><div>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.<br></div></div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><br></div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;">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:</div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><br class="" style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><b class="" style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><i class="">Formal Verification of Closure Conversion</i></b><br class="" style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><br class="" style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><i class="" style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;">CertiCoq is a formally verified compiler for dependently typed functional<br class="">languages that aims to bridge the gap between certified high-level programs and<br class="">their translation to a low-level machine language. In this talk I will describe<br class="">the process of implementing and proving correct, using machine checked proofs,<br class="">the closure conversion phase of CertiCoq. The main transformation is preceded by<br class="">a lambda lifting phase, that can be seen as an unboxing optimization for closure<br class="">environments, and followed by a hoisting transformation, which flattens the<br class="">structure of function definitions. As opposed to previous closure conversion<br class="">implementations, our implementation decouples the lambda lifting phase from the<br class="">closure conversion phase, allowing us to achieve a more modular design which is<br class="">more amenable to formal verification. I will explain the implementation of the<br class="">three phases as well as the proof techniques that were used to prove their<br class="">correctness. Finally, I will focus on the challenges involved in the composition<br class="">of the correctness proofs of the three phases.<br class=""><br class=""></i><br class="" style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff;"><span style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; display: inline !important; float: none;">Reading List</span></div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><span style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; display: inline !important; float: none;"><span class="" style="color: #000000; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; font-family: 'times new roman'; background-color: #ffffff;">——————</span></span></div><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000;"><span style="color: #000000; font-family: 'Times New Roman'; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; background-color: #ffffff; display: inline !important; float: none;"><span class="" style="color: #000000; font-size: 14.16px; font-style: normal; font-variant-ligatures: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: 2; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-text-stroke-width: 0px; font-family: 'times new roman'; background-color: #ffffff;">* Closure conversion <br>** Zhong Shao and Andrew Appel, "Efficient and safe-for-space closure conversion" <br>** Amal Ahmed and Matthias Blume, "Typed Closure Conversion Preserves Observational Equivalence" <br>** Morrisett et al., ">From System F to Typed Assembly Language" <br><br>* Compiler correctness <br>** Nick Benton and Chung-Kil Hur, "Biorthogonality, Step-Indexing and Compiler Correctness" <br>** Yong Kiam Tan et al., "A New Verified Compiler Backend for CakeML" (This is the new CakeML paper appearing in ICFP 2016) <br>** Georg Neis et al., "Pilsner: A Compositionally Verified Compiler for a Higher-Order Imperative Language" <br><br>* Extending Coq with effects <br>** Aleksandar Nanevski e al., "Ynot : Reasoning with the Awkward Squad" <br><br>* Parametricity and Relational Reasoning <br>** John Reynolds, "Types, Abstraction and Parametric Polymorphism" <br>** Philip Wadler, "Theorems for free!" <br>** Andrew Appel and David McAllester, "An Indexed Model of Recursive Types for Foundational Proof-Carrying Code" <br><br>* Books <br>** The Formal Semantics of Programming Languages, Glynn Winskel <br>** Types and Programming Languages, Benjamin C. Pierce </span></span></div></div></div></div></div></div></div><br></div></div></body></html>