- 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
- Mechanizing Universally Composable Security (joint work with Ran
Canetti, Assaf Kfoury, Tomislav Petrovic and 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