- Formal language theory: toolsets and pedagogy.
- Functional programming: ML, Concurrent ML, eXene, pretty printing,
- Programming language semantics: operational semantics frameworks,
logical relations, lambda definability, full abstraction and the
relationship between operational and denotational semantics, models of
the applied typed lambda calculus PCF.
- Logic: proof search and countermodel generation for intuitionistic
- Security: formal methods for cryptography, programming languages based
I am currently working on:
- Mechanizing the proof of adaptive, information-theoretic security
of cryptographic protocols in the random oracle model (joint work
with Mayank Varia);
- Mechanizing Universal Composability (joint work with Ran Canetti
and Mayank Varia);
- A formalization in EasyCrypt of the indifferentiability result for
the SHA3 Secure Hash Algorithm standard (joint work with Cécile
Baritel-Ruet, Gilles Barthe, François Dupressoir, Benjamin Grégoire
and Pierre-Yves Strub).
The Forlan Project consists of a
toolset for experimenting with formal languages, a
draft textbook entitled Formal Language Theory:
Integrating Experimentation and Proof, and associated
I led a group continuing the development
of eXene, Gansner and Reppy's multi-threaded,
higher-order user-interface toolkit for the X window system.
Former Research Students