Propositions as games as types

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.The idea of re-working the results of Game-Theoretical Semantics in Martin-Löf's Type Theory dates back to a seminar on constructive logic led by Jan von Plato in the Department of Philosophy, University of Helsinki, since Spring 1986. I have gained a lot from discussions in the seminar and personally with Jan von Plato. The essential content of this paper has also been presented in the Departments of Mathematics and Philosophy, University of Stockholm, in seminars led by Per Martin-Löf and Dag Prawitz, respectively, and in this case also I have enjoyed personal conversation with the seminar leaders. Other persons I wish to thank are Jaakko Hintikka and Göran Sundholm.