README.md

PL Grad Schools

Finding grad schools that fit your interests can be a daunting task. Rather than making a ranking of the 'best' grad schools using some subjective metric, we decided to list out grad schools with professors studying PL that are open to take new students.

Feel free to make a PR adding other schools/faculty/topics to the list. Or remove them if the PL faculty are no longer there. We want this to be a living list of active PL schools for new students/postdocs/etc.

• LogSem @ Aarhus University

  • Topics
    • Logic
    • Type Theory
    • Language base security
    • Formal verification
    • Model checking
  • Faculty
    • Aslan Askarov
    • Lars Birkedal
    • Jaco van de Pol
    • Bas Spitters

• Australian National University

  • Topics
    • Program verification
    • Security
    • Logic for computer science
    • Memory management
    • Language runtimes
  • Faculty
    • Jeremy Dawson
    • Alwen Tiu
    • Steve Blackburn
    • Tony Hosking
    • Dirk Pattinson
    • Michael Norrish

• PLT @ Brown University

  • Topics
    • PL applied to education
    • Metaprogramming
    • Programming environments
    • Tested semantics
    • Applied model theory
  • Faculty
    • Shriram Krishnamurthi
    • Tim Nelson
    • Kathi Fisler

• POP @ Carnegie Mellon University

  • Topics
    • Logic
    • Type Theory
    • Functional programming
  • Faculty
    • Robert Harper
    • Frank Pfenning
    • Jan Hoffmann
    • Karl Crary

• PL @ Cornell University

  • Topics
    • Architecture / Heterogeneous Computing
    • Networking
    • Constructive Type Theory (NuPRL)
    • Typed Assembly Languages
    • Kleene Algebra with Tests
    • Information Flow Control systems
    • Security
    • Privacy aware programming Languages
    • Distributed Computing
  • Faculty
    • Nate Foster
    • Adrian Sampson
    • Robert Constable
    • Dexter Kozen
    • Owolabi Legunsen
    • Greg Morrisett
    • Andrew Myers
    • Fred Schneider

• Indiana University

  • Topics
    • Gradual Typing

• Computer Software Group @ Kyoto University

  • Topics
    • Object-oriented programming
    • Gradual typing
    • Automated program verification
  • Faculty
    • Atsushi Igarashi
    • Kohei Suenaga

• RSS @ Universidade de Lisboa

  • Topics
    • Session Types
    • Program Synthesis
    • PL for ML
  • Faculty
    • Vasco Vasconcelos
    • Alcides Fonseca
    • Andreia Mordido

• Massachusetts Institute of Technology

  • Topics
    • DeepSpec
    • Program synthesis
    • Software engineering

• McMaster University

  • Topics
    • Dependently typed programming
    • Typed functional programming
    • DSLs for many purposes
    • Languages for programming mathematics
    • Software Engineering
  • Faculty
    • Jacques Carette
    • Wolfram Kahl
    • Richard Paige
    • William Farmer

• POEM @ North Carolina State University

  • Topics
    • Logic programming
    • Typed functional programming
    • Logical frameworks/dependent type systems
    • Substructural and modal logics
    • Structure editors
    • Applied language design for interactive virtual agents, virtual worlds, simulation, and procedural content generation
  • Faculty
    • Chris Martens

• PRL @ Northeastern University

  • Topics
    • Gradual Typing
    • Verified Compilation
    • Language Oriented Programming
    • Concurrent Programming Models
  • Faculty
    • Matthias Felleisen
    • Amal Ahmed
    • Jan Vitek
    • Frank Tip

• Princeton University

  • Topics
    • DeepSpec
    • Verified Compilers
    • Networking
    • Program Analysis
    • Formal Verification
  • Faculty
    • Andrew Appel
    • Aarti Gupta
    • Zachary Kincaid
    • David Walker

• PurPL @ Purdue University

  • Topics
    • Language Design
    • Security
    • Compilers
    • Verification
    • Program Synthesis
    • Program Analysis
    • Formal Verification
    • Distributed Systems
    • Software Engineering
  • Faculty
    • Benjamin Delaware
    • Tiark Rompf
    • Roopsha Samantha
    • Milind Kulkarni
    • Suresh Jagannathan
    • Xiangyu Zhang

• PLASMA @ UMass

  • Topics
    • Applied PL
    • Software Engineering
    • Systems
  • Faculty
    • Emery Berger
    • Arjun Guha
    • Yuriy Brun

• Maple @ University of Alberta

  • Topics
    • Scalable Program Analysis
    • Security Analysis Tools
    • Energy-Efficient Software Systems
    • Just-In-Time Compilers
    • Applications of Symbolic Execution in Machine Learning
    • Type Systems
  • Faculty
    • Karim Ali

• University of British Columbia

  • Topics
    • Gradual Typing
    • Multi-stage Programming
    • Typestate-oriented programming
    • Verified Compilation
    • Dependent Types
    • Aspect-oriented programming
    • Programming Language MOOCs
  • Faculty
    • Ron Garcia
    • William Bowman

