针对一级 Shift 和 Reset 的类型导向部分求值
编程语言
2013-09-06 v4
摘要
我们展示了在 Coq 证明助手中实现的类型导向部分求值（TDPE）算法，适用于带有强和类型的按名调用和按值调用的 shift 和 reset delimited 控制算子版本。我们证明了该算法能将良类型程序转换为范式。这些范式并不总能通过目前已知的等式理论获得。该类型系统不允许对函数类型进行修改答案类型，并允许分隔符最多设置在一个原子类型上。求值的语义域在构造类型论中表示为一种依赖类型的单子结构，结合了 Kripke 模型和延续传递风格翻译。
引用
@article{arxiv.1210.2094,
title = {Type Directed Partial Evaluation for Level-1 Shift and Reset},
author = {Danko Ilik},
journal= {arXiv preprint arXiv:1210.2094},
year = {2013}
}
备注
In Proceedings COS 2013, arXiv:1309.0924