定量经典可实现性
计算机科学中的逻辑
2012-11-20 v2
摘要
定量可实现性由 Dal Lago 和 Hofmann 引入，是一种用于为基于乘法线性逻辑的逻辑定义模型的技术。其特点是将函数解释为有界时间可计算函数。它已被用于针对某些时间复杂度类，给出几个类型系统可靠性的新颖且统一的证明。我们建议在 Krivine 的经典可实现性框架下重构他们的思想。所获得的框架推广了 Dal Lago 和 Hofmann 的可实现性，并揭示了定量可实现性与 Cohen 强制法的线性变体之间的深刻联系。
引用
@article{arxiv.1201.4307,
title = {Quantitative classical realizability},
author = {Aloïs Brunel},
journal= {arXiv preprint arXiv:1201.4307},
year = {2012}
}
备注
Revised version