Career: Type Theory and Operational Semantics for Programming Languages

这个职业奖支持对类型理论和操作语义在编程语言的设计和实现中的使用进行调查。 类型理论已被证明是程序设计语言设计中的一个重要组织原则。 在模块化和抽象构造的设计中使用类型理论很好地说明了这一点。 这项调查旨在巩固ML 2000编程语言的设计在类型理论的进步。 类型理论已被证明对编程语言的实现非常重要。 传统的语法定向编译方法被推广到类型定向编译，允许在编译期间利用类型信息。 复杂的类型系统，如那些来自吉拉德-雷诺兹多态的类型演算提出了新的实现策略的基础上，在链接和运行时传递类型信息。 本研究探讨使用基于类型的编译技术。 操作语义学为解决编译器正确性问题和证明程序属性提供了一个合适的框架。 类型化编程语言（如标准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.