Imperative programs as proofs via game semantics |
| |
Authors: | Martin Churchill Jim Laird Guy McCusker |
| |
Institution: | 1. University of Bath, United Kingdom;2. Swansea University, United Kingdom |
| |
Abstract: | Game semantics extends the Curry–Howard isomorphism to a three-way correspondence: proofs, programs, strategies. But the universe of strategies goes beyond intuitionistic logics and lambda calculus, to capture stateful programs. In this paper we describe a logical counterpart to this extension, in which proofs denote such strategies. The system is expressive: it contains all of the connectives of Intuitionistic Linear Logic, and first-order quantification. Use of Laird?s sequoid operator allows proofs with imperative behaviour to be expressed. Thus, we can embed first-order Intuitionistic Linear Logic into this system, Polarized Linear Logic, and an imperative total programming language. |
| |
Keywords: | 68Q55 03B70 03F52 18C50 |
本文献已被 ScienceDirect 等数据库收录! |
|