- 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.

- Equationally Fully Abstract Models of PCF
- Experimenting with Formal Languages Using Forlan
- Fully Abstract Models of Programming Languages
- A Functional Model-View-Controller Software Architecture for Command-oriented Programs
- Infinite Pretty-printing in eXene
- Interdefinability of Parallel Operations in PCF
- Mechanizing Logical Relations
- Mechanizing the Proof of Adaptive, Information-theoretic Security of Cryptographic Protocols in the Random Oracle Model (EasyCrypt Proof on GitHub)
- An Operational Semantics Framework Supporting the Incremental Construction of Derivation Trees
- Parallel PCF Has a Unique Extensional Model
- Porgi: a Proof-Or-Refutation Generator for Intuitionistic Propositional Logic
- Studying the Fully Abstract Model of PCF within its Continuous Function Model
- Substitution Revisited
- You Sank My Battleship! A Case Study in Secure Programming

- Kripke: a Countermodel Checker for Intuitionistic Propositional Logic
- Lambda: a Program for Solving Lambda Definability Problems of Order at most Two
- Porgi: a Proof-Or-Refutation Generator for Intuitionistic Propositional Logic
- An SML/NJ Library for Pretty-printing Possibly Infinite Syntax Trees

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 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
lecture slides.

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.

- Dustin deBoer
- Christian Haack
- Sam Henke
- Jonathan Hoag
- Matthew Hoag
- Cole Hoosier
- Sergey Kotov

Alley Stoughton (alley.stoughton@icloud.com)