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.

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

[website]

programming languages, program verification, type theory, and logic

[website]

algorithms and data structures, parallel computing, theory of computing

[website]

theory of computing, programming languages

[website]

computational logic, type theory, programming languages, concurrency

[website]

formal methods/verification, logic, programming languages

[website]

[website]

programming languages

[website]

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

[website]programming languages, logic, security

[website]

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

[website]

formal methods/verification, programming languages, security, computational biology

[website]

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

[website]

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

[website]

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

[website]

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

[website]

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

[website]

software engineering, software systems and architecture, parallel computing

[website]

Name |
Position |

Carlo Angiuli | Graduate student |

Brandon Bohrer | Graduate student |

Evan Cavallo | Graduate student |

Michael Coblenz | Graduate student |

Katherine Cordwell | Graduate student |

Flavio Cruz | Graduate student |

Ankush Das | Graduate student |

Henry DeYoung | Graduate student |

Nicolas Feltman | Graduate student |

Travis Hance | Graduate student |

David Henriques | Graduate student |

Fabian Immler | Postdoc |

Ryan Kavanagh | Graduate student |

David Kahn | Graduate student |

Jonathan Laurent | Graduate student |

Darya Melicher | Graduate student |

João Martins | Graduate student |

Stefan Muller | Postdoc |

Yue Niu | Graduate student |

Klaas Pruiksma | Graduate student |

Siva Somayyajula | Graduate student |

Jonathan Sterling | Graduate student |

Yong Kiam Tan | Graduate student |

Di Wang | Graduate student |

Samuel Westrick | Graduate student |

Erik Zawadzki | Graduate student |