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
- Ruben Martins
- Assistant Research Professor
- constraint programming, verification, synthesis, decision procedures
- Bryan Parno
- Professor
- verification, security
- Frank Pfenning
- Professor
- programming languages, logic, 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