Research
Interests
- Formal language theory: toolsets and pedagogy.
- Functional programming: ML, Concurrent ML, eXene, pretty printing,
programming methodology.
- 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
propositional logic.
- Security: formal methods for cryptography, programming languages based
security.
Tools
EasyCrypt
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 Universally Composable Security (joint work with Ran
Canetti, Assaf Kfoury, Tomislav Petrovic and Mayank Varia).
See
github.com/easyuc/EasyUC.
Forlan Project
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
lecture slides.
eXene
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
Alley Stoughton
(alley.stoughton@icloud.com)