Acknowledging the ordeal of a fully formal development in a proof assistant such as Coq, we investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucial tradeoff between graduality and the key properties of normalization and closure of universes under dependent product that CIC enjoys. Beyond this Fire Triangle of Graduality, we explore the gradualization of CIC with three different compromises, each relaxing one edge of the Fire Triangle. We develop a parametrized presentation of gradual CIC (GCIC) that encompasses all three variations, and develop their metatheory. We first present a bidirectional elaboration of GCIC to a dependently-typed cast calculus, CastCIC, which elucidates the interrelation between typing, conversion, and the gradual guarantees. We use a syntactic model of CastCIC to inform the design of a safe, confluent reduction, and establish, when applicable, normalization. We study the static and dynamic gradual guarantees as well as the stronger notion of graduality with embedding-projection pairs formulated by New and Ahmed, using appropriate semantic model constructions. This work informs and paves the way towards the development of malleable proof assistants and dependently-typed programming languages.


翻译:承认Coq 等校对助理的全面正式发展的考验,我们调查进化建筑(CIC)的微积分的逐渐变异,以便以不精确的类型和术语更迅速的原型。我们用不切实际的理论观察,逐渐地与CIC所依赖的产品下的宇宙正常化和封闭的关键特性之间的重要权衡。除了这个渐变的火三角外,我们探索CIC的逐渐化,采用三种不同的妥协,每个妥协都放松了火三角的边缘。我们开发一种渐进式CIC(GCIC)的均衡化演示,包括所有三种变异,并发展其元理论。我们首先用一种依赖性的刻变形微积分(CastCIC)进行双向的阐述,以说明CastCIC所享受的成成正统和封闭的产物。我们使用CastCIC的合成模型来指导安全、相容的减少,并在适用时建立正常化。我们研究静态和动态的逐步保证,以此作为更牢固的渐进式模型,同时使用嵌入式和铺路的模。

0
下载
关闭预览

相关内容

《计算机信息》杂志发表高质量的论文,扩大了运筹学和计算的范围,寻求有关理论、方法、实验、系统和应用方面的原创研究论文、新颖的调查和教程论文,以及描述新的和有用的软件工具的论文。官网链接:https://pubsonline.informs.org/journal/ijoc
【硬核书】矩阵代数基础,248页pdf
专知会员服务
85+阅读 · 2021年12月9日
因果图,Causal Graphs,52页ppt
专知会员服务
247+阅读 · 2020年4月19日
强化学习最新教程,17页pdf
专知会员服务
176+阅读 · 2019年10月11日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【资源】文本风格迁移相关资源汇总
专知
13+阅读 · 2020年7月11日
分布式并行架构Ray介绍
CreateAMind
9+阅读 · 2019年8月9日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
已删除
将门创投
7+阅读 · 2019年3月28日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Arxiv
14+阅读 · 2020年12月17日
Arxiv
6+阅读 · 2017年12月7日
VIP会员
相关资讯
【资源】文本风格迁移相关资源汇总
专知
13+阅读 · 2020年7月11日
分布式并行架构Ray介绍
CreateAMind
9+阅读 · 2019年8月9日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
已删除
将门创投
7+阅读 · 2019年3月28日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
计算机视觉近一年进展综述
机器学习研究会
9+阅读 · 2017年11月25日
【学习】Hierarchical Softmax
机器学习研究会
4+阅读 · 2017年8月6日
Top
微信扫码咨询专知VIP会员