Karl Crary

9217 Gates-Hillman Center
School of Computer Science
Carnegie Mellon University
5000 Forbes Avenue
Pittsburgh, PA 15213

Phone: (412) 268-7687
Email: [my-last-name]@cs.cmu.edu

Research Interests

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, proof assistants, 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 programming languages.

Publications

Most of my publications are available online.

Software

Istari is a proof assistant intended for mathematical developments involving computation -- particularly imperative computation -- and dependent types.
CM-Lex and CM-Yacc are a lexer and parser generator for Standard ML, OCaml, and Haskell that resolve the "disembodied code" problem.
CMlib is a collection of libraries for Standard ML.

Teaching

This Fall, I am teaching Constructive Logic (15-317), an undergraduate course on intuitionistic logic, proof theory, and logic programming.
Last Spring, I taught HOT Compilation (15-417), an undergraduate course on the implementation of compilers for higher-order, typed languages.
In Fall 2023, I taught Constructive Logic.
In Spring 2023, I taught Functional Programming (15-150), an introductory course on functional programming.
In Fall 2022, I taught Constructive Logic.
In Spring 2022, I taught Functional Programming.

Former Students

"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 hear. -- 2 Timothy 4:3

A Man For All Seasons
The Gods of the Copybook Headings