Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing 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 type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. 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 type-checking algorithm that has been implemented in a prototype and used in practice with many theories.

翻译：双向类型标注是一种将类型判断显式分解为推理模式与检查模式的规约方法，通过在类型规则中控制类型信息的流向，实现了类型推导规则的算法化规范。虽然双向类型标注已在多种类型理论中得到深入研究并构建了相应的双向系统，但其形式化发展迄今仍局限于特定理论，通用准则仍停留在非正式层面。本研究针对一类通用依赖类型理论，给出了双向类型标注的通用描述框架。我们首先建立了类型理论（等价于逻辑框架）的通用定义，并为此定义了声明式与双向式两种类型系统。随后以理论无关的方式证明了两种系统的等价性。最后，针对规范化理论证明了双向类型标注的可判定性，由此得到一个通用类型检查算法——该算法已在原型系统中实现，并在实践中成功应用于多种类型理论。