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

see a complete list of 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

Reasoning About Paths in the Interface Graph Michael Greenberg

--popl-2023

From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Aaron Bembenek, Michael Greenberg, and Stephen Chong

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

Files-as-Filesystems for POSIX Shell Data Processing Michael Greenberg

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

The Dynamic Practice and Static Theory of Gradual Typing Michael Greenberg

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

CS 284-A Data Structures

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

--smoosh

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

--ffs

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

--pash

light-touch data-parallel shell scripting

correct and automatic parallelization of shell scripts; a source-to-source compiler with a lightweight runtime

--kmt

Kleene Modulo Theories

a framework for deriving sound, complete, and decidable instances of Kleene Algebras with Tests (KATs)

--formulog

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

--sf

Software Foundations

a textbook introducing logical principles and PL concepts using the Coq interactive theorem prover

--security

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

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.