Categorical Semantics of Programming Languages

The Team

Projects

Research Activities

• Axiomatic and Synthetic Domain Theory. The first identifies minimal requirements on categories of domains to ensure the existence of basic constructions, mainly linked to recursive definitions of types and functions. The second provides models and model constructions, in which categories of domains are embedded as full reflective sub-categories in a logical universe of sets (usually a topos).
• Programming Language Semantics. The main efforts are on modelling important language features (e.g. parametricity in polymorphism, computational aspects, phase-distinction) using category-theoretic tools (like internally complete categories, monads, fibrations). Often this modelling has a feedback into language design (e.g. the use of monads in Haskell, the addition of higher order functors to ML modules). There is also work in progress on intensional semantics for complexity, and on extensions of ML with shapely types (in collaboration with B. Jay). There is also an interest in modelling paradigmantic languages (e.g. the pi-calculus).
• Evaluation Logic. This is an extension of predicate calculus for metalanguges with computational types. It can be used to axiomatize properties of computational monads, and as a framework for representing program logics. Its semantics fundations rely on Synthetic Domain Theory.

External collaborations