Reasoning about Idealized ALGOL Using Regular Languages

We explain how recent developments in game semantics can be applied to reasoning about equivalence of terms in a non-trivial fragment of Idealized Algol (IA) by expressing sets of complete plays as languages. Being derived directly from the fully abstract game semantics for IA, our method of reasoning inherits its desirable theoretical properties. The method is mathematically elementary and formal, which makes it uniquely suitable for automation. We show that reasoning can be carried out using only a meta-language of extended regular expressions, a language for which equivalence is formally decidable.

• Type: Conference
• Year: 2000
• Where: ICALP
• Authors: Dan R. Ghica, Guy McCusker
• Keywords: Abstract Game Semantics, Desirable Theoretical Properties, Game Semantics, ICALP 2000, Programming Languages