We develop an extension of the proof environment Beluga with datasort refinement types and study its impact on mechanized proofs. In particular, we introduce refinement schemas, which provide fine-grained classification for the structures of contexts and binders. Refinement schemas are helpful in concisely representing certain proofs that rely on relations between contexts. Our formulation of refinements combines the type checking and sort checking phases into one by viewing typing derivations as outputs of sorting derivations. This allows us to cleanly state and prove the conservativity of our extension.

翻译：我们开发了证明环境Beluga的一种扩展，该扩展引入了数据类型精化类型，并研究了其对机械化证明的影响。具体而言，我们提出了精化模式，它为上下文和绑定符的结构提供了细粒度的分类。精化模式有助于简洁地表示某些依赖于上下文间关系的证明。我们的精化形式化方法通过将类型派生视为排序派生的输出，将类型检查与排序检查阶段合并为一个阶段。这使我们能够清晰陈述并证明该扩展的保守性。