Dipartimento di Informatica e Scienze dell'Informazione
Categorical Semantics of Programming Languages
Prof. Eugenio Moggi ,
Prof. Giuseppe Rosolini
Dr. Anna Bucalo
Cristiano Calcagno ,
Former PhD students:
The activities are centered around domain theory, programming language
semantics and program logics.
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.
Edinburgh University (LFCS):
Queen Mary and Westfield College:
University of Technology, Sydney:
Ecole Normale Superieure, Paris:
INRIA, Sophia Antipolis:
Comments to: Eugenio Moggi.
Last Updated: 24 Apr 1999