انجمن کامپیوتر ایران

In a two player game, the choices of our player can be modeled by angelic nondeterminism and those of our opponent by demonic nondeterminism. In this paper, we introduce some notations and semantics to Martin- Löf's theory of types which facilitate the use of angelic and demonic interpretations of nondeterminism in type theoretical specifications. Using the proposed, nondeterministic constructs, we can formally specify two player games and derive them from correctness proofs of their formal specifications.