Zoe Paraskevopoulou will present her general exam on Monday, October 24, 2016 at 9:30am in CS 402.
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" ** Yasuhiko Minamide et al., "Typed Closure Conversion” ** 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" * Books ** The Formal Semantics of Programming Languages, Glynn Winskel ** Types and Programming Languages, Benjamin C. Pierce
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"
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" * Books ** The Formal Semantics of Programming Languages, Glynn Winskel ** Types and Programming Languages, Benjamin C. Pierce
participants (1)
-
Nicki Gotsis