一句话：提出依赖类型理论的通用双向类型化框架，证明其与声明系统等价并在规范化时给出可判定算法。
双向类型化将类型判断分解为推导与检查两种模式，从而控制类型信息流向并指定算法使用方式。已有工作多针对具体类型理论，缺乏通用形式化。本文为一般依赖类型理论建立通用双向类型化理论：先定义一类双向类型理论，使每个理论同时产生声明式与双向类型系统；再以与具体理论无关的方式证明二者等价；最后对规范化理论证明双向类型化可判定，从而得到通用类型算法。该算法已在原型中实现，并应用于多种理论。
Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing one to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of bidirectional type theories, each giving rise to both a declarative and a bidirectional type system. We then show, in a theory-independent fashion, that the two systems are equivalent. Finally, we establish the decidability of bidirectional typing for normalizing theories, yielding a generic typing algorithm that has been implemented in a prototype and used in practice with many theories.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Felicissimo24,
title = {Generic Bidirectional Typing for Dependent Type Theories},
author = {Thiago Felicissimo},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {1},
year = {2025},
doi = {10.1145/3715095}
}