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
a weasel in a hat blog twitter youtube icon youtube twitch icon twitch google scholar icon google scholar dblp icon dblp github icon github sigplan researchr icon researchr orcid icon orcid

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 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.

Teaching

SemesterCourses
S2021 CS 105 (w/ Prof. Birrell)
CS 190
F2020 CS 054 (archived)
CS 190 (archived)
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 105 Tue 9-11am PT Zoom
CS 105 Fri 1:30-3pm PT Zoom

I can be reached via email to schedule meetings on Zoom, Skype, or telephone. I am also on Zulip for my respective courses.

Materials

Research

Venue Paper (see a complete list)
In submission Solver-based Gradual Type Migration Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha
In submission Gradual Algebraic Datatypes Stefan Malewski, Michael Greenberg, and Éric Tanter
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
(MIT)		 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