一句话：给出带控制算子和依赖类型的 call-by-value 语言的相继式演算，并用 CPS 翻译证明其可靠性。
依赖类型是 Curry-Howard 对应下证明助手的核心特性。经典逻辑可通过控制算子扩展该对应，但依赖类型环境下控制算子通常行为异常，除非把依赖限制在值上；此外，依赖类型语言缺少相继式演算表示。本文从 call-by-value 的 λμ˜μ-演算出发，设计一个带 value restriction 与显式依赖列表的最小语言及类型系统，以保持类型安全；进而放松 value restriction、引入 delimited continuations，并通过 continuation-passing-style 翻译证明一致性。最后将系统与 Lepigre 的相似系统关联，提出迁移性质的方法。
Dependent types are a key feature of the proof assistants based on the Curry-Howard isomorphism. It is well known that this correspondence can be extended to classical logic by enriching the language of proofs with control operators. However, they are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. Moreover, while sequent calculi naturally support continuation-passing-style interpretations, there is no such presentation of a language with dependent types. The main achievement of this article is to give a sequent calculus presentation of a call-by-value language with a control operator and dependent types, and to justify its soundness through a continuation-passing-style translation. We start from the call-by-value version of the λμ˜μ -calculus. We design a minimal language with a value restriction and a type system that includes a list of explicit dependencies to maintain type safety. We then show how to relax the value restriction and introduce delimited continuations to directly prove the consistency by means of a continuation-passing-style translation. Finally, we relate our calculus to a similar system by Lepigre and present a methodology to transfer properties from this system to our own.
DOI 原文 ·
@article{paperbot714,
title = {A Classical Sequent Calculus with Dependent Types},
author = {Étienne Miquey},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {2},
year = {2019},
doi = {10.1145/3230625}
}