PL Theory PhD Directory 2026–2027

Australian National University

Application deadline: ❔

Alex Potanin

security, language design, software engineering, quantum devices, trustworthy systems

Alwen Tiu

formal methods, logic, automated theorem proving, security

Dirk Pattinson

modal logic, domain theory, coalgebraic semantics, category theory

Fabian Muehlboeck

type systems, gradual typing, language design, language implementation

Liam O'Connor

property-based testing, language semantics, temporal logic

Michael Norrish

interactive theorem provers, language semantics

Nisansala Yatapanage

software verification, formal methods, concurrency, rely/guarantee, separation logic, temporal logic

Peter Hoefner

formal methods, software verification, algebraic methods, concurrency and distributed systems

Ranald Clouston

logic, type systems, type theory

Steve Blackburn

garbage collection, language implementation, performance analysis

Tony Hosking

programming language runtimes, compilation, garbage collection, data storage and management

Trustworthy Systems @ UNSW

Application deadline: Multiple (check link)

Thomas Sewell

formal methods, program verification

IST Austria

Application deadline: January 8th

Krishnendu Chatterjee

formal methods, program analysis, concurrency

Michael Sammler

automated reasoning, separation logic, formal methods

forsyte @ TU Wien

Application deadline: Multiple (check link)

Laura Kovács

automated reasoning, computer algebra, automated deduction, program verification, formal methods

KU Leuven

Application deadline: Rolling (position-based)

Bart Jacobs

program logics, separation logic, program verification, language features for security and correctness, static analysis, type systems, concurrent programming, language semantics, theorem proving, proof assistants

Dominique Devriese

modal types, dependent types, type theory, functional programming, security, verified compilation, capabilities, formalized ISAs

Tom Schrijvers

functional programming, logic programming, effect handlers, algebraic effects

CLG @ McGill University

Brigitte Pientka

type theory, dependent types, refinement types, automated reasoning, functional programming, logic programming, metaprogramming

Christophe Dubach

data-parallel language design and implementation, high-level code generation, optimization for parallel hardware (GPUs, FPGAs), advanced compiler optimization techniques, architecture design space exploration, machine learning

Clark Verbrugge

program optimization, concurrency, compilers, computer games

Université de Montréal

Stefan Monnier

type systems, Emacs, language semantics, functional programming, compilers, garbage collection

Marc Feeley

dynamic language implementation, parallel processing, functional programming, Scheme, Gambit, education in CS, computer architecture

Concordia University

Joey Paquet

design and implementation of programming languages, context-aware computing, service-oriented computing, software engineering

Université du Québec à Montréal (UQAM)

Application deadline: Rolling

Ryan Kavanagh

type systems, session types, concurrent programming, debian

Simon Fraser University

Anders Miltner

refinement types, program synthesis

Yuepeng Wang

formal methods, program verification, program synthesis

SPL @ University of British Columbia

Application deadline: December 15th

Alexander J. Summers

program verification, program analysis, formal methods

Caroline Lemieux

program analysis, static analysis, program synthesis, property-based testing, formal methods

Ronald Garcia

type systems, language design, functional programming, language semantics

William J. Bowman

verified compilation, dependent types, program verification, metaprogramming

University of Regina

Joseph Eremondi

language semantics, dependent types, type theory, gradual typing, dependent pattern matching, type error diagnosis

ProSE @ University of Toronto

Application deadline: December 1st

Azadeh Farzan

software verification, formal methods, program synthesis, security, concurrency

Ningning Xie

type systems, language design, language implementation, algebraic effects, effect handlers, functional programming

PLG @ University of Waterloo

Ondrej Lhoták

program analysis, static analysis, compilers, object-oriented programming, Scala, call graph construction, points-to analysis

Yizhou Zhang

language design, compilers, formal verification, proof assistants, probabilistic programming, machine learning

Universidad de Chile

Matías Toro

gradual typing, differential privacy, security typing, linear types, type systems, formal verification, language semantics, language design

Éric Tanter

gradual typing, type systems, algebraic effects, security typing, language semantics, language design, functional programming, object-oriented programming, formal methods

LogSem @ Aarhus University

Application deadline: Multiple (check link)

Amin Timany

type theory, formal methods, program verification, separation logic, proof assistants, distributed systems

Anders Møller

dynamic program analysis, static analysis

Andreas Pavlogiannis

formal methods, algorithmic verification, automata theory, concurrency, static & dynamic program analysis, network diffusion, evolutionary graph theory, evolutionary game theory

Daniel Gratzer

modal types, type theory, category theory, program logic, denotational semantics, dependent types

Jaco van de Pol

