Dependently-Typed Programming with Logical Equality Reflection
Dependently-Typed Programming with Logical Equality Reflection
复制标题
具有逻辑相等反射的依赖类型编程
DOI：
10.1145/3607852
复制
发表时间：
2023
影响因子：
--
通讯作者：
Weirich, Stephanie
中科院分区：
文献类型：
--
作者：
Liu, Yiyun;Weirich, Stephanie
在允许一般递归的依赖类型函数式编程语言中，必须对用作证明的程序进行评估以保持类型稳健性。因此，程序员必须在性能和安全性之间做出权衡。为了解决这个问题，我们提出了System DE，一种支持终止跟踪和等式反射的显式类型、建模核心演算。程序员可以用逻辑子语言编写关于潜在的发散程序的归纳证明，并将这些证明反映给类型检查器，同时知道这些证明将在执行之前被编译器擦除。System DE的一个关键特性是它对终止和相关跟踪的模式的使用，这不仅简化了设计，而且为将来的扩展留有余地。System DE适合在Glasgow Haskell编译器中使用，但也可以作为任何通用的依赖类型语言的基础。
In dependently-typed functional programming languages that allow general recursion, programs used as proofs must be evaluated to retain type soundness. As a result, programmers must make a trade-off between performance and safety. To address this problem, we propose System DE, an explicitly-typed, moded core calculus that supports termination tracking and equality reflection. Programmers can write inductive proofs about potentially diverging programs in a logical sublanguage and reflect those proofs to the type checker, while knowing that such proofs will be erased by the compiler before execution. A key feature of System DE is its use of modes for both termination and relevance tracking, which not only simplifies the design but also leaves it open for future extension. System DE is suitable for use in the Glasgow Haskell Compiler, but could serve as the basis for any general purpose dependently-typed language.
登录
查看更多内容
类型推断、Haskell 和依赖类型
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Adam Gundry
通讯作者：
Adam Gundry
无穷大的数学
DOI：
10.1007/3-540-52335-9_54
发表时间：
1988
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
P. Martin
通讯作者：
P. Martin
结合证明和程序
DOI：
10.4230/lipics.rta.2011.9
发表时间：
2011
期刊：
J. Log. Comput.
影响因子：
--
作者：
Stephanie Weirich
通讯作者：
Stephanie Weirich
Type:Type 的多态 Lambda 演算
DOI：
--
发表时间：
1986
期刊：
影响因子：
--
作者：
L. Cardelli
通讯作者：
L. Cardelli
模态类型理论中的内涵性、外延性和证明无关性
DOI：
10.1109/lics.2001.932499
发表时间：
2001
期刊：
Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
F. Pfenning
通讯作者：
F. Pfenning