A temporal-logic approach to binding-time analysis
A temporal-logic approach to binding-time analysis
复制标题
结合时间分析的时间逻辑方法
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
Rowan Davies
中科院分区：
文献类型：
--
作者：
Rowan Davies
咖喱 - 霍华德同构用键入 /spl lambda /-calculus项标识了证据，并相应地识别了具有类型的命题。我们展示了如何扩展这种同构以将建设性的时间逻辑与结合时间分析相关联。特别是我们展示了如何扩展咖喱 - 霍华德同构，以包括线性时间逻辑中的O（“ Next”）操作员。这产生了简单的键入/spl lambda // sup o/calculus，我们被证明等同于多级绑定时间分析，例如用于功能编程语言的部分评估中的分析。此外，我们证明/spl lambda中的归一化//可以按照与逻辑时间相对应的顺序完成，这解释了为什么/spl lambda // sup o/sup o/与部分评估有关。然后，我们将/spl lambda // sup o/sup o/sup o/to小型功能语言，mini-ml/sup o/，并为其提供操作语义。最后，我们证明该操作语义正确反映了语言中的绑定时间，该定理是时间顺序归一化的功能编程类似物。
The Curry-Howard isomorphism identifies proofs with typed /spl lambda/-calculus terms, and correspondingly identifies propositions with types. We show how this isomorphism can be extended to relate constructive temporal logic with binding-time analysis. In particular we show how to extend the Curry-Howard isomorphism to include the O ("next") operator from linear-time temporal logic. This yields the simply typed /spl lambda//sup O/-calculus which we prove to be equivalent to a multi-level binding-time analysis like those used in partial evaluation for functional programming languages. Further, we prove that normalization in /spl lambda//sup O/ can be done in an order corresponding to the times in the logic, which explains why /spl lambda//sup O/ is relevant to partial evaluation. We then extend /spl lambda//sup O/ to a small functional language, Mini-ML/sup O/, and give an operational semantics for it. Finally, we prove that this operational semantics correctly reflects the binding-times in the language, a theorem which is the functional programming analog of time-ordered normalization.