formal methods, model checking, automated reasoning, concurrency, distributed systems, quantum computing, quantum programming

Jean Pichon-Pharabod

model checking, separation logic, program verification, compilers, concurrency

Lars Birkedal

type theory, program verification, separation logic, distributed systems, language semantics

Magnus Madsen

algebraic effects, program analysis, static analysis, compilers, language design, logic programming, concurrency

PLS @ IT University of Copenhagen

Application deadline: Rolling (position-based)

Patrick Bahr

type systems, formal methods, functional programming, compilers

Rasmus Ejlers Møgelberg

type theory, language semantics, category theory, domain theory, type systems, algebraic effects

University of Copenhagen

Application deadline: Rolling (position-based)

Dmitriy Traytel

interactive theorem provers, automata theory, runtime verification, decision procedures, (co)induction, (co)recursion

Fritz Henglein

type systems, program analysis, functional programming, language semantics, type inference, program analysis

Martin Elsman

parallel programming, compilers, functional programming, language design, language implementation

Thomas P. Jensen

static analysis, abstract interpretation, type systems, information flow, security, program analysis, compiler verification

Troels Henriksen

parallel programming, functional programming, HPC, compilers

Aix-Marseille Université

Pierre Clairambault

language semantics, denotational semantics, linear logic, concurrency, dependent types

Ecole Normale Superieure

Albert Cohen

compilers, program analysis, optimization, computer architecture, hardware-software interface

Caterina Urban

program analysis, static analysis, program verification

Cezara Dragoi

formal verification, automated reasoning, separation logic, static analysis

Marc Pouzet

type systems, functional programming, language design, language implementation, language semantics

Xavier Rival

static analysis, abstract interpretation, shape analysis, program verification, compiler verification, probabilistic programming

INRIA

Application deadline: Rolling (position-base)

François Pottier

type systems, language design, functional programming, object-oriented programming

Kenji Maillard

type theory, dependent types, type systems, program verification, proof assistants

Luc Maranget

language design, compilers, lazy languages, concurrency

Matthieu Sozeau

type theory, dependent types, type systems, automated reasoning, proof assistants, interactive theorem provers, program verification, functional programming, metaprogramming

Nicolas Tabareau

proof assistants, Rocq, type theory, homotopy type theory, language semantics

Pierre-Marie Pédrot

type theory, proof assistants, Rocq, logic, language semantics

Xavier Leroy

algebraic effects, automated reasoning, static analysis, compilers, functional programming, concurrency

Yannick Forster

type theory, type systems, proof assistants, Rocq

Yannick Zakowski

proof assistants, language semantics, compiler verification, concurrency, memory models, interactive theorem proving, Rocq

CISPA Helmholtz Center

Application deadline: Rolling (position-based)

Simon Oddershede Gregersen

type systems, program verification, separation logic, distributed systems, formal methods, interactive theorem provers

Karlsruhe Inst. of Technology

Sebastian Erdweg

static analysis, abstract interpretation, incremental computation, domain-specific languages, program analysis, soundness

Max Planck Society

Catalin Hritcu

verified compilation, memory management, program verification, dependent types, language semantics, property-based testing, cryptography, information flow control analysis

Deepak Garg

security, privacy, type systems, information flow, separation logic, logic, incremental computation

Derek Dreyer

separation logic, type systems, Rust, memory models, concurrency, compiler verification, dependent types, language semantics, modularity

Georg Zetzsche

model checking, automated reasoning, concurrency, program verification, formal methods

Gilles Barthe

program verification, relational verification, security, cryptography, differential privacy, formal methods, logic

Rupak Majumdar

automated reasoning, program analysis, program verification

Viktor Vafeiadis

memory models, concurrency, separation logic, program verification, model checking, compiler verification, proof assistants, non-volatile memory, language semantics

RWTH Aachen University

Joost-Pieter Katoen

model checking, concurrency, probabilistic programming, formal methods, language semantics

Saarland University

Benjamin Lucien Kaminski

formal methods, program verification, program analysis, static analysis, concurrency, probabilistic programming

Sebastian Hack

program analysis, program synthesis, compilers, domain specific languages

TU Braunschweig

Roland Meyer

formal verification, automata theory, concurrency, memory models, game theory, language semantics

PG @ TU Darmstadt

Guido Salvaneschi

distributed systems, reactive programming, security, testing, e-graphs

TU Kaiserslautern

Anthony Widjaja Lin

formal methods, automated reasoning, program synthesis

University of Freiburg

Andreas Podelski

program verification, model checking, program analysis

Peter Thiemann

functional programming, type systems, type classes, session types, web programming, program generation, static analysis, language-based security

