My Research Project
My research concerns semantics of programming languages, in particular category theoretic analysis of recursion schemes and
recursive types. The basis is Freyd's work on dialgebra, i.e. a simultaneous mixed-variant generalisation of
algebra and coalgebra arising from Scott's minimality principle and Plotkin/Smythe's bilimit construction (ep-pairs).
Dialgebras appear quite frequently in denotational semantics, ranging from lambda models to models of object-based languanges.
My work aims to develop new reasoning principles for denotational semantics, e.g. by parameterising Freyd's scheme, developing a theory of "bisimulations" etc. It is well known that an algebra can be quotiented by a congruence (Birkhoff),
and similarly that a coalgebra can be quotiented by a bisimulation equivalence (Aczel, presumably), that induction is a minimality principle, and so on. On the other hand, less is known about
what properties an initial dialgebra satisfies, what kinds of "bisimulation" relations emerge, and so forth. To illustrate this, note that applicative bisimilarity is coalgebraic in the sense that a term is applied to all possible other terms after which observations are being made (divergence in Abramsky's work) and so on with new terms in case of convergence. If we instead quantify over pairs of related terms, it seems to mean going from coiteration to direcursion. While work on bisimulations exist also for mixed-variant functors, almost all of the the theory
collapsed (including existence of final system, closure under union/intersection/composition, and much more). If we take instead Freyd's work as a basis, as I have done in my work, some of this collapse can immediately be avoided, while the other properties are quite interesting open research problems.
I have in previous work said something about the relationship between parametric algebras/coalgebras, and dialgebras, from which it follows in particular that applicative bisimilarity is the kernel of a unique map between Freyd dialgebras (CALCO 2007). The latter was indeed further investigated in Fiore's PhD thesis and also in Pitts' work on relational properties of domains, which makes the Computer Laboratory an excellent venue to further the above line of work.
Finally, if you are interested in any of this, or would like to know a bit more, please just contact me in my office or elsewhere!
|
