游戏式、流状计算
计算机科学中的逻辑
2007-06-17 v1
摘要
我们对顺序程序的交互式解释作一简短巡览。我们强调流状计算——即应请求计算连续的信息位。此处所考察方法的核心可追溯到 Berry 与作者在七十年代末关于具体数据结构上的顺序算法的工作，并 culminate 于编程语言 CDS 的设计，其中任意类型程序的语义均可交互式地探究。大约十年后，Cartwright 与 Felleisen 一方面的以及 Lamarche 另一方面的两个主要洞见给予了顺序性研究新的决定性推动。Cartwright 与 Felleisen 观察到顺序算法为诸如“call-cc”的控制算子提供了直接语义，并提议在 PCF 语言的语法与语义中均包含显式错误。Lamarche（未发表）将顺序算法与线性逻辑及博弈相联系。成功的博弈语义纲领自九十年代延续至今，始于 Abramsky、Jagadeesan 与 Malacaria 一方面以及 Hyland 与 Ong 另一方面对 PCF 项模型的语法无关刻画。
引用
@article{arxiv.cs/0501033,
title = {Playful, streamlike computation},
author = {Pierre-Louis Curien},
journal= {arXiv preprint arXiv:cs/0501033},
year = {2007}
}