University of Tübingen

Jonathan Immanuel Brachthäuser

algebraic effects, effect handlers, effect systems, continuations, type systems

Klaus Ostermann

functional programming, type systems, program analysis, object-oriented programming, program transformation

University of Athens

Application deadline: Rolling (contact advisor directly)

Dimitris Mitropoulos

software engineering, security, program analysis

Yannis Smaragdakis

type systems, program analysis, static analysis, compilers, memory management, domain specific languages, object-oriented programming, parallel programming, concurrency, distributed systems, formal methods

TACO @ HKUST

Application deadline: December 1st

Lionel Parreaux

type systems, compilers, functional programming, domain specific languages

PL Group @ University of Hong Kong

Application deadline: December 1st

Bruno C. d. S. Oliveira

type systems, functional programming, object-oriented programming

National Inst. of Informatics

Taro Sekiyama

type theory, type systems, program verification

University of Tokyo

Application deadline: ❔

Naoki Kobayashi

higher-order model checking, program verification, type systems, automated reasoning, security protocols, resource usage analysis

University of Tsukuba

Hiroshi Unno

refinement types, program verification, higher-order model checking, automated reasoning, temporal verification, termination analysis

Radboud University

Robbert Krebbers

program verification, separation logic, static analysis, language semantics

PL Group @ TU Delft

Benedikt Ahrens

type theory, functional programming, language semantics, homotopy type theory, univalent foundations, category theory

Casper Bach

domain-specific languages, language design, metaprogramming, algebraic effects, language semantics

Jesper Cockx

dependent types, type theory, Agda, proof assistants

Soham Chakraborty

formal methods, program analysis, compilers, memory management, concurrency

Utrecht University

Wouter Swierstra

dependent types, functional programming

VU Amsterdam

Klaus von Gleissenthall

refinement types, formal methods, distributed systems

University of Wroclaw

Dariusz Biernacki

functional programming, language semantics, abstract machines, continuations, control effects, Curry-Howard isomorphism, program equivalence

Maciej Piróg

type theory, dependent types, automated reasoning, interactive theorem provers, program analysis

Universidade de Lisboa

Alcides Fonseca

program synthesis, liquid types, concurrent programming, parallel programming

Bernardo Toninho

type theory, type systems, concurrency, distributed systems

José Fragoso Santos

automated reasoning, program analysis, static analysis, program synthesis, logic programming, object-oriented programming, language-based security, formal methods

Nuno P. Lopes

model checking, static analysis, compilers, program verification, formal methods

Vasco Thudichum Vasconcelos

concurrency, distributed systems, type systems, process calculi, specification and verification

Nanyang Technological University

C.-H. Luke Ong

probabilistic programming, game semantics, higher-order model checking, lambda calculus, type theory, algorithmic game theory, categorical logic

Conrad Watt

WebAssembly, formal methods, concurrency

Yong Kiam Tan

deductive verification, interactive theorem proving, automated reasoning, compilers, formalized mathematics, hybrid systems, security

PLSE @ National University of Singapore

Ilya Sergey

program verification, distributed systems, program synthesis, proof assistants, Lean

Umang Mathur

concurrency, formal methods, hardware design, program analysis, automata theory, program synthesis, logic

DGIST

Minseok Jeon

program analysis, program synthesis, domain specific languages, functional programming, object-oriented programming

Yoonseung Kim

formal methods, compilers, language design, object-oriented programming, distributed systems

Hanyang University

Woosuk Lee

program synthesis, program analysis, program repair, software engineering, compilers, security

KAIST

Hongseok Yang

probabilistic programming, program analysis, machine-learning

Kihong Heo

program analysis, program synthesis, language-based security

Korea University

Hakjoo Oh

static analysis, program verification, software testing, fuzzing, program repair, program synthesis, quantum programming

POSTECH

Wonyeol Lee

language design, program verification, probabilistic programming

Seoul National University

Chung-Kil Hur

type theory, automated reasoning, interactive theorem provers, concurrency, program verification, probabilistic programming

Kwangkeun Yi

static program analysis, software verification, program analysis

State University of New York, Korea

Zhoulai Fu

security, program analysis, testing, program verification, machine-learning, abstract interpretation, scientific computing

IMDEA Software Institute

Application deadline: Rolling (position-based)

Aleksandar Nanevski

type theory, interactive theorem provers, dependent types, compilers

Niki Vazou

type systems, refinement types, program verification, automated reasoning

Chalmers/GU

Andreas Abel

program verification, dependent types, type theory, functional programming, type systems, modal types, automated reasoning

Magnus O. Myreen

