This project conducts research in the semantics of computation, with a focus on the development and verification of semantics-based compilers. The goal of the research is to extend semantics-based compiler technology to encompass more of the workings of real compilers, by showing how conventional run-time language structures are formalized as representations of the data manipulated by formal language specifications, and by showing how compiler optimizations are justified by flow analyses. In addition, the project explores issues in type theory, including its relation to flow analysis and questions of complexity in type inference.
