Projects per year
Abstract
We describe a type theory or metalanguage for constructing and reasoning about higher-order programs with global and local state, and its categorical model. This provides an encapsulation primitive for abstracting global state and making it local to an object, so that it is passed only between its invocations. Our calculus and its semantics extend the interpretation of lambda-terms in a Cartesian closed category with a monoidal action on a category of evaluation contexts - the sequoid - which is dual to the action of the function type. This gives an interpretation of a new type constructor which allows the representation of both global state - via "state-passing-style" interpretation which uses it to represent output states - and local state, via encapsulation, which corresponds to the unique map into a final coalgebra for the sequoid. This provides the equational theory of our calculus with a coinduction rule for proving equivalence between objects with local state. We show that this theory is sound and complete with respect to the categorical semantics by constructing a term model and we show that it is consistent by giving a concrete example based on a category of games and strategies previously used to interpret general references.
Original language | English |
---|---|
Pages (from-to) | 203-222 |
Number of pages | 20 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 347 |
DOIs | |
Publication status | Published - 30 Nov 2019 |
Event | 35th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2019 - London, UK United Kingdom Duration: 4 Jun 2019 → 7 Jun 2019 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science
Fingerprint
Dive into the research topics of 'From Global to Local State, Coalgebraically and Compositionally'. Together they form a unique fingerprint.Projects
- 2 Finished
-
Semantic Types for Verified Program Behaviour
Laird, J. (PI)
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council
-
Semantic Structures for Higher-Order Information Flow
Laird, J. (PI)
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council