mgreenblog

posts by category about this blog

I'm looking for PhD students!

I'm looking for PhD students in the Fall 2021 application cycle, to start in Fall 2022. Come work with me at Stevens CS in Hoboken, NJ!

I work in Gateway South (the left-hand side of this photo). You could, too! (Photo credit: Stevens Alumni.)

What will we work on?

I'm interested in applying formalism --- all those pretty Greek letters in program semantics, type systems, and static analysis --- directly to real systems --- all that nitty gritty code that makes these beautiful, horrible machines do their thing. I'm working on a few projects that variously emphasize theoretical or practical aspects. My main goal these days is to provide better support for the POSIX shell and its ecosystem, but here's a sampling from recent papers:

  • Smoosh (POPL 2020): I'm interested in improving and supporting the shell. Smoosh is a formal model of the POSIX shell that can be executed and passes the POSIX test suite. Continuing work on Smoosh means hacking in Lem, OCaml, and Coq (and maybe Rust or C or JS or Elm), and thinking about virtualization, symbolic execution, fuzzing, and how specifications and implementations interact. Or maybe it just means building cool tools for the POSIX world!
  • Formulog (OOPSLA 2020): Datalog, functional programming, and SMT combine to let you write down and run things that look a lot like your formal spec. Continuing work in this line means hacking in Rust (and maybe C++ or Java), and thinking about SMT and how we can be confident that the formalism we write is the code that we run---and that our code is efficient.
  • Gradual types (OOPSLA 2021) and type migration (OOPSLA 2021): People have been trying to combine the benefits of dynamic and static types for years. Work in this line will mean hacking in Rust (and maybe JS or TS or Haskell) and doing classic PL stuff like type soundness, type inference, and proofs of contextual equivalence (by logical relations or bisimulation, on paper or in Coq).

A slide from a Keynote deck. The title is "semantics engineering". The left-hand side illustrates systems challenges: a "C" monster, complicated specs, a dog in front of a laptop (programming is hard!) The right-hand side illustrates PL formalism: inference rules, helper functions, grammars, etc.

I've been calling this combination of executable systems and PL formalism "semantics engineering", with inspiration from the PLT folks (though I don't really use Redex).

You can check out a list of all my papers. Are any of these papers the sort of thing you'd like to write? Come join me for a PhD!

Who will you work with?

Stevens has about thirty research faculty, and we're growing fast. We have a great group of people interested in PL, security, and systems: Eduardo Bonelli, Tegan Brennan, Dominic Duggan, Eric Koskinen, Philippe Meunier, David Naumann, Georgios Portokalidis, Susanne Wetzel, and Jun Xu. And there are of course many other fantastic researchers in other topics to learn from in class and collaborate with on research. And beyond all that, I got a lot out of my internships (AT&T Shannon Labs; MSR Cambridge), and I encourage my students to find stimulating opportunities.

Where is Hoboken, again?

Hoboken, NJ is directly across the Hudson River from Manhattan a/k/a New York City. There's 24-hour train service and frequent ferries to and from New York. Hoboken is a vision zero city, where it's safe and comfortable to bike and walk. There are other cool cities nearby, like Jersey City.

How do you apply?

You can learn more about the CS PhD program at Stevens and apply online. If you have questions, please don't hesitate to get in touch.