A Classical Sequent Calculus with Dependent Types
A Classical Sequent Calculus with Dependent Types
复制标题
具有相关类型的经典序列微积分
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Étienne Miquey
中科院分区：
文献类型：
--
作者：
Étienne Miquey
依赖类型是基于咖喱 - 霍华德同构的证明助手的关键特征。依赖类型的存在，除非依赖性限制在价值中，而序列的calculi自然支持延续的式解释，否则没有这种语言的呈现方式。用控制运算符和依赖类型的逐个呼叫语言，通过延续式式翻译来证明其声音设计具有价值限制的最小语言和一个类型系统，其中包含一个明确的依赖性列表以维持类型的安全性。最终，我们通过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：
10.1145/2933575.2934511
发表时间：
2016
期刊：
--
影响因子：
--
作者：
Blot V
通讯作者：
Blot V