[talks] Olivier Savary Belanger will present his general exam Wednesday, May 11, 2016 at 10am in CS 302.

[Nicki Gotsis]

Olivier Savary Belanger will present his general exam Wednesday, May 11, 2016 at 10am in CS 302.

The members of his committee are Andrew Appel (adviser), Aarti Gupta, and Davis August.

Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so.  His abstract and reading list follow below.

Abstract:
An increasing amount of software is written and proven correct in proof assistants. For example, an optimizing compiler for C, CompCert, has been developed and fully verified in Coq, an interactive theorem prover. For interactive theorem provers to become credible programming environments, their compilation pipelines must generate production quality code. Moreover, these compilation pipelines should be proven correct, lest the guarantees achieved in the interactive theorem provers will not apply to the program being run. 

We have begun working on a verified compiler for Coq. In addition to being formally verified to preserve semantics from end-to-end, it will include some of the optimizations which are at the heart of fast functional language compilers such as SML/NJ and the OCaml compiler. As preliminary work, I have implemented a shrink-reducer performing reductions analogous to dead-code elimination and function inlining over a CPS intermediate language, and proven it correct for a subset of the language. I will report on the performance of our implementation compared to alternatives which use impure features, and discuss the next few steps towards completing the compilation pipeline.


Textbooks:
 - B. C. Pierce. Types and Programming Languages. ISBN 0262162091. The MIT Press, 2002 
      Part I (Untyped Systems)
      Part II (Simple Types)
      Part IV (Recursive Types)
      Part V (Polymorphism) Ch. 22-25
 - B. C. Pierce. Advanced Topics in Types and Programming Languages. ISBN 0262162288. The MIT Press, 2004.
       Dependent Types (Ch. 2)
 - A. W. Appel. Compiling with Continuations. ISBN 0521416957. Cambridge University Press, 1992.

Papers: 
 - O. Danvy and A. Filinski. Representing control: a study of the CPS transformation. MSCS 1992. 
 - A. W. Appel and T. Jim. Shrinking Lambda Expressions in Linear Time. JFP 1997.
 - O. Danvy and L. R. Nielsen. A first-order one-pass CPS transformation. TCS 2003
 - P. Letouzey. A New Extraction for Coq. TYPES 2002.
 - A. Kennedy. Compiling with continuations, continued. ICFP 2007.
 - R. Kumar et al. CakeML: A Verified Implementation of ML. POPL 2014