Combinatorial Problems in Typed Lambda-Calculi

类型 Lambda 演算中的组合问题

• 批准号: 9417382
• 负责人: Assaf Kfoury
• 金额: $ 32.93万
• 依托单位: Trustees of Boston University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-05-15 至 1999-04-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9417382&HistoricalAwards=false
• 关键词: Combinatorial; Problems; Typed; Lambda; Calculi

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

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