Karl Crary

Associate Professor, Director of Doctoral Programs

Website

Office 9217 Gates and Hillman Centers

Email crary@cmu.edu

Phone (412) 268-7687

Department
Computer Science Department

Administrative Support Person
Matt McMonagle

Research Interests
Programming Languages
Security and Privacy

Advisees
Matias Scharager
Joshua Grosso

CSD Courses Taught

15998 - Spring, 2025

15997 - Spring, 2025

15819 - Spring, 2025

15317 - Fall, 2024

15657 - Fall, 2024

15998 - Fall, 2024

15997 - Fall, 2024

15996 - Fall, 2024

15998 - Spring, 2024

15617 - Spring, 2024

15417 - Spring, 2024

15997 - Spring, 2024

Research Statement

My research interests are in the design and implementation of advanced programming languages and in applying programming language technology to improve the development, maintenance, and performance of software systems. I am particularly interested in the application of types to the structure and implementation of programming languages and software systems.

One current focus of my research is on mechanized metatheory. The aim of mechanized metatheory is to give proof of the properties of programming languages (for example, the type safety property says that no well-typed program can crash or otherwise violate its interface) in a form that can be checked by a computer. Not only does this give us greater confidence of the correctness of our proofs, but it also makes it possible for the proof itself to become part of a software system.

For example, we can use mechanized metatheory to provide a form of certified code. By equipping a program with a proof of type safety for the language it is provided in (this may be a source or executable language), we make it possible to determine the safety of the program automatically, simply by checking the proof and type-checking the program. Thus it is feasible to check the safety of programs in a purely automated fashion.

Another current focus of my research is on the application of certified code to operating systems.  Using certified code, we can replace the dynamic protection checks that are ubiquitous in systems today with purely static ones. Since dynamic checks can be unreliable and costly, this can improve the reliability and performance of software systems.  Moreover, static checks have greater expressive power than dynamic checks, so they can offer a greater level of protection and security than existing means.

Publications