MGREENBE(1) Assistant Professor @ Stevens CS MGREENBE(1)
a picture of me, michael greenberg


Michael Greenberg -- assistant professor of computer science


mgreenbe --office=Gateway Academic Center South, office 447
mgreenbe --office-hours=Thursday, 2–4pm on Zoom


My research focuses on directly applying formalism to practical problems. Much of my work takes place in the emerging field of semantics engineering, where I scale PL techniques up to work on real systems.

My primary focus is on improving the POSIX shell and building tools to support its use.

I work in a variety of other areas: contracts and gradual types; tools for directly expressing PL formalism, using logic programming and SMT solving; and foundational semantics for decidable languages, like Kleene algebra with tests.


Functional Extensionality for Refinement Types Niki Vazou and Michael Greenberg
Solver-based Gradual Type Migration Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha
Gradually Structured Data Stefan Malewski, Michael Greenberg, and Éric Tanter
Kleene Algebra Modulo Theories Michael Greenberg, Ryan Beckett and Eric Campbell
Report on the “The Future of the Shell” Panel at HotOS 2021 Michael Greenberg, Konstantinos Kallas, Nikos Vasilakis, and Stephen Kell
Unix Shell Programming: The Next 50 Years Michael Greenberg, Konstantinos Kallas, and Nikos Vasilakis
Formulog: Datalog for SMT-based Static Analysis Aaron Bembenek, Michael Greenberg, and Stephen Chong
Datalog-Based Systems Can Use Incremental SMT Solving Aaron Bembenek, Michael Ballantyne, Michael Greenberg, and Nada Amin
Executable formal semantics for the POSIX shell Michael Greenberg and Austin J. Blatt

For a full list of publications, see mgreenbe.papers(5).


CS 515 — Fundamentals of Computing
archived course websites from pomona college
CS 054 F2020, S2020, S2018 CS 055 S2017 CS 105 S2021 CS 131 S0218, F2017, S2017, F2016, F2015 CS 181-N S2020 (FP), S2016 (SF) CS 190 S2021, F2020, F2017, F2016


the symbolic, mechanized, observable, operational shell

bringing PL tools to bear on the shell and its ecosystem; visualize the POSIX shell language using the shtepper or parse dash using libdash

the file filesystem

work with semi-structured data (like JSON) using conventional shell tools; a userspace filesystem for mounting files in tree-/semi-structured formats

light-touch data-parallel shell scripting

correct and automatic parallelization of shell scripts; a source-to-source compiler with a lightweight runtime

Kleene Modulo Theories

a framework for deriving sound, complete, and decidable instances of Kleene Algebras with Tests (KATs)

Formulog = Datalog + Functional Programming + SMT

Formulog is a language for expressing PL concepts: Datalog defines inductive relations; functional programming yields helper functions; SMT provides logical reasoning

Software Foundations

a textbook introducing logical principles and PL concepts using the Coq interactive theorem prover

computer security in the face of a hostile government

a talk for non-CS people about how to defend digital identities; check out my security checklist



I got a BA in Computer Science and Egyptology from Brown University (2007) and a PhD in Computer and Information Science from the University of Pennsylvania (2013). I did a postdoc with Dave Walker at Princeton (2013–2015), after which I was an assistant professor at Pomona College (2015–2021) before moving to Stevens Institute of Technology (2021). I visited Steve Chong in a scholarly way at Harvard University (2018–2019).


You can find my old website at Pomona College.


I can be reached at I'm in Gateway Academic Center South (GS), office 447.