We introduce CompLF, a logical framework allowing for the definition of computational type theories -- that is, those whose definitional equality is purely generated by rewrite rules. Its main goal is to capture the usual presentation of type theories in a faithful way. Whereas other frameworks impose a fully-annotated presentation of syntax, quite different from the ones used in practice, our proposal allows the definition of dependent type theories with their usual non-annotated syntaxes. This is achieved by the introduction of erased arguments, which correspond to premises of typing rules that are not recorded in the syntax. If on the one hand erased arguments allow us to capture the usual syntax of type theories, they can easily break decidability of type checking, as one might need to guess the erased information. We address this by proposing a bidirectional typing algorithm for CompLF. When comparing it with other algorithms in the literature, its main novelty is that it is not designed for a specific theory, but is instead generic and can be instantiated with various type theories. Moreover, it features a modular proof of completeness, in which one can fine-tune the subset of terms for which it is complete by varying the amount of annotations in the syntax. In particular, we can capture in a single framework the two main approaches for bidirectional typing, in which one reduces the amount of annotations to the minimal by restricting completeness only to normal forms, or in which one trades minimality of annotations in exchange for full completeness. Finally, CompLF is designed to be not only a theoretical tool but also a practical one: it has been implemented in a prototype that is openly available on GitHub.

翻译：我们提出CompLF，一种允许定义计算类型理论（即定义性等式完全由重写规则生成的理论）的逻辑框架。其主要目标是忠实地刻画类型理论的惯常呈现方式。与其他强制使用全注解语法呈现（与实践中的使用方式迥异）的框架不同，我们的提议允许在保留非注解语法的情况下定义依赖类型理论。这通过引入擦除参数实现，此类参数对应类型规则中未被语法记录的前提。虽然擦除参数使我们能捕捉类型理论的惯用语法，但它们可能轻易破坏类型检查的可判定性——因为需要猜测擦除的信息。为此，我们提出适用于CompLF的双向类型检查算法。与文献中其他算法相比，其主要新颖之处在于并非为特定理论设计，而是通用的，可实例化至多种类型理论。此外，该算法具有模块化的完备性证明，通过调整语法中的注解数量，可精细调控其完备性所覆盖的项集合。特别地，我们能在单一框架中捕捉双向类型检查的两种主流方法：将注解数量降至最低（仅对范式保证完备性），或为获得完全完备性而牺牲注解最小化。最后，CompLF不仅作为理论工具设计，也兼具实用性：其原型已在GitHub上开源实现。