TRELLYS: The TRELLYS
project seeks to design a
dependently-typed programming language that
supports both programming
and theorem proving in the same framework.
With Aaron
Stump (Iowa
State) and Tim
Sheard
(Portland State), we have been discovering
what
it means for programs and proofs to interact.
See our POPL 2014 paper, as well as papers in MSFP2012
and PLPV
2012. Also, slides from PLPV
2010 and RDP
2011, give an
overview of our work.
In 2013 and 2014, I presented a tutorial on designing dependently-typed
languages at the Oregon Programming Languages Summer School.

Dependently-Typed
Haskell: this project works to extend the type
system of Haskell with better support for
dependently-typed programing. My primary collaborators for this project are
Simon Peyton Jones and Dimitrios Vytiniotis at MSR Cambridge, and Penn
student Richard Eisenberg.

Type-directed
programming: Defining
functions via type information cuts down
on boilerplate programming as many operations
may be defined once, for
all types of data. With my student Brent
Yorgey and
collaborator Tim
Sheard
(Portland State), I developed Unbound,
a Haskell
library for
declaratively specifying binding structure and
automatically generating
free variable, alpha-equivalence and
substitution functions. This
library is built using RepLib,
an
expressive library that I developed for generic
programming in Haskell.
My student Chris
Casinghino
and I explored arity
and
type generic programming in Agda, lecture
notes
from the
Spring
School on Generic and Indexed Programming
provide a gentle
introduction.

Machine
assistance
for programming languages research:
Designing and proving
properties about programming languages is hard,
but the proofs
themselves are straightforward once you know how
to set them up. At the
same time, it is all too easy to miss the one
little case that ruins
the
whole "proof". Modern proof assistants, such as
Twelf,
Coq, and Isabelle
are good at expressing this sort of reasoning,
but it is hard to
know where to start. I've been working with the
POPLmark
team to
issue challenge
problems, organize a workshop,
explore techniques
for
reasoning
about
binding, and develop educational
materials about mechanizing programming
language metatheory. Brian
Aydemir developed a library
for
programming language metatheory (used in the
Penn tutorials) and LNgen,
a
tool for automatically proving properties about
binding.

Type
inference for
advanced type systems: Advanced type
system features, such as first-class
polymorphism,impredicative
polymorphism and generalized
algebraic datatypes,
do
not
interact
well
with
the
standard
algorithms
for type inference in
modern typed functional languages, such as ML
and Haskell. Simon
Peyton Jones,
my
students
Dimitrios
Vytiniotis,
Geoffrey
Washburn and I have incorporated ideas from
Local Type
Inference to extend the Glasgow
Haskell Compiler with support for these
features.

postal
mail: School of Engineering and Applied
Science
Department of Computer and Information Science
Levine Hall
3330 Walnut Street
Philadelphia, PA 19104-6389