 |
VOOZH | about |
|
VOOZH | about |
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.
| Semester | Courses |
|---|---|
| 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) |
| 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.
| 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 ... | |
| 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 |
