Skip to main content

Karl Crary

Associate Professor, School of Computer Science


Research Areas

Survivable Distributed Systems, Trustworthy Computing Platforms and Devices


Karl Crary is an Associate Professor in the School of Computer Science. Crary's research interests are in applying programming language technology to improve the development, maintenance, and performance of software systems. He is particularly interested in mechanization of the metatheory of programming languages, type-oriented compilation strategies, in type-based certification of machine code, and in the design of practical, high- or low-level programming languages.

Research Projects

A Static Approach to Operating System Security IV

Research Area: Trustworthy Computing Platforms and Devices
Researcher: Karl Crary

Proposal: Trust-free Garbage Collection for Mobile Code

Research Area: Survivable Distributed Systems
Researcher: Karl Crary


"Higher-order Representation of Substructural Logics". Karl Crary. 2010 International Conference on Functional Programming, to appear.

"A Simple Proof of Call-by-Value Standardization". Karl Crary. CMU Technical Report CMU-CS-09-137, 2009.

"A Syntactic Account of Singleton Types via Hereditary Substitution". Karl Crary. 2009 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.

"Mechanized Definition of Standard ML (alpha release)". Karl Crary and Robert Harper. 2009.

"Explicit Contexts in LF". Karl Crary. 2008 Workshop on Logical Frameworks and Meta-Languages: Theory and Practice.