TY - CONF
T1 - Automata-Theoretic Semantics of Idealized Algol with Passive Expressions
AU - Reddy, Uday
PY - 2013/11/4
Y1 - 2013/11/4
N2 - 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.
AB - 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.
KW - Idealized Algol
KW - Relational parametricity
KW - Functor categories
KW - Reflexive graphs
KW - Algebraic automata theory
U2 - 10.1016/j.entcs.2013.09.020
DO - 10.1016/j.entcs.2013.09.020
M3 - Paper
SP - 325
EP - 348
T2 - 29th Conference on Mathematical Foundations of Programming Semantics (MFPS XXIX)
Y2 - 23 June 2013 through 25 June 2013
ER -