- 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.
- Algorithms: using a proof assistant to mechanize proofs using the adversarial method for showing lower bounds.

- EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security
- Equationally Fully Abstract Models of PCF
- Experimenting with Formal Languages Using Forlan
- Formalizing Algorithmic Bounds in the Query Model in EasyCrypt
- 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
- Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
- 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 (case study code)

- 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 Universally Composable Security (joint work with Ran Canetti, Megan Chen, Assaf Kfoury, Tomislav Petrovic and Mayank Varia). See github.com/easyuc/EasyUC.
- Formalizing algorithmic lower and upper bounds using the EasyCrypt proof assistant (joint work with Mark Bun, Carol Chen, Marco Gaboardi and Weihao Qu). See github.com/alleystoughton/AlgorithmicBounds.
- Mechanizing the proof of adaptive, information-theoretic security of cryptographic protocols in the random oracle model (joint work with Mayank Varia). See github.com/alleystoughton/PCR.

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)