Propositions as games as types

Aarne Ranta

pp. 377-395

in: Synthese 76 (3), 1988.

Abstract

Without violating the spirit of Game-Theoretical semantics, its results can be re-worked in Martin-Löf's Constructive Type Theory by interpreting games as types of Myself's winning strategies. The philosophical ideas behind Game-Theoretical Semantics in fact highly recommend restricting strategies to effective ones, which is the only controversial step in our interpretation. What is gained, then, is a direct connection between linguistic semantics and computer programming.