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

NAME

Michael Greenberg -- assistant professor of computer science

SYNOPSIS

mgreenbe --email=michael@greenberg.science
mgreenbe --office=Gateway Academic Center South, office 447
mgreenbe --office-hours=Wednesdays, 2–4pm on Zoom
mgreenbe --papers=all

DESCRIPTION

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.

RESEARCH

--all-papers
--hotos-2023
Executing Shell Scripts in the Wrong Order, Correctly Georgios Liargkovas, Konstantinos Kallas, Michael Greenberg, Nikos Vasilakis
--types-2023
Towards a Translation from Liquid Haskell to Coq Lykourgos Mastorou, Niki Vazou, Michael Greenberg
--tse-2023
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
--evcs-2023
--popl-2023
--datalog-2022
Formulog: Datalog + SMT + FP Aaron Bembenek, Michael Greenberg, and Stephen Chong
--haskell-2022
How to Safely Use Extensionality in Liquid Haskell Niki Vazou and Michael Greenberg
--osdi-2022
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
--pldi-2022
Kleene Algebra Modulo Theories Michael Greenberg, Ryan Beckett and Eric Campbell
--plos-2021
--oopsla-2021a
Solver-based Gradual Type Migration Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha
--oopsla-2021b
Gradually Structured Data Stefan Malewski, Michael Greenberg, and Éric Tanter
--arxiv-2021
Report on the “The Future of the Shell” Panel at HotOS 2021 Michael Greenberg, Konstantinos Kallas, Nikos Vasilakis, and Stephen Kell
--hotos-2021
Unix Shell Programming: The Next 50 Years Michael Greenberg, Konstantinos Kallas, and Nikos Vasilakis
--oopsla-2020
Formulog: Datalog for SMT-based Static Analysis Aaron Bembenek, Michael Greenberg, and Stephen Chong
--iclp-2020
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
--snapl-2019

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

TEACHING

--spring-2024
CS 515-A Fundamentals of Computing
CS 525-A Systems Programming
--fall-2023
CS 515-A Fundamentals of Computing
--spring-2023
CS 515-A Fundamentals of Computing
--fall-2022
CS 515 Fundamentals of Computing
--spring-2022
--fall-2021
CS 515 Fundamentals of Computing
--pomona
archived course websites from pomona college
CS 054 Discrete Math and Functional Programming
F2020, S2020, S2018
CS 055 Discrete Math
S2017
CS 105 Computer Systems
S2021
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.

MATERIALS

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

SEE ALSO

HISTORY

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

COMPATIBILITY

You can find my old website at Pomona College.

Here is how to pronounce my name.

AUTHOR

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

(END)