Order-Enriched Categories

A general treatment of program behaviour was developed with Bernhard Steffen and Michael Mendler in Compositional Characterization of Observable Program Properties .

Non-termination issues lead to the study of partial functions and their order, in Partial Functions, Ordered Categories, Limits and Cartesian Closure .

Rewriting information can be captured in a confluent category Modelling reduction in confluent categories which exploits the Church-Rosser property within the categorical structure.

This work lead to a deeper appreciation of the significance of eta-expansions in the lambda-calculus. The denotational adjunction between product and function types should lift to an enriched adjunction in the ordered setting. (An early paper Local Adjunctions is available on request.) This works best with eta-expansions instead of the original eta-contractions. The full story is presented in joint work with Neil Ghani in a paper called The Virtues of Eta-expansion .