The $\lambda$$\Pi$-calculus modulo theory is a logical framework in which various logics and type systems can be encoded, thus helping the cross-verification and interoperability of proof systems based on those logics and type systems. In this paper, we show how to encode predicate subtyping and proof irrelevance, two important features of the PVS proof assistant. We prove that this encoding is correct and that encoded proofs can be mechanically checked by Dedukti, a type checker for the $\lambda$$\Pi$-calculus modulo theory using rewriting.


翻译:$\ lambda$\ Pi$- calculus modulo 理论是一个逻辑框架,在这个框架中,各种逻辑和类型系统可以编码,从而帮助基于这些逻辑和类型系统的验证系统的交叉验证和互操作性。在本文中,我们展示了如何编码上游亚缩和证据无关性,这是PVS 验证助理的两个重要特征。我们证明这一编码是正确的,编码证据可以由Dedukti进行机械检查,Dedukti是使用重写对 $\ lambda$\ Pi$\ Pi$- calcululs 模型理论进行字型检查的。

0
下载
关闭预览

相关内容

专知会员服务
79+阅读 · 2021年5月4日
专知会员服务
76+阅读 · 2021年3月16日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
【硬核书】群论,Group Theory,135页pdf
专知会员服务
124+阅读 · 2020年6月25日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
【论文笔记】通俗理解少样本文本分类 (Few-Shot Text Classification) (1)
深度学习自然语言处理
7+阅读 · 2020年4月8日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
学术会议 | 知识图谱顶会 ISWC 征稿:Poster/Demo
开放知识图谱
5+阅读 · 2019年4月16日
人工智能 | NIPS 2019等国际会议信息8条
Call4Papers
7+阅读 · 2019年3月21日
ACM UMAP 2018:用户建模与个性化国际会议征搞
LibRec智能推荐
4+阅读 · 2017年10月9日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
21+阅读 · 2019年8月21日
Arxiv
4+阅读 · 2018年5月14日
VIP会员
相关主题
相关VIP内容
专知会员服务
79+阅读 · 2021年5月4日
专知会员服务
76+阅读 · 2021年3月16日
【干货书】机器学习速查手册,135页pdf
专知会员服务
125+阅读 · 2020年11月20日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
【硬核书】群论,Group Theory,135页pdf
专知会员服务
124+阅读 · 2020年6月25日
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
Top
微信扫码咨询专知VIP会员