在统一框架中编码紧致类型系统
计算机科学中的逻辑
2021-10-29 v3 编程语言
摘要
本文探讨如何通过按值推送调用(call-by-push-value, CBPV)所提供的更通用框架，将传名调用(call-by-name, CBN)与传值调用(call-by-value, CBV)的交叉类型理论统一起来。具体而言，我们为 CBN 和 CBV 提出紧致类型系统(tight type systems)，二者均可编码于唯一的 CBPV 紧致类型系统中。所有这些系统都是定量的，即它们提供关于到范式归一化序列长度以及这些范式大小的精确信息。此外，归约序列的长度按其乘法与指数性质区分，这一概念继承自线性逻辑。最后同样重要的是，可以从 CBN 和 CBV 在 CBPV 中的相应编码提取定量度量。
引用
@article{arxiv.2105.00564,
title = {Encoding Tight Typing in a Unified Framework},
author = {Delia Kesner and Andrés Viso},
journal= {arXiv preprint arXiv:2105.00564},
year = {2021}
}
备注
arXiv admin note: text overlap with arXiv:2002.04011