Michael Greenberg

Assistant Professor Department of Computer Science Pomona College
a picture of me, michael greenberg
Office: Edmunds 225
Phone: 909-607-4554
Zoom: 797-068-5800
Skype: michael.m.greenberg

I study programming languages. I am interested in foundations, both theoretical and practical. My research has focused on strengthening the guarantees on offer at the “easy and automatic” end of the spectrum.

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

I work in a variety of other areas: contracts, a flexible form of runtime verification for higher-order programming languages; and software-defined networking, a recent development that allows for straightforward centralized control of computer networks.


F2020 CS 054
CS 190
S2020 CS 054 (archived) (w/ Prof. Osborn)
CS 181-N (archived)
F2019 On leave
S2019 On leave
F2018 On leave
S2018 CS 131 (archived)
CS 54 (archived)
F2017 CS 131 (archived)
CS 190 (archived)
S2017 CS 55 (archived)
CS 131 (archived)
F2016 CS 131 (archived)
CS 190 (archived)
S2016 CS 51 (w/ Profs. Chen, Kampe, and Wu)
CS 181-N Software Foundations (archived)
F2015 CS 51 (w/ Profs. Chen, Kampe, and Wu)
CS 131 (archived)
Office hours
Course Day Time Location
CS 054 Tue 4–5pm Seaver Commons 104
CS 181-N Wed 10am–noon Edmunds 225
CS 054 Wed 2–5pm Edmunds 225
CS 181-N Thu 11am–noon Millikan 1249

Office hours are in flux as we pivot to video. I am available by appointment. I can be reached via email to schedule meetings on Zoom, Skype, or telephone.



Venue Paper (see a complete list)
In submission Functional Extensionality for Refinement Types Niki Vazou and Michael Greenberg
In submission Kleene Algebras Modulo Theories Ryan Beckett, Eric Campbell, and Michael Greenberg
OOPSLA 2020 Formulog: Datalog for SMT-based Static Analysis Aaron Bembenek, Michael Greenberg, and Stephen Chong
ICLP 2020
(ext. abs.)
Datalog-Based Systems Can Use Incremental SMT Solving Aaron Bembenek, Michael Ballantyne, Michael Greenberg, and Nada Amin
POPL 2020 Executable formal semantics for the POSIX shell Michael Greenberg and Austin J. Blatt
WGT 2020 Gradual Algebraic Data Types Michael Greenberg, Stefan Malewski, and Éric Tanter
SNAPL 2019 The Dynamic Practice and Static Theory of Gradual Typing Michael Greenberg
CoqPL 2019 Teaching Discrete Mathematics to Early Undergraduates with Software Foundations Michael Greenberg and Joseph C. Osborn
DSLDI 2018 The POSIX shell is an interactive DSL for concurrency Michael Greenberg
PX 2018 Word expansion supports POSIX shell interactivity Michael Greenberg
TOPLAS 2017 Polymorphic Manifest Contracts, Revised and Resolved Taro Sekiyama, Astushi Igarashi, Michael Greenberg
OBT 2017 Understanding the POSIX Shell as a Programming Language Michael Greenberg
TFP 2016 Space-Efficient Latent Contracts Michael Greenberg
SIGCOMM 2016 SNAP: Stateful Network-Wide Abstractions for Packet Processing Mina Tahmasbi Arashloo, Yaron Koral, Michael Greenberg, Jennifer Rexford, and David Walker
PLDI 2016 Temporal NetKAT Ryan Beckett, Michael Greenberg, David Walker
... complete list ...
Student theses
Year Student Title
2019 Teddy Katz
Verified Compilation of Abstract Network Policies
(with Adam Chlipala)
2018 Austin Blatt Mechanized Semantics for Word Expansion in the POSIX Shell
2017 Eric Campbell Infiniteness and Linear Temporal Logic

Other news and activities