9217 Gates-Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213
Phone: (412) 268-7687
Fax: (412) 268-5576
My research interests are in applying programming language technology
to improve the development, maintenance, and performance of software
systems. I am particularly interested in the application of type
theory to systems programming, in mechanization of the metatheory of
programming languages, in type-oriented compilation strategies, in
type-based certification of machine code, and in the design of
practical, high- or low-level programming languages.
Most of my publications are available online.
This Spring, I am teaching HOT
Compilation (15-417), an undergraduate course on the
implementation of compilers for higher-order, typed languages.
- Last Fall, I taught Type Systems (15-814), a graduate course
on type systems for programming languages and logic.
In Spring 2017, I taught HOT Compilation.
In Fall 2016, I taught Type Systems.
In Spring 2016, I taught Computation and Deduction (15-851), a
graduate course on logical frameworks and machine-checkable proofs.
In Fall 2015, I taught HOT
In Spring 2015, I taught Foundations of Programing Languages (15-312), an undergraduate course on programming language theory.
In Fall 2014, I taught Constructive Logic (15-317), an undergraduate course on intuitionistic logic, proof theory, and logic programming.
"Of all the commandments, which is the most important?"
"The most important one," answered Jesus, "is this: 'Hear, O Israel, the
Lord our God, the Lord is one. Love the Lord your God with all your heart and
with all your soul and with all your mind and with all your strength.' The
second is this: 'Love your neighbor as yourself.' There is no commandment
greater than these."
-- Mark 12:29-31