Research

2005--2007: 'operational reasoning'; 'structural operational semantics'; 'alpha-structural recursion'; 'monadic semantics for freshness';

2000--2004: 'categorical logic'; 'order theory'; 'abstract syntax'; 'program equivalence'; 'new approach'; 'nominal unification'; 'nominal logic'; 'structural operational semantics'; 'imperative core calculus'; 'programming with bound names modulo renaming'; 'denotational semantics of staged execution of @comment open code'; 'binders made simple'; 'operational semantics'; 'operational properties';

1995--1999: 'logical relations'; 'operational equivalence'; 'fixpoint computations'; 'abstract syntax'; 'program equivalence'; 'local variables'; 'tripos theory'; 'committed form'; 'new approach'; 'process calculus'; 'operational reasoning'; 'parametric polymorphism'; 'local state'; 'process calculuses'; 'abstract syntax involving binders'; 'existential types'; 'operationally-based theories';

1990--1994: 'fixpoint computations'; 'computer science'; 'defined domains'; 'new foundations'; 'relational properties'; 'functional programs'; 'inductive definitions'; 'order quantification'; 'computational adequacy'; 'co-inductive techniques'; 'co-induction principle'; 'evaluation logic';

1985--1989: 'categorical logic'; 'category theory'; 'conceptual completeness'; 'polymorphic types'; 'cartesian closed categories'; 'non-trivial power types'; 'presentable categories'; 'set theoretic'; 'order intuitionistic logic'; '{j.} {lambek}'; 'topos-theoretic models'; 'categorical semantics';

1980--1984: 'categorical logic'; 'local variables'; 'tripos theory'; '{heyting} algebras';