Coalgebraic semantics of self-referential behaviours

In this thesis, we investigate the semantics of systems which can refer to themselves, e.g., by ``passing around" systems of the same kind as values (hence potential observables). For this reason, we refer to these systems as self-referential. Instances of this scenario are higher-order calculi like the λ-calculus, the calculus of higher-order communicating systems (CHOCS), the higher-order π-calculus (HO-π), HOcore, etc. It is well known that higher-order systems pose unique challenges and are difficult to reason about. Many bisimulations and proof methods have been proposed also in recent works. This ongoing active effort points out that a definition of abstract self-referential behaviour is still elusive. We address these difficulties by providing an abstract characterisation of self-referential behaviours as self-referential endofunctors, i.e. functors whose definition depends on their own final coalgebra. The construction of these functors is not trivial, since they must be defined at once with their own final coalgebra and due to the presence of both covariant and contravariant dependencies (e.g. arising from higher-order inputs). We provide such a construction, where algebraic compact functors are the key technicality, like other works dealing with mixed-variance dependencies of some kind. Similarly defined endofunctors arise from considering as object systems (i.e, those which can be values) only certain subclasses of systems (usually via some syntactic restriction) or a syntactic representations (cf. higher-order process algebras): self-referential endofunctors are shown to be universal among them. Universality renders self-referential endofunctors a touchstone for similar behavioural functors and offers the mathematical structure for assessing soundness and completeness of other models via properties of the associated universal morphisms. As a further contribution, we provide a construction capturing infinite trace semantics by finality whereas the state of the art characterisations are weakly final. This result, together with existing accounts of finite traces, allows the definition of self-referential behaviours with respect to (in)finite trace semantics.