program verification, interactive theorem provers

Nils Anders Danielsson

dependent types, functional programming, proof assistants, interactive theorem provers, type theory, type systems, modal types, Agda

Uppsala University

Bengt Jonsson

formal methods, distributed systems, language semantics, program verification, concurrency, security

Tobias Wrigstad

memory management, type systems, security, data-race freedom, concurrency, garbage collection, verified compilation, nominal typing

EPFL

Application deadline: December 1st

Clément Pit-Claudel

compilers, formal methods

Martin Odersky

language design, language implementation, Scala

Nate Foster

proof assistants, type systems, networking

Viktor Kuncak

automated reasoning, program verification, formal methods, program synthesis, proof assistants, parsing

ETH Zurich

Application deadline: Rolling (position-based)

Peter Müller

automated reasoning, Viper

Ralf Jung

formal methods, Rust

Zhendong Su

compilers, security, education

Università della Svizzera italiana

Walter Binder

program analysis, concurrency, parallel programming, language implementation

Heriot-Watt University

Andrew Ireland

automated reasoning, theorem proving, program verification, software safety, static analysis

Ekaterina Komendantskaya

logic, AI safety, AI verification, formal methods, security

Filip Sieczkowski

separation logic, language semantics, concurrency, effect handlers

Hans-Wolfgang Loidl

parallel programming, functional programming, language implementation, symbolic computation

Jamie Gabbay

nominal techniques, foundations of computer science, logic, set theory, abstraction

James McKinna

dependent types, type theory, proof assistants, bidirectional transformations, lambda calculus, Agda

Joe Wells

type systems, rewriting, language design, language implementation, security

Jurriaan Hage

static analysis, type error diagnosis, functional programming, software analysis, testing

Kathrin Stark

proof assistants, interactive theorem proving, mechanized proofs, formal verification

Lilia Georgieva

formal methods, program analysis, security, knowledge representation

Marko Doko

foundations of mathematics, interactive theorem proving, program verification, formal methods, weak memory concurrency

Radu Mardare

logics for algebras and co-algebras, quantitative algebraic reasoning, approximation theories for systems, reasoning about probabilistic and stochastic systems, behavioural metrics

Rob Stewart

domain-specific languages, parallel programming, dataflow programming, FPGA languages, compiler verification

Imperial College London

Alastair F. Donaldson

formal methods, testing, parallel programming, compilers, concurrency, software verification, GPU programming, HPC

Azalea Raad

concurrency, language semantics, static analysis, weak memory models, program logic, formal methods

Nicolas Wu

language semantics, domain specific languages, effect handlers

Nobuko Yoshida

type systems, type theory, session types, language semantics, information flow analysis, distributed systems, Hoare logic, concurrency

Philippa Gardner

program verification, formal methods

Sophia Drossopoulou

concurrency, automated reasoning, program verification

King's College London

Stephen Kell

language implementation, compilers, language design

Queen Mary University of London

Raymond Hu

distributed systems, type systems, session types, generics, refinement types, software verification

Vasileios Klimis

model checking, compilers, quantum computing

Royal Holloway Univ. of London

Francisco Ferreira

type systems, formal methods, concurrency, modal types

Julien Lange

type systems, program verification, session types, automata theory, static analysis, GPU program verification, distributed systems

Matthew Hague

program verification, model checking, concurrency

Reuben N. S. Rowe

type systems, program verification, automated reasoning, separation logic, program synthesis, language design, concurrency

Theory Group @ University of Birmingham

Sergey Goncharov

algebraic effects, program verification, language semantics, category theory

University of Bristol

Eddie Jones

formal methods, functional programming, logic programming, formal verification

G. A. Kavvos

homotopy type theory, modal types, category theory, concurrency, security

Meng Wang

functional programming, bidirectional programming, software engineering, testing

Steven Ramsay

functional programming, automated reasoning, model checking

University of Cambridge

Application deadline: December 2nd (check link for more)

Anil Madhavapeddy

OCaml, functional programming

Jeremy Yallop

OCaml, metaprogramming, program verification, algebraic effects

Neel Krishnaswami

program verification, language design, language semantics, type theory

Peter Sewell

type systems, formal methods, concurrency, memory management, program verification

Tobias Grosser

formal methods, compilers, language design, HCI, SMT

LFCS @ University of Edinburgh

Amir Shaikhha

domain-specific languages, databases, compilers

Ajitha Rajan

software engineering, software testing, static analysis, robustness and interpretability of AI models

Björn Franke

compilers, JIT compilers, parallelisation, dynamic binary translation, processor simulation

Chris Heunen

quantum programming languages, categorical semantics

