Semantics of Computation

该项目对计算的语义进行研究，重点是基于语义的编译器的开发和验证。该研究的目标是扩展基于语义的编译器技术以包含更多真实编译器的工作，通过展示传统的运行时语言结构如何被形式化为由正式语言规范操纵的数据的表示，并通过展示如何通过流分析来证明编译器优化是合理的。此外，该项目还探讨了类型理论中的问题，包括它与流程分析的关系以及类型推理中的复杂性问题。

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.