[talks] Santiago Cuellar will present his General Exam on Wednesday, January 21st, 2015 in Room 402 at 2pm.

[Nicki Gotsis]

Santiago Cuellar will present his General Exam on Wednesday, January 21st, 2015 in Room 402 at 2pm.

The members of his committee are Andrew W. Appel, David Walker, and Aarti Gupta.

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

================================================

Abstract:


The first verified separate compiler for C, Compositional CompCert, was recently introduced with an operational model supporting language-independent linking and machine-checked proofs of vertical and horizontal composition, strengthening Leroy’s original CompCert proofs. The key techniques for its verification are structured simulations: logical relations between runtime states that enforce safety invariants in the presence of compiler-managed memory regions (private) and addressable portions of the stack frames that might be leaked to foreign modules through external function calls (public). However, the invariants are too strict to allow merging of stack frame as needed, for example, in function inlining optimizations. Moreover, changing the simulations is challenging since they strike a delicate balance that satisfies relies and guarantees among the compiled modules. In this work we present a refinement of the structured simulations that admits a larger number of compiler transformations (e.g. Function inlining) while maintaining compatibility with the operational model and the semantics preservation proof of the full compiler. The relaxation of the simulation works together with a strengthening of the proof for the composition of compiler phases (transitivity). The development has been written and verified in the proof assistant Coq.


========================================================

Reading List:

Text books:

    * A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998

        * Part I Fundamentals of Compilation
        * 13. Garbage Collection
        * 15. Functional Programming Languages (?)
        * 17. Dataflow Analysis
        * 19. Static Single-Assignment Form

B. Pierce. Types and Programming Languages. 2002.

        * Part I Untyped Systems
        * Part II Simple Types
        * Part IV Recursive Types
        * Part V Polymorphism


            * 22. Type Reconstruction
            * 23. Universal Types
            * 24. Existencial Types
            * 25. An ML Implementation of system F


Papers

    * [A. W. Appel] VeriSmall: Verified Smallfoot Shape Analysis. In First International Conf. on Certified Programs and Proofs Dec. 2011
    * *[L. Beringer, G. Stewart, and A. W. Appel] Verified compilation for shared-memory C. In Esop’ 14: The 23rd European Symposium on Programming, 2014.
    * *[Leroy 2009] X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009.
    * *[James T. Perconti and Amal Ahmed] Verifying an Open Compiler Using Multi-Language Semantics. Programming Languages and Systems 2014
    * [Reynolds 2002] J.C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In LICS’02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55 - 74, 2002.
    * [Lerner 2003] S. Lerner, T. Millstein, and C. Chambers. Automatically Proving the Correctness of Compiler Optimizations. In PLDI’03: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2003.
    * [Leroy and Blazy 2008] X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Automated Reasoning, 41(1):1–31, 2008.
    * [G. Morrisett and D. Walker] From System F to Typed Assembly Language