博弈语义

概述Lorenzen和Kuno Lorenz的主要动机是为直觉逻辑找到一种博弈论(他们的术语是“对话式”Dialogische Logik)语义。Blass首先指出在博弈语义和线性逻辑之间的联系。这个路线进一步由Samson Abramsky、Radhakrishnan Jagadeesan、Pasquale Malacaria和独立的由Martin Hyland和Luke Ong发展，对合成性加以特别强调，就是递归的在语法上定义策略。使用博弈语义，上面提及的作者们解决了长期存在的为可计算函数的编程语言定义完全抽象模型的问题。从此，博弈语义成为各种编程语言的完全抽象的语义模型，导致了软件模型检查的软件验证的新的语义制导的方法。