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. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.

翻译：双向类型化是一种将类型判断显式分解为推理模式和检查模式的规范，旨在控制类型规则中类型信息的流动，并算法化地指定其使用方式。双向类型化已得到富有成效的研究，并为多种类型理论开发了双向系统。然而，迄今为止，双向类型化的形式化发展仍局限于特定理论，通用准则仍停留在非正式层面。本文针对一类通用的依赖类型理论，给出了双向类型化的通用描述。首先，我们提出类型理论（即逻辑框架）的通用定义，并为其定义了声明式和双向式类型系统。随后，以与理论无关的方式证明这两个系统是等价的。进一步利用这种等价性，确立了弱规范化理论的类型可判定性，从而生成了一个通用的类型检查算法。该算法已在原型中实现，并实际应用于多种理论。