Combinatorial Problems in Typed Lambda-Calculi

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

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).