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 15997 - Spring, 2024 15998 - Spring, 2024 15617 - Spring, 2024 15417 - Spring, 2024 15998 - Fall, 2024 15997 - Fall, 2024 15996 - Fall, 2024 15657 - Fall, 2024 15317 - Fall, 2024 Research/Teaching 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 Journal Article A focused solution to the avoidance problem 2020 • Journal of Functional Programming • 30: Crary K Journal Article Fully Abstract Module Compilation 2019 • Proceedings of the ACM on Programming Languages • 3: Crary K Conference Hygienic Source-Code Generation Using Functors 2018 • Lecture Notes in Computer Science • 10702:53-60 Crary K Conference Strong Sums in Focused Logic 2018 • Proceedings - Symposium on Logic in Computer Science • 265-274 Crary K Preprint TWAM: A Certifying Abstract Machine for Logic Programs 2018 Bohrer R, Crary K
Journal Article A focused solution to the avoidance problem 2020 • Journal of Functional Programming • 30: Crary K
Journal Article Fully Abstract Module Compilation 2019 • Proceedings of the ACM on Programming Languages • 3: Crary K
Conference Hygienic Source-Code Generation Using Functors 2018 • Lecture Notes in Computer Science • 10702:53-60 Crary K
Conference Strong Sums in Focused Logic 2018 • Proceedings - Symposium on Logic in Computer Science • 265-274 Crary K