The gentle art of levitation
The gentle art of levitation
复制标题
轻柔的悬浮艺术
DOI：
10.1145/1932681.1863547
复制
发表时间：
2010
影响因子：
--
通讯作者：
Chapman J
中科院分区：
文献类型：
--
作者：
Chapman J
我们提出了一个封闭的依赖类型理论，其归纳类型不是由生成声明的方案给出的，而是由在一个宇宙中编码的。每个归纳数据类型都是通过解释其描述而产生的--描述数据类型中的第一类值。此外，后者本身也有描述。数据类型泛型编程因此成为普通编程。我们展示了一些由此产生的通用操作，并将它们部署在数据类型描述本身的数据类型上。在现有系统中的模拟表明，这种明显的自支持设置是可以实现的，没有悖论或无限回归。
We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in auniverse. Each inductive datatype arises by interpreting itsdescription- a first-class value in a datatype of descriptions. Moreover, the latter itself has a description. Datatype-generic programming thus becomes ordinary programming. We show some of the resulting generic operations and deploy them in particular, useful ways on the datatype of datatype descriptions itself. Simulations in existing systems suggest that this apparently self-supporting setup is achievable without paradox or infinite regress.
登录
查看更多内容
依赖类型理论中的泛型程序和证明的宇宙
DOI：
10.5555/985799.985801
发表时间：
2003
期刊：
Nord. J. Comput.
影响因子：
--
作者：
Marcin Benke;P. Dybjer;Patrik Jansson
通讯作者：
Patrik Jansson
函数式泛型编程和类型理论
DOI：
--
发表时间：
2002
期刊：
影响因子：
--
作者：
U. Norell
通讯作者：
U. Norell
具有单例类型和证明无关性的类型论模块化类型检查算法
DOI：
--
发表时间：
2009
期刊：
International Conference on Typed Lambda Calculus and Applications
影响因子：
--
作者：
Andreas Abel;T. Coquand;Miguel Pagano
通讯作者：
Miguel Pagano
Arity-通用数据类型-通用编程
DOI：
--
发表时间：
2010
期刊：
Programming Languages meets Program Verification
影响因子：
--
作者：
Stephanie Weirich;Chris Casinghino
通讯作者：
Chris Casinghino
COQ 中的多型编程
DOI：
--
发表时间：
2008
期刊：
Workshop on Generic Programming
影响因子：
--
作者：
W. Verbruggen;Edsko de Vries;Arthur P. Hughes
通讯作者：
Arthur P. Hughes