سال انتشار: ۱۳۸۵
محل انتشار: دوازدهمین کنفرانس سالانه انجمن کامپیوتر ایران
تعداد صفحات: ۸
Hassan Haghighi – Department of Computer Engineering, Sharif University of Technology, Tehran, Iran
Seyyed Hassan Mirian-Hosseinabadi – Department of Computer Engineering, Sharif University of Technology, Tehran, Iran
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.