Automata-Theoretic Semantics of Idealized Algol with Passive Expressions
Research output: Contribution to conference (unpublished) › Paper › peer-review
Authors
Colleges, School and Institutes
Abstract
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.
Details
Original language | English |
---|---|
Pages | 325-348 |
Number of pages | 24 |
Publication status | Published - 4 Nov 2013 |
Event | 29th Conference on Mathematical Foundations of Programming Semantics (MFPS XXIX) - New Orelans, United States Duration: 23 Jun 2013 → 25 Jun 2013 |
Conference
Conference | 29th Conference on Mathematical Foundations of Programming Semantics (MFPS XXIX) |
---|---|
Country | United States |
City | New Orelans |
Period | 23/06/13 → 25/06/13 |
Keywords
- Idealized Algol, Relational parametricity, Functor categories, Reflexive graphs, Algebraic automata theory