合取结构上的并发可实现性
计算机科学中的逻辑
2021-12-30 v1 逻辑
摘要
本工作的重点是利用证明论与可实现性技术研究并发计算的公理化。为处理该问题，我们使用带有全局融合的 -演算作为可实现子，重新定义了 Beffara 的并发可实现性。我们定义了 É Miquey 的合取结构的一个变体，作为一种一般结构，其中包含了来自可实现性的可实现子与真值。如同顺序可实现性，我们遵循 Honda & Yoshida 的工作，通过组合子表示将可实现子编码进代数结构。在这首项工作中，我们限定于不使用复制的 -演算，其对应的类型系统为乘法线性逻辑（MLL）。
引用
@article{arxiv.2112.14606,
title = {Concurrent Realizability on Conjunctive Structures},
author = {Emmanuel Beffara and Félix Castro and Mauricio Guillermo},
journal= {arXiv preprint arXiv:2112.14606},
year = {2021}
}