Combinatorial Problems in Typed Lambda-Calculi

该奖项支持在类型化肾结石领域的研究， 特别强调组合学、复杂性和逻辑 类型推断。 具体问题涉及类型重建， 类型检查和相关方面，并由设计驱动 以及编程语言中的实现问题。 特别注意这些问题的代数特征。这样的刻画产生了新的和更一般的统一形式，特别是半统一，通常在计算机科学的其他部分（术语重写系统，数据库理论，计算语言学）的应用。 基于一些相同的技术， 该项目探讨了两个研究领域的问题， 都有重要的应用：（1）高阶匹配（自动定理证明）和（2）ML风格的扩展 多态性（polymorphism）：多态类型的编程语言。

This award supports research in the area of typed lambda-calculi, with special emphasis on the combinatorics, complexity, and logic of type inference. Specific problems concern type- reconstruction, type-checking, and related aspects, and are motivated by design and implementation issues in programming languages. Particular attention is given to algebraic characterizations of these problems. Such characterizations give rise to new and more general forms of unification, in particular semi unification, often with applications in other parts of computer science (term-rewriting systems, database theory, computational linguistics). Based on some of the same techniques, the project explores problems in two research areas, both with important applications: (1) higher-order matching \ (for automatic theorem proving) and (2) extensions of ML-style polymorphism (for polymorphically typed programming languages).