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=Wednesdays, 2–4pm on Zoom
mgreenbe --papers=all


My research focuses on directly applying formalism to practical problems with usable tools. 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 it and its ecosystem.

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.


Executing Shell Scripts in the Wrong Order, Correctly Georgios Liargkovas, Konstantinos Kallas, Michael Greenberg, Nikos Vasilakis
Towards a Translation from Liquid Haskell to Coq Lykourgos Mastorou, Niki Vazou, Michael Greenberg
A Scalable and Extensible Approach to Benchmarking NL2Code for 18 Programming Languages Federico Cassano, John Gouwar, Daniel Nguyen, Sydney Nguyen, Luna Phipps-Costin, Donald Pinckney, Ming Ho Yee, Yangtian Zi, Carolyn Jane Anderson, Molly Q Feldman, Arjun Guha, Michael Greenberg, Abhinav Jangda
Formulog: Datalog + SMT + FP Aaron Bembenek, Michael Greenberg, and Stephen Chong
How to Safely Use Extensionality in Liquid Haskell Niki Vazou and Michael Greenberg
Practically Correct, Just-in-Time Shell Script Parallelization Konstantinos Kallas, Tammam Mustafa, Jan Bielak, Dimitris Karnikis, Thurston H.Y. Dang, Michael Greenberg, and Nikos Vasilakis
Kleene Algebra Modulo Theories Michael Greenberg, Ryan Beckett and Eric Campbell
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
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-A Fundamentals of Computing
CS 525-A Systems Programming
CS 515-A Fundamentals of Computing
CS 515-A Fundamentals of Computing
CS 515 Fundamentals of Computing
CS 515 Fundamentals of Computing
archived course websites from pomona college
CS 054 Discrete Math and Functional Programming
F2020, S2020, S2018
CS 055 Discrete Math
CS 105 Computer Systems
CS 131 Programming Languages
S0218, F2017, S2017, F2016, F2015
CS 181-N Special Topics
S2020 (Functional Programming), S2016 (Software Foundations)
CS 190 Senior Seminar (readings focused on social issues)
S2021, F2020, F2017, F2016

Please feel free to steal these materials for your own courses! If you do use these materials, please let me know; I like to know what others find useful, and I appreciate feedback.


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.

Here is how to pronounce my name.


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