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.

Papers (BibTeX, ACM Author Page)

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

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

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