Automata-Theoretic Semantics of Idealized Algol with Passive Expressions

Research output: Contribution to conference (unpublished)Paperpeer-review


Colleges, School and Institutes


Passive expressions in Algol-like languages represent computations that read the state but do not modify it. The need for such read-only computations arises in programming logics as well as in concurrent programming. It is also a central facet in Reynolds's Syntactic Control of Interference. Despite its importance and essentially basic character, capturing the notion of passivity in semantic models has proved to be difficult. In this paper, we provide a new model of passive expressions using an automata-theoretic framework recently proposed by the author. The central idea is that the store of a program is viewed as an abstract form of an automaton, with a representation of its states as well as state transitions. The framework allows us to combine the strengths of conventional state-based models and the more recent event-based models to synthesize new "automata-based" models. Once this basic framework is set up, relational parametricity does the job of identifying passive computations.


Original languageEnglish
Number of pages24
Publication statusPublished - 4 Nov 2013
Event29th Conference on Mathematical Foundations of Programming Semantics (MFPS XXIX) - New Orelans, United States
Duration: 23 Jun 201325 Jun 2013


Conference29th Conference on Mathematical Foundations of Programming Semantics (MFPS XXIX)
CountryUnited States
CityNew Orelans


  • Idealized Algol, Relational parametricity, Functor categories, Reflexive graphs, Algebraic automata theory