模态 λ-演算的众多世界：I. 必然性、可能性与时间的柯里-霍华德对应
计算机科学中的逻辑
2016-05-27 v1
摘要
本文是对通过柯里-霍华德（Curry-Howard）同构对应于构造性模态逻辑的 λ-演算的综述。我们涵盖该主题的前史，然后集中于 1990 年代和 2000 年代初的发展。我们讨论逻辑方面、模态 λ-演算及其范畴语义。所综述演算背后的逻辑是 K、K4、S4 和 LTL 的构造性版本。
引用
@article{arxiv.1605.08106,
title = {The Many Worlds of Modal {\lambda}-calculi: I. Curry-Howard for Necessity, Possibility and Time},
author = {G. A. Kavvos},
journal= {arXiv preprint arXiv:1605.08106},
year = {2016}
}