9217 Gates-Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213
Phone: (412) 268-7687
My research interests are in applying programming language technology
to improve the development, maintenance, and performance of software
systems. I am particularly interested in type theory for software
verification, mechanization of the metatheory of programming
languages, type-oriented compilation strategies, the application
of type theory to systems programming, type-based certification of
machine code, and the design of practical, high- or low-level
Most of my publications are available online.
Frequently asked questions about prerequisites and waitlists for Functional Programming (15-150).
This Fall, I am teaching Constructive Logic (15-317), an undergraduate course on intuitionistic logic, proof theory, and logic programming.
This Spring, I taught Functional Programming (15-150), an introductory course on functional programming.
Last Fall, I taught Constructive Logic.
In Spring 2021, I taught Functional Programming.
In Fall 2020, I taught Constructive Logic.
In Spring 2020, I taught HOT
Compilation (15-417), an undergraduate course on the
implementation of compilers for higher-order, typed languages.
In Fall 2019, I taught Constructive Logic.
In Spring 2019, I taught Functional Programming.
In Fall 2018, I taught Constructive Logic.
In Spring 2018, I taught HOT Compilation (15-417).
- In Fall 2017, 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.
"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
I saw that wisdom is better than folly,
just as light is better than darkness.
The wise have eyes in their heads,
while the fool walks in the darkness;
but I came to realize
that the same fate overtakes them both.
-- Ecclesiastes 2:13-14
For the time will come when people will not put up with sound
doctrine. Instead, to suit their own desires, they will gather around
them a great number of teachers to say what their itching ears want to
-- 2 Timothy 4:3
The Gods of the Copybook Headings