• CLC @ University of Iowa

  • Topics
    • First-order Theorem Proving
    • Model Checking and Verification
    • Programming Languages Theory
    • Privacy
    • Proof Checking
    • Satisfiability Modulo Theories
    • Security
    • Verified Programming
  • Faculty
    • Aaron Stump
    • Cesare Tinelli
    • Omar Chowdhury

• McGill University

  • Topics
    • Logical Frameworks
    • Higher-order Abstract Syntax
  • Faculty
    • Brigitte Pientka
    • Prakash Panangaden
    • Clark Verbrugge

• Queen's University

  • Topics
    • Type systems
    • Gradual typing
    • Incremental computation
  • Faculty
    • Jana Dunfield

• Tohoku University

  • Topics
    • Functional programming languages
    • Bidirectional Programming
    • Partial evaluation
    • Program verification
  • Faculty
    • Eijiro Sumii
    • Kazutaka Matsuda
    • Oleg Kiselyov
    • Atsushi Ohori
    • Keisuke Nakano

• Tufts University

  • Topics
    • Domain specific languages
    • Program synthesis
    • Functional programming
    • Type systems
    • Security
    • Garbage collection
    • Static analysis
  • Faculty
    • Kathleen Fisher
    • Samuel Guyer
    • Norman Ramsey
    • Jeff Foster

• Theory Group @ University of Birmingham

  • Topics
    • Topology and domain theory
    • Homotopy type theory and constructive mathematics
    • Semantics of effects
    • Higher category theory
    • String diagrams and graphical calculi
    • Quantum computation
    • Proof theory and computational complexity

• University of California, Santa Cruz

  • Topics
    • Language support for distributed and decentralized systems
    • Language-based security; information flow
    • Concurrency
  • Faculty
    • Owen Arden
    • Cormac Flanagan
    • Lindsey Kuper
    • Tyler Sorensen (starting fall '20)

• University of California, Riverside

  • Topics

    • Verification and synthesis for distributed computing.
    • Compiler and architectural support for parallel systems.
    • Scalable static analysis techniques.

  • Faculty

    • Rajiv Gupta
    • Mohsen Lesani
    • Manu Sridharan
    • Zhijia Zhao

  • Research Groups

    • RIPLE (Riverside Programming Languages and Software Engineering).

• LFCS @ University of Edinburgh

  • Topics
    • Logic
    • Type Theory

• PL Group @ University of Hong Kong

  • Topics
    • Type systems
    • Functional programming
    • Object-oriented programming
  • Faculty
    • Bruno C. d. S. Oliveira

• Hong Kong University of Science and Technology

  • Topics
    • Type systems
    • Functional programming
    • Compiler optimization
    • Domain-specific languages
  • Faculty
    • Lionel Parreaux

• PLAS @ University of Kent (Programming Languages and Systems)

  • Topics
    • Logic and Type theory
    • Semantics
    • Verification
    • Programming language design
    • Compilation
    • Runtime systems
  • Faculty
    • 16 faculty members, see website.

• FP @ University of Nottingham

  • Topics
    • Logic
    • Type Theory

• PLUM @ University of Maryland

  • Topics
    • Functional programming
    • Probabilistic programming
    • Program analysis
    • Quantum computing
    • Security
    • Testing
    • Type systems
    • Verification
  • Faculty
    • Mike Hicks
    • David Van Horn

• MPLSE @ University of Michigan

  • Topics
    • Programming environments / PL + HCI
    • Functional programming
    • Type systems
    • Program analysis
    • Program synthesis
    • Gradual Typing
    • Category Theory
    • Verification
    • Formal methods
    • Software Engineering
  • Faculty
    • Jean-Baptiste Jeannin
    • Max New
    • Cyrus Omar
    • Xinyu Wang
    • Manos Kapritsos
    • Yatin Manerkar
    • Satish Narayanaswamy
    • Stephen Oney
    • Karem A. Sakallah
    • Westley Weimer

• University of Pennsylvania

  • Topics
    • DeepSpec

• MSP @ University of Strathclyde

  • Topics
    • Logic
    • Type Theory

• CPU @ University of Utah

  • Topics
    • compiler optimization
    • verification, testing, formal methods
    • PL design & implementation
    • gradual typing
  • Faculty
    • Eric Eide
    • Matthew Flatt
    • Ganesh Gopalakrishnan
    • Ben Greenman
    • Mary Hall
    • Pavel Panchekha
    • Zvonimir Rakamaric
    • John Regehr
    • Saday Sadayappan

• PLAID @ University of Vermont

  • Topics
    • Privacy
    • Program Analysis
    • Security
    • Type Systems
    • Verification
  • Faculty
    • David Darais
    • Joe Near
    • Christian Skalka

• PLSE @ University of Washington

  • Topics
    • Applied PL

• PLG @ University of Waterloo

  • Topics
    • Type Systems
    • Program Analysis
    • Concurrency
  • Faculty
    • Werner Dietl
    • Patrick Lam

• Yale University

  • Topics
    • DeepSpec

• University at Buffalo, SUNY

  • Topics
    • Type Systems
    • Compilers
    • Concurrency
    • Language-Based Security
  • Faculty
    • Lukasz Ziarek
    • Andrew K. Hirsch