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
  • 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
  • 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