Open Access Te Herenga Waka-Victoria University of Wellington
thesis_access.pdf (530.27 kB)

A Modal Proof Theory for Polynomial Coalgebras

Download (530.27 kB)
posted on 2021-11-03, 01:49 authored by Friggens, David

The abstract mathematical structures known as coalgebras are of increasing interest in computer science for their use in modelling certain types of data structures and programs. Traditional algebraic methods describe objects in terms of their construction, whilst coalgebraic methods describe objects in terms of their decomposition, or observational behaviour. The latter techniques are particularly useful for modelling infinite data structures and providing semantics for object-oriented programming languages, such as Java. There have been many different logics developed for reasoning about coalgebras of particular functors, most involving modal logic. We define a modal logic for coalgebras of polynomial functors, extending Rößiger’s logic [33], whose proof theory was limited to using finite constant sets, by adding an operator from Goldblatt [11]. From the semantics we define a canonical coalgebra that provides a natural construction of a final coalgebra for the relevant functor. We then give an infinitary axiomatization and syntactic proof relation that is sound and complete for functors constructed from countable constant sets.


Copyright Date


Date of Award



Te Herenga Waka—Victoria University of Wellington

Rights License

Author Retains Copyright

Degree Discipline

Logic and Computation

Degree Grantor

Te Herenga Waka—Victoria University of Wellington

Degree Level


Degree Name

Master of Science

Victoria University of Wellington Item Type

Awarded Research Masters Thesis



Victoria University of Wellington School

School of Mathematics, Statistics and Computer Science


Goldblatt, Robert