Principles of Programming Group

Computer Science Department

Carnegie Mellon University

What We Do

The goal of the PoP group is to understand, develop, and demonstrate the principles, processes, and supporting technologies for the construction of computing systems.

Special areas of interest include: applications of logic (including formal semantics and type theory); techniques for designing and implementing programming languages; formal specification and verification of hardware and software systems.

A distinguishing characteristic of the PoP group is that it applies formal principles to problems of realistic scale and complexity, for example: automatic verification of large-scale commercial hardware systems; implementation of high-speed network communication software in the ML language; application of type-theoretic principles in the construction of realistic compilers.

Keep in Touch


Computer Science Department

Umut Acar

algorithms and data structures, parallel computing, programming languages, software systems and architecture

Stephanie Balzer

programming languages, program verification, type theory, and logic

Guy Blelloch

algorithms and data structures, parallel computing, theory of computing

Stephen Brookes

theory of computing, programming languages

Iliano Cervesato

computational logic, type theory, programming languages, concurrency

Karl Crary

formal methods/verification, logic, programming languages

Matt Fredrikson


Robert Harper

programming languages

Marjin Heule


Jan Hoffmann

verification, programming languages, resource analysis, security


Dilsun Kaynar

modeling and verification, programming languages, and security


Stefan Mitsch

modeling, refactoring, collaboration, and verification methods for hybrid systems


Bryan Parno

verification, security


Frank Pfenning

programming languages, logic, security

André Platzer

control systems, cyber physical systems, formal methods/verification, game theory, logic, programming languages, robotics, security

Electrical and Computer Engineering Department

Limin Jia

formal aspects of software security, in particular, applying formal logic to constructing software systems with known security guarantees

Departments of Mathematical Sciences and Philosophy

Jeremy Avigad

mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning

Steve Awodey

category theory, logic, philosophy of mathematics, early analytic philosophy

Richard Statman

proof theory and the theory of computation, theory of programming languages

Institute for Software Research

Jonathan Aldrich

compilers, formal methods/verification, parallel computing, programming languages, software engineering

William Scherlis

software engineering, software systems and architecture, parallel computing

Students and Postdocs

Name Position
Daniel Anderson Graduate student
Jatin Arora Graduate student
Emily Black Graduate student
Jay Bosamiya Graduate student
Katherine Cordwell Graduate student
Ankush Das Graduate student
Luiz Gustavo de Sá Graduate student
Magdalen Dobson Graduate student
Myra Dotzel Graduate student
Sydney Gibson Graduate student
Jessie Grosen Graduate student
Travis Hance Graduate student
Aditi Kabra Graduate student
David Kahn Graduate student
Abhiram Kothapalli Graduate student
Jonathan Laurent Graduate student
Klas Leino Graduate student
Evan Lohn Graduate student
Elisaweta Masserova Graduate student
Yue Niu Graduate student
Long Pham Graduate student
Klaas Pruiksm Graduate student
Joseph Reeves Graduate student
Matias Scharager Graduate student
Ziv Scully Graduate student
Siva Somayyajula Graduate student
Bernardo Anibal Graduate student
Yong Kiam Tan Graduate student
Saranya Vijayakumar Graduate student
Di Wang Graduate student
Yuanhao Wei Graduate student
Samuel Westrick Graduate student
Mingkuan Xu Graduate student
Yue Yao Graduate student
Emre Yolcu Graduate student
Han Zhang Graduate student
Yi Zhou Graduate student