Name Binding
Abstracting Syntax (with Brian Aydemir and Stephan A. Zdancewic), Technical Reports (CIS) (2009)
Binding is a fundamental part of language specification, yet it is both difficult and tedious...
Engineering Formal Metatheory (with Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, and Randy Pollack), Departmental Papers (CIS) (2008)
Machine-checked proofs of properties of programming languages have become a critical need, both for increased...
Mechanized Metatheory for the Masses: The POPLMARK Challenge (with Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, and Stephan A. Zdancewic), Departmental Papers (CIS) (2005)
How close are we to a world where every paper on programming languages is accompanied...
Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism (Extended Version) (with Geoffrey Washburn), Technical Reports (CIS) (2003)
Higher-order abstract syntax is a simple technique for implementing languages with functional programming. Object variables...
Haskell Type System
FPH: First-class Polymorphism for Haskell Declarative, Constraint-free Type Inference for Impredicative Polymorphism (with Dimitrios Vytiniotis and Simon Peyton Jones), Departmental Papers (CIS) (2008)
Languages supporting polymorphism typically have ad-hoc restrictions on where polymorphic types may occur. Supporting "first...
Practical Type Inference for Arbitrary-Rank Types (with Simon Peyton Jones, Dimitrios Vytiniotis, and Mark Shields), Departmental Papers (CIS) (2007)
Haskell's popularity has driven the need for ever more expressive type system features, most of...
Boxy Types: Inference for Higher-Rank Types and Impredicativity (with Dimitrios Vytiniotis and Simon Peyton Jones ), Departmental Papers (CIS) (2006)
Languages with rich type systems are beginning to employ a blend of type inference and...
Practical Type Inference for Arbitrary-Rank Types: Technical Appendix (with Dimitrios Vytiniotis and Simon Peyton Jones), Technical Reports (CIS) (2005)
Generic Programming
RepLib: A library for derivable type classes, Departmental Papers (CIS) (2006)
Some type class instances can be automatically derived from the structure of types. As a...
A Design for Type-Directed Programming in Java (with Liang Huang), Departmental Papers (CIS) (2005)
Type-directed programming is an important and widely used paradigm in the design of software. With...
Generalizing Parametricity Using Information-flow (with Geoffrey Washburn), Departmental Papers (CIS) (2005)
Run-time type analysis allows programmers to easily and concisely define operations based upon type structure,...
Generalizing Parametricity Using Information Flow (Extended Version) (with Geoffrey Washburn), Technical Reports (CIS) (2005)
Run-time type analysis allows programmers to easily and concisely define operations based upon type structure,...
An Open and Shut Typecase (Extended Version) (with Dimitrios Vytiniotis and Geoffrey Washburn), Technical Reports (CIS) (2004)
Ad-hoc polymorphism is a compelling addition to typed programming languages. There are two different forms...
Dependent Types
Termination Casts: A Flexible Approach to Termination with General Recursion (Technical Appendix) (with Aaron Stump and Vilhelm Sjoberg), Technical Reports (CIS) (2010)
This paper proposes a type-and-effect system called Teq↓, which distinguishes terminating terms and total functions...
Functional Programming
LNgen: Tool Support for Locally Nameless Representations (with Brian Aydemir), Technical Reports (CIS) (2010)
Given the complexity of the metatheoretic reasoning about current programming languages and their type systems,...
AspectML: A Polymorphic Aspect-Oriented Functional Programming Language (with Daniel Dantas, David Walker, and Geoffrey Washburn), Departmental Papers (CIS) (2008)
This paper defines AspectML, a typed functional, aspect-oriented programming language. The main contribution of AspectML...
Low-level Types
Safe and Flexible Dynamic Linking of Native Code (with Michael Hicks and Karl Crary), Computer Science Department (2000)
We present the design and implementation of the first complete framework for flexible and safe...
No subject area
Manifest Security (with Karl Crary, Robert Harper, Frank Pfenning, Benjamin C. Pierce, and Stephan Zdancewic), Computer Science Department (2007)
This project proposes manifest security as a new architectural principle for secure extensible systems. Its...
PolyAML: A Polymorphic Aspect-Oriented Functional Programming Language (Extended Version) (with Daniel S. Dantas, David Walker, and Geoffrey Washburn), Technical Reports (CIS) (2005)
This paper defines PolyAML, a typed functional, aspect-oriented programming language. The main contribution of PolyAML...
A Calculus for Dynamic Loading (with Michael Hicks), Technical Reports (CIS) (2001)
We present the load-calculus, used to model dynamic loading, and prove it sound. The calculus...