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.