Certified Compilers and Program Analyses

Abstract

In this talk I will give an overview of my work on implementing and formally verifying compilers, program analyses and program transformations. In the first part of the talk I will present a formal reasoning framework for deriving compilers that are correct by construction. Starting from a formal semantics of the object language and a statement of the compiler correctness property, the reasoning framework allows us to derive – systematically and machine-checked – a compiler implementation that satisfies this specification. In the second part of the talk, I will give a concrete example of a certified implementation of a domain-specific language: a combinator language to formally describe financial contracts. The language is complemented with formally certified contract analyses and transformations. This functionality is used for composing, manipulating, and evolving contracts as well as supporting numerical contract analyses such as stochastic and closed-form contract valuation.

Categories: Compilers, Formal Verification, Domain-specific Languages, Type Systems