From Global to Local State, Coalgebraically and Compositionally

Research output: Contribution to journalConference article

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 languageEnglish
Pages (from-to)203-222
Number of pages20
JournalElectronic Notes in Theoretical Computer Science
Volume347
DOIs
Publication statusPublished - 30 Nov 2019
Event35th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2019 - London, UK United Kingdom
Duration: 4 Jun 20197 Jun 2019

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this