David Aspinall

software security and privacy, theorem proving, specification and verification

Elizabeth Polgreen

program synthesis, software verification

Ian Stark

programming language models, concurrency

Jacques Fleuriot

formal verification, interactive theorem proving

James Cheney

databases, logic, verification, provenance, scientific-data management, security

Markulf Kohlweiss

formal verification of cryptographic-protocol designs and implementations

Mike O'Boyle

compilers, machine-learning-based compilation, heterogeneous systems, design space exploration

Myrto Arapinis

provable security, verification of cryptographic protocols, formal models, applied cryptography, quantum cryptography, electronic voting

Ohad Kammar

programming-language theory, probabilistic programming, metaprogramming, category theory, logic in computer science

Paul Jackson

formal verification of hardware, software and cyber-physical systems, interactive theorem proving

Perdita Stevens

software engineering, model-driven engineering

Peter Buneman

query languages, semi-structured data, data provenance

Rob van Glabbeek

foundations of concurrency and distribution

Sam Lindley

functional programming, effect handlers, behavioural types, metaprogramming, type inference

University of Glasgow

Blair Archibald

modelling concurrent systems, parallel functional programming

Colin Perkins

protocol specifications and standards

Gerardo Aragon Camarasa

programming languages for robotics

H. Gül Çalikli

empirical software engineering, cognitive psychology, machine learning, software quality

Jeremy Singer

managed runtime systems

José Cano Reyes

hardware-software co-design, edge computing

Michele Sevegnani

concurrent modelling languages

Ornela Dardha

behavioural types, mechanised programming language theory

Paul Harvey

runtime systems, adaptability, autonomous networks

Quintin Cutts

programming language education

Simon Fowler

functional programming, concurrent programming, behavioural types, multi-tier programming

Simon J. Gay

behavioural types, quantum programming languages

Wim Vanderbauwhede

programming language approaches to security, compilation to hardware, low-carbon and sustainable computing

PLAS @ University of Kent

David Castro-Perez

interactive theorem provers, language design, language implementation, concurrency, distributed systems, parallel programming

Dominic A. Orchard

type theory, type systems, functional programming, program verification

Mark Batty

compilers, concurrency, formal methods

FP Lab @ University of Nottingham

Graham Hutton

functional programming, program correctness, compiler calculation, monadic parsing, program reasoning

Thorsten Altenkirch

type theory, dependent types, functional programming, logic programming, category theory

University of Oxford

Application deadline: ❔

Sam Staton

probabilistic programming, quantum computing, quantum programming, category theory

University of Sheffield

Andrei Popescu

proof assistants, type theory, automated reasoning, language-based security

University of St Andrews

Adam Barwell

concurrency, parallelism, refactoring, behavioural types

Christopher Brown

refactoring, energy-aware programming, parallel programming

Edwin C. Brady

dependent types, type-driven development, domain-specific languages, reasoning about effects

Ian Miguel

constraint modelling and solving

Olexandr Konovalov

programming language education, modelling

Özgür Akgün

domain-specific languages, constraint solutions, automated configuration

Ruth Hoffmann

domain-specific languages, models and symmetry reduction

Susmit Sarkar

formal architecture, memory consistency, compiler correctness

Tom Spink

compiler implementations, runtime systems, security

University of Stirling

Patrick Maier

parallel and distributed programming languages, parallel symbolic computation, parallel cost models

MSP @ University of Strathclyde

Clemens Kupke

coalgebraic modelling of systems, logical verification, model-checking, fixpoint logics, game-theoretic semantics, automata theory

Conor McBride

dependent type theory, functional programming, effects and handlers, programming language design and metatheory, category theory

Fredrik Nordvall Forsberg

dependent type theory, homotopy type theory, constructive mathematics, categorical semantics of programming languages

Guillaume Allais

type-driven programming, correct-by-construction methodology, proof automation, generic programming

Jan de Muijnck-Hughes

applications of type systems, dependent types, and functional programming to make systems more trustworthy

Robert Atkey

formal analysis of programming languages, type theory, denotational semantics, theorem provers

Ross Horne

protocol verification, session types, proof theory, attack trees, logic on graphs

University of the West of Scotland

Paul Keir

compilers, heterogeneous systems, metaprogramming, functional programming

Binghamton University

Application deadline: Rolling

Eric Atkinson

language implementation, program analysis, formal methods, language design

William T. Hallahan

program verification, program synthesis, program analysis, networking

Yu David Liu

energy-aware software, energy-efficient software, security

Boston College

Application deadline: January 2nd

Aaron Stump

type theory, dependent types, lambda encodings, automated reasoning, intuitionistic logic, functional programming

