Career: Type Theory and Operational Semantics for Programming Languages

该职业奖支持在编程语言的设计和实现中使用类型理论和操作语义的研究。类型理论已被证明是程序设计中一个重要的组织原则。在模块化和抽象构造的设计中使用类型理论就是很好的例证。本研究旨在将类型理论的进步整合到ML2000编程语言的设计中。类型理论对于编程语言的实现已经被证明是重要的。传统的定向语法编译方法被推广为定向类型编译，从而允许在编译过程中利用类型信息。复杂的类型系统，如源自吉拉德-雷诺兹多态lambda演算的系统，提出了基于在链接和运行时传递类型信息的新实现策略。本研究调查了基于类型的编译技术的使用。操作语义为解决编译器正确性问题和证明程序属性提供了合适的框架。类型化编程语言（如Standard ML）提供了丰富的环境，可以在其中讨论高级编程技术，如数据抽象、模块化和单独编译。类型对于程序的推理是必不可少的。一般来说，只有假设过程的参数具有合适的类型，才能认为过程具有特定的输入/输出属性。操作语义学是本科编程教学的一个有用的教学工具，既是一种解释手段，也是证明程序和语言性质的基础。通过研究和教育之间的相互作用，预计将产生重要的优势。

This CAREER award supports an investigation into the use of type theory and operational semantics in the design and implementation of programming languages. Type theory has proved to be an important organizing principle in programming language design. This is well exemplified by the use of type theory in the design of modularity and abstraction constructs. This investigation seeks to consolidate advances in type theory into the design of the ML2000 programming language. Type theory has proved important for the implementation of programming languages. Conventional syntax-directed compilation methods are generalized to type-directed compilation, allowing type information to be exploited during compilation. Sophisticated type systems such as those derived from the Girard- Reynolds polymorphic lambda-calculus suggest new implementation strategies based on passing type information at link- and run- time. This research investigates the use of type-based compilation techniques. Operational semantics provides a suitable framework for addressing issues of compiler correctness and proving properties of programs. Typed programming languages such as Standard ML provide a rich setting in which to discuss high-level programming techniques such as data abstraction, modularity, and separate compilation. Types are essential for reasoning about programs. A procedure can in general be deemed to have certain input/output properties only under the assumption that its arguments have suitable types. Operational semantics is a useful pedagogical tool for teaching undergraduate programming, both as an explanatory device and as the basis for proving properties of programs and languages. Important advantages are expected through the interplay between research and education.