Research

2005--2007: 'first-order clauses'; 'machine-generated resolution problems'; 'interactive proof'; 'elementary functions'; 'lightweight relevance'; 'interactive theorem proving'; 'equivalence classes'; 'concurrent systems'; 'automatic proofs'; 'proof pearl'; 'cardholder registration in SET'; 'accountability protocols'; 'source-level proof reconstruction'; 'compositional reasoning'; 'resolution prover';

2000--2004: 'interactive proof'; 'program composition'; 'fixedpoint approach'; 'security protocols'; 'mutilated chess board'; 'industrial payment protocol'; 'non-repudiation protocol'; 'yahalom protocol'; 'formal verification'; 'axiom of choice mechanised using ISABELLE/ZF'; 'cardholder registration in SET'; 'numerical theories'; 'relative consistency'; 'codatatype definitions'; 'meta-theoretic reasoning'; 'mechanical proofs'; 'axiomatic type classes'; 'simple formalisation'; 'reflection theorem'; 'formal analyses'; 'second-level security protocols';

1995--1999: 'set theory'; 'higher-order problems'; 'inductive analysis'; 'security protocols'; 'inductive methods'; 'kerberos authentication systems'; 'interactive theorem proving'; 'secrecy goals'; 'recursive authentication protocol'; 'nonstandard analysis'; 'internet protocol TLS'; 'cryptographic protocols'; 'computer algebra'; 'final coalgebras'; 'higher-order logic'; 'BAN kerberos'; 'sectioning concept'; 'formal proof'; 'II. induction'; 'abstract algebra'; 'mechanised proofs'; 'inductive approach'; 'isabelle HOL'; 'geometry theorem proving'; 'kerberos version'; 'pragmatic approach';

1990--1994: 'set theory'; 'theorem prover'; 'fixedpoint approach'; 'logic programming'; 'coinductive definitions'; 'inductive definitions'; 'functional programming'; 'functional programs';

1985--1989: 'theorem prover'; 'normalisation functions for conditional expressions'; 'intuitionistic type theory'; 'higher-order resolution'; 'unification algorithms'; 'recursion operators'; 'natural deduction';

1980--1984: 'higher-order implementation'; 'structural induction'; 'semantics-directed compiler generator';