- 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 language based
I am a member of
Computer-Aided Cryptography Group. I am currently working on:
- A formalization in EasyCrypt of the indifferentiability result for
the SHA-3 Secure Hash Algorithm standard. (Joint work with Gilles
Barthe, François Dupressoir, Benjamin Grégoire and Pierre-Yves Strub).
- Proving the security of a simple private information retrieval
protocol in EasyCrypt. (Joint work with Mayank Varia.)
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