picture of Jonathan Aldrich

Jonathan Aldrich

Software and Societal Systems Department and Computer Science Department
School of Computer Science
Carnegie Mellon University

Office: 422 TCS Hall

Contact Information

+1-412-268-7278 (phone)
+1-412-268-2338 (fax)
personal contact info and cell phone (CMU only)

ORCID iD 0000-0003-0631-5591

Shipping Address

Jonathan Aldrich
CMU - ISR - TCS Hall 430
4665 Forbes Avenue
Pittsburgh, PA 15213

Executive Assistant

Linda Campbell
lv2c at cs dot cmu dot edu


I work at the intersection of programming languages and software engineering. My research explores how the way we express software affects our ability to engineer software at scale. A particular theme of much of my work is improving software quality and programmer productivity through better ways to express structural and behavioral aspects of software design within source code.

I have contributed to object-oriented typestate checking, modular and gradual verification techniques for aspects and stateful programs, and new object-oriented language models. For my work specifying and verifying architecture, I received a 2006 NSF CAREER award and the 2007 Dahl-Nygaard Junior Prize (press release, article).


During my Spring 2022 sabbatical, I co-founded Noteful, a company whose mission is teaching the world to read music. Our app is available on the web, iOS, and Android platforms!

New Students Wanted!

I have information for prospective Ph.D. students and advice for current students.

Active Projects

  • Gradual Verification - Analogous to gradual typing, allows programmers to effectively verify partially specified code, checking statically where possible and at run time where neceesary.
  • TTPython - a Python-based DSL making it easier to write time-sensitive IoT applications
  • From Sketches to Code for Data Scientists
  • Liquid Java - Usable Liquid Types for Java
  • Penrose - A language for visualizing mathematical objects.
  • SASyLF - An educational proof assistant for language and logic metatheory
  • Wyvern - A general-purpose language focused on security, modularity, and language extensibility.

Past Projects

  • Obsidian - A domain-specific language for writing safer smart contracts on blockchain and other platforms.
  • Plaid - A typestate-oriented, gradually typed programming language
  • AEminium - A concurrent-by-default programming language, implemented as an extension to Plaid
  • Object-Oriented Foundations - New models for object-oriented languages
  • Typestate - Verifying component and library usage constraints (Plural tool)
  • Separation Logic - Modular verification of higher-order, typed programs
  • Ownership and Architecture - Capturing the high-level structure of object graphs
  • ArchJava Enforcing run-time software architecture within object-oriented code
  • Crystal - A Eclipse-based framework for teaching dataflow analysis


Selected talks and tutorials


All papers

Curriculum Vitae (html, PDF)


I'm a member of the ACM Publications Board and I've created an informal FAQ to help people deal with publications issues that may come up. Questions and feedback on how we can do a better job is welcome!


In August 2003, I started teaching at Carnegie Mellon University. Before that, I was a graduate student in Computer Science and Engineering at the University of Washington, working with Craig Chambers and David Notkin.

My wife Becky Billock and I enjoy hiking, backpacking, and mountain climbing, and playing music together. We were married in 2000 and have two awesome kids, Seal and Evelyn.