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 the 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.
  • 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 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 it 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 something 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, 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.

Heaven, Hell, or Hoboken!

After six years at Pomona College, I’ve moved to Stevens Institute of Technology as an assistant professor in the computer science department. I miss my lovely Pomona colleagues—they’re hiring!—but I’m excited to be on the East Coast and to be doing more research with a new set of lovely colleagues.

A photo of my office nameplate. The Stevens logo in red, with the following text:

Michael Greenberg
Assistant Professor
Department of Computer Science

447 (in Braille)

I’ve got a new webpage, but the old webpage should stay up.

We’ll be spinning up the Stevens PL/systems/security seminar soon, and I’m hopeful we can involve lots of interesting people, as speakers and attendees. If you’re in the New York area, come by and say hi!

Also… I’ll be looking to hire PhD students for the coming year! More info on that soon.

The Dynamic Practice and Static Theory of Gradual Typing

I’ll be presenting my thoughts on the state of gradual typing research—along with some goals and challenges—at SNAPL 2019. Here’s the abstract of my paper, The Dynamic Practice and Static Theory of Gradual Typing:

We can tease apart the research on gradual types into two ‘lineages’: a pragmatic, implementation-oriented dynamic-first lineage and a formal, type-theoretic, static-first lineage. The dynamic-first lineage’s focus is on taming particular idioms—‘pre-existing conditions’ in untyped programming languages. The static-first lineage’s focus is on interoperation and individual type system features, rather than the collection of features found in any particular language. Both appear in programming languages research under the name “gradual typing”, and they are in active conversation with each other.

What are these two lineages? What challenges and opportunities await the static-first lineage? What progress has been made so far?

See you in Providence?