Boston University

Application deadline: December 15th

Ankush Das

security, distributed systems

Marco Gaboardi

formal methods, differential privacy, refinement types, dependent types, type systems, sensitivity analysis

PLT @ Brown University

Application deadline: December 15th

Will Crichton

HCI, Rust

POP @ Carnegie Mellon University

Application deadline: ❔

Feras Saad

probabilistic programming

Frank Pfenning

type theory, type systems

Heather Miller

distributed systems, concurrency, type systems, functional programming, eventual consistency, edge computing, serialization, Scala

Jan Hoffmann

model checking, type systems, static analysis, probabilistic programming, formal methods

Jonathan Aldrich

gradual typing, separation logic, static analysis, language design, object-oriented programming, formal methods

Robert Harper

type theory, proof assistants, compilers, functional programming

Stephanie Balzer

type systems, separation logic, functional programming, object-oriented programming, concurrency, language-based security

Umut A. Acar

formal methods, concurrency, parallel programming, quantum computing, self-adjusting computation, machine learning

PL @ Cornell University

Application deadline: December 15th

Adrian Sampson

computer architecture, hardware-software interface, approximate computing, compilers, hardware design

Alexandra Silva

category theory, automata theory, Kleene algebra, language semantics, formal verification, automata learning

Andrew C. Myers

type systems, compilers, functional programming, object-oriented programming, language-based security, formal methods, probabilistic programming

J. Gregory Morrisett

type systems, compilers, memory management, language-based security, formal methods

Sorin Lerner

program verification, security, privacy, HCI, live programming, program synthesis, automated theorem proving, machine learning for proofs, web security

Justin Hsu

type systems, dependent types, refinement types, formal methods, separation logic, program analysis, language design, functional programming, language-based security, probabilistic programming

Georgia Institute of Technology

Application deadline: December 15th

Jacob Laurel

static analysis, object-oriented programming, probabilistic programming

Qirun Zhang

program analysis, static analysis, compilers, language design

Santosh Pande

compilers, program analysis, static analysis, runtime analysis, hardware security, embedded systems

Vivek Sarkar

compilers, language implementation, parallel programming, HPC, distributed systems

Harvard University

Application deadline: December 15th

Nada Amin

program synthesis, metaprogramming, probabilistic programming

Stephen Chong

compilers, language-based security

Wonks @ Indiana University

Application deadline: December 15th

Amr Sabry

language semantics, continuations, monadic effects, staged computation, quantum computing, functional programming

Carlo Angiuli

type theory, dependent types, type systems, proof assistants, functional programming

Chung-chieh Shan

probabilistic programming, language semantics, language design, logic

Jeremy G. Siek

dependent types, gradual typing, proof assistants, compilers, domain specific languages, functional programming, metaprogramming, language semantics, language-based security

Sam Tobin-Hochstadt

gradual typing, type systems, program analysis, language design, functional programming, object-oriented programming, formal methods

PL @ Massachusetts Inst. of Technology

Application deadline: December 1st

Adam Chlipala

dependent types, program verification, automated reasoning, proof assistants, program analysis, compilers, language design, functional programming, concurrency

Armando Solar-Lezama

type systems, model checking, automated reasoning, program analysis, static analysis, program synthesis, compilers

Michael Carbin

program analysis, language design, functional programming, object-oriented programming, probabilistic programming

Rachit Nigam

compilers, domain specific languages

Saman P. Amarasinghe

compilers, language implementation, language design, domain specific languages

ACSys @ New York University

Application deadline: December 1st

Joseph Tassarotti

formal methods, separation logic, program synthesis, concurrency, distributed systems, probabilistic programming

Patrick Cousot

program verification, model checking, program analysis, static analysis, compilers

Sam Westrick

separation logic, memory management, functional programming, parallel programming

Thomas Wies

type systems, model checking, automated reasoning, interactive theorem provers, separation logic, program analysis, static analysis, language design, functional programming, object-oriented programming, concurrency

PRL @ Northeastern University

Application deadline: December 15th

Amal Ahmed

type theory, type systems, dependent types, gradual typing, separation logic, compilers, language design, functional programming, object-oriented programming, concurrency, formal methods, probabilistic programming

Arjun Guha

program verification, program synthesis, compilers

Chris Martens

proof assistants, type systems, language design, logic programming

Frank Tip

program analysis, static analysis, compilers

Jan Vitek

type systems, gradual typing, program analysis, compilers, memory management

Joshua Gancher

proof assistants, distributed systems

Olin Shivers

compilers, programming language design, language semantics, systems programming, higher-order languages

Steven Holtzen

type systems, program verification, automated reasoning, separation logic, probabilistic programming

Northwestern University

Application deadline: December 1st

Christos Dimoulas

contracts, gradual typing, language-based security, functional programming, language semantics, program analysis

Robert Bruce Findler

formal methods

Ohio State University

Michael D. Bond

concurrency, memory models, garbage collection, program analysis, runtime systems, security, information flow control

PL @ Princeton University

Application deadline: December 15th

David Walker

language design, functional programming, language-based security

Mae Milano

compilers, language design, functional programming, concurrency, distributed systems

Zachary Kincaid

model checking, automated reasoning, program analysis, object-oriented programming, concurrency

PurPL @ Purdue University

Application deadline: December 1st

Benjamin Delaware

proof assistants, type systems, automated reasoning, program synthesis, Rocq

Milind Kulkarni

compilers, object-oriented programming

Suresh Jagannathan

type systems, program verification, language design, functional programming, object-oriented programming

Tiark Rompf

proof assistants, program analysis, compilers, metaprogramming

Rice University

Application deadline: January 1st (Check link there's more)

Konstantinos Mamouras

stream processing, runtime verification, program semantics, Kleene algebra, logics for verification

Rutgers University

He Zhu

refinement types, model checking, static analysis, program synthesis, compilers, language design, functional programming

Santosh Nagarakatte

formal methods, program analysis, static analysis, compilers, memory management, language design, object-oriented programming, parallel programming, concurrency

Stanford University

Application deadline: December 2nd

Alex Aiken

compilers, language design

Fredrik Kjolstad

compilers, language implementation, language design, parallel programming, concurrency

Stevens Institute of Technology

Eric Koskinen

formal methods, concurrency, program verification, distributed systems

Michael Greenberg

gradual typing, static analysis, compilers, functional programming, formal methods

TUPL @ Tufts University

Guannan Wei

type systems, program analysis, program verification, compilers, metaprogramming

Jeffrey S. Foster

program analysis, static analysis, program synthesis, compilers, language-based security, formal methods

Univ. of California - Berkeley

Application deadline: December 1st

Max Willsey

e-graphs, automated reasoning, program analysis, compilers, logic programming

Sarah E. Chasins

program synthesis, compilers

Univ. of California - Davis

Caleb Stanford

formal methods, distributed systems, security, regular expressions, dataflow programming, program verification

Univ. of California - Los Angeles

Application deadline: December 15th

Guoqing Harry Xu

static analysis, compilers, object-oriented programming, distributed systems, formal methods

Jens Palsberg

compilers, language design, quantum computing, quantum programming

Konstantinos Kallas

static analysis, compilers, distributed systems

Todd D. Millstein

type systems, program verification, automated reasoning, interactive theorem provers, property-based testing, probabilistic programming

Yisu Remy Wang

equality saturation, query optimization, databases, Datalog, program synthesis

Univ. of California - Riverside

Jay P. Lim

compilers, numerical computing, correctly-rounded math libraries, language design

Manu Sridharan

static analysis, software engineering, program reliability, software maintenance

ProgSys @ Univ. of California - San Diego

Application deadline: December 23rd

Deian Stefan

refinement types, program analysis, compilers, language implementation, language design, functional programming, language-based security, memory management

Loris D'Antoni

static analysis, program synthesis, compilers, language-based security, formal methods

Michael J. Coblenz

type systems, formal methods, static analysis, memory management, language design, functional programming, property-based testing

Nadia Polikarpova

refinement types, separation logic, program analysis, program synthesis, compilers, functional programming, object-oriented programming, language-based security, formal methods

Ranjit Jhala

refinement types, model checking, program analysis, compilers

Univ. of California - Santa Barbara

Application deadline: December 15th

Ben Hardekopf

program analysis, static analysis, formal verification, security, hardware design, CS education, language design

Yu Feng

program synthesis, type theory, constraint solving, formal verification, zero-knowledge proofs, compilers, smart contracts, security, program analysis

Univ. of California - Santa Cruz

Application deadline: January 5

Cormac Flanagan

refinement types, gradual typing, model checking, program analysis, language design, concurrency, language-based security, formal methods

Lindsey Kuper

distributed systems, choreographic programming, refinement types, dependent types, concurrency, causal consistency, formal verification, functional programming, Rust

Mohsen Lesani

distributed systems, program synthesis, formal verification, domain-specific languages, type systems, concurrency, memory models, RDMA, smart contracts, program analysis

Tyler Sorensen

heterogeneous architectures, memory models, operational semantics, axiomatic semantics, empirical testing, model checking, auto-tuning, domain-specific languages

Univ. of Illinois at Urbana-Champaign

Application deadline: December 15th

Charith Mendis

compilers, language semantics, compiler verification, ML compilers

Gagandeep Singh

formal methods, trustworthy AI, program synthesis, software verification

Grigore Rosu

static analysis, language design

Mahesh Viswanathan

algorithms, automata theory, logic, software verification

P. Madhusudan

software verification, trustworthy AI, program synthesis, logic

Sasa Misailovic

probabilistic programming, compilers, trustworthy AI, program synthesis

Talia Ringer

type theory, formal methods, automated reasoning, proof assistants, compilers, interactive theorem provers, dependent types, Rocq

William S. Moses

compilers, scientific computing, parallel programming, HPC

PLUM @ Univ. of Maryland - College Park

Application deadline: December 5th

David Van Horn

gradual typing, automated reasoning, program analysis, static analysis, program synthesis, Racket

Leonidas Lampropoulos

property-based testing, functional programming, type systems, type theory

Milijana Surbatovich

formal methods, systems

University at Buffalo

Andrew K. Hirsch

language design, language implementation, choreographic programming

Harrison Goldstein

metaprogramming, property-based testing, probabilistic programming

Lukasz Ziarek

language design, compilers, runtime systems, concurrency, software engineering

Qianchuan Ye

type theory, program verification, proof assistants, language-based security

University of Chicago

Application deadline: December 11

John H. Reppy

language design, language implementation, parallel programming

Ravi Chugh

HCI, live programming, domain specific languages, functional programming

Robert Rand

type systems, formal methods, program analysis, quantum computing, quantum programming

Shan Lu

program analysis, software verification, systems

CUPLV @ University of Colorado Boulder

Application deadline: December 15th

Bor-Yuh Evan Chang

automated reasoning, static analysis, program verification, software engineering

Gowtham Kaki

dependent types, program synthesis, language design, domain specific languages, functional programming, concurrency, distributed systems

University of Connecticut

Application deadline: January 1st

Stefan K. Muller

language design, type systems, static resource analysis, parallel programming

CLC @ University of Iowa

Application deadline: January 1st

J. Garrett Morris

type systems, substructural types, qualified types, concurrency, records and variants

University of Massachusetts Lowell

Matteo Cimini

formal methods, type systems, gradual typing, interactive theorem provers, concurrency

Paul Downen

language semantics, language design, language implementation

MPLSE @ University of Michigan

Application deadline: December 15th

Cyrus Omar

proof assistants, live programming, functional programming, HCI

Max S. New

language semantics, gradual typing, interoperability, category theory, compiler intermediate languages

Xinyu Wang

program synthesis, query optimization, databases, web automation, formal methods

PLClub @ University of Pennsylvania

Application deadline: Decmeber 15th

Benjamin C. Pierce

type systems, type theory, property-based testing, interactive theorem provers

Mayur Naik

program verification, program analysis, program synthesis, language design

Michael Hicks

security, fuzzing, property-based testing, domain-specific languages, quantum computing, compiler verification, Rust, information flow, type systems

Stephanie Weirich

type systems, dependent types

Steve Zdancewic

linear types, automated reasoning, program synthesis, compilers, functional programming, type theory

University of Southern California

Application deadline: December 15th

Mukund Raghothaman

automated reasoning, program analysis, static analysis, program synthesis, domain specific languages

University of Texas at Austin

Application deadline: December 15th

Isil Dillig

type systems, automated reasoning, program synthesis, domain specific languages

CPU @ University of Utah

Application deadline: December 15th

Ben Greenman

gradual typing, language design, formal methods, HCI

John Regehr

compiler optimization, software testing, formal verification, LLVM, random testing

Matthew Flatt

Racket, macro systems, language extensibility, module systems, language runtimes

Pavel Panchekha

memory management

PLSE @ University of Washington

Application deadline: December 15th

Dan Grossman

program analysis, program synthesis, compilers

Zachary Tatlock

formal methods, compilers

madPL @ University of Wisconsin - Madison

Application deadline: December 15th

Adithya Murali

program verification, program synthesis

Aws Albarghouthi

program synthesis, compilers, program verification, quantum computing

Charles Yuan

quantum computing, quantum programming

Ethan Cecchetti

type theory, language-based security, information-control flow, choreographic programming, language design

Thomas W. Reps

everything apparently

Yale University

Application deadline: December 15th

Alexander K. Lew

probabilistic programming, differentiable programming, Bayesian inference, machine learning

Ruzica Piskac

program verification, security, automated reasoning, program synthesis

Zhong Shao

program verification, compilers, language design, concurrency, language-based security, formal methods