Principles of Programming Group
Carnegie Mellon University, Computer Science Department
The goal of the PoP group is to understand, develop, and demonstrate the principles, processes, and supporting technologies for the construction of computing systems.
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, quantum computing, and probabilistic programming.
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.
Group Members
Computer Science Department
- Umut Acar
- Associate Professor
- algorithms and data structures, parallel computing, programming languages, software systems and architecture, quantum computing
- Stephanie Balzer
- Assistant Professor
- programming languages, program verification, type theory, logic
- Guy Blelloch
- Professor
- algorithms and data structures, parallel computing, theory of computing
- Iliano Cervesato
- Teaching Professor
- computational logic, type theory, programming languages, concurrency
- Karl Crary
- Professor
- formal methods & verification, logic, programming languages
- Matt Fredrikson
- Associate Professor
- security, privacy, formal methods
- Robert Harper
- Professor
- programming language design and implementation, type theory, verification of cost and correctness of programs
- Marijn Heule
- Associate Professor
- formal verification, number theory, SAT solvers, extremal combinatorics
- Jan Hoffmann
- Associate Professor
- verification, programming languages, resource analysis, security
- Dilsun Kaynar
- Associate Teaching Professor
- modeling and verification, programming languages, security
- Stefan Mitsch
- Senior Systems Scientist
- modeling, refactoring, collaboration, verification methods for hybrid systems
- Ruben Martins
- Assistant Research Professor
- constraint programming, verification, synthesis, decision procedures
- Bryan Parno
- Professor
- verification, security
- Frank Pfenning
- Professor
- programming languages, logic, security
- Andre Platzer
- Professor
- control systems, cyber physical systems, formal methods & verification, game theory, logic, programming languages, robotics, security
- Feras Saad
- Assistant Professor
- probabilistic programming languages, Bayesian inference, mathematics of computing
Electrical and Computer Engineering Department
- Limin Jia
- Research Professor
- formal aspects of software security; applying formal logic to constructing software systems with known security guarantees
Departments of Mathematical Sciences and Philosophy
- Jeremy Avigad
- Professor
- mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning
- Steve Awodey
- Professor
- category theory, logic, philosophy of mathematics, early analytic philosophy
- Richard Statman
- Professor
- proof theory, theory of computation, theory of programming languages
Software and Societal Systems Department
- Jonathan Aldrich
- Professor
- compilers, formal methods & verification, parallel computing, programming languages, software engineering
- William Scherlis
- Professor
- software engineering, software systems and architecture, parallel computing