Towards a Formally Verified Proof Assistant

Towards a Formally Verified Proof Assistant
复制标题

走向正式验证的证明助手

DOI：
--
复制
发表时间：
2014
期刊：
International Conference on Interactive Theorem Proving
影响因子：
--
通讯作者：
Vincent Rahli
Vincent Rahli
中科院分区：
--
文献类型：
--
作者：
A. Anand;Vincent Rahli

文献摘要

被引文献

相似文献

本文介绍了NUPRL在Coq中的元态的格式化。 per）这种类型的系统包括依赖类型，宇宙的层次结构，归纳类型和部分类型。 W.R.T.这是通过语义的，因此将NUPRL的一致性降低了COQ的一致性。
This paper presents a formalization of Nuprl’s metatheory in Coq. It includes a nominal-style definition of the Nuprl language, its reduction rules, a coinductive computational equivalence, and a Curry-style type system where a type is defined as a Partial Equivalence Relation (PER) a la Allen. This type system includes Martin-Lof dependent types, a hierarchy of universes, inductive types and partial types. We then prove that the typehood rules of Nuprl are valid w.r.t. this PER semantics and hence reduce Nuprl’s consistency to Coq’s consistency.