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

Papers (dblp, ACM Author Page)

• EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable 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
• 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)

Tools

• 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

EasyCrypt

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.

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

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