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@stevens.edu

DESCRIPTION

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

RESEARCH

--all-papers
--in-submission
Functional Extensionality for Refinement Types Niki Vazou and Michael Greenberg
--oopsla-2021a
(cond. acc.)
Solver-based Gradual Type Migration Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha
--oopsla-2021b
(cond. acc.)
Gradual Algebraic Datatypes Stefan Malewski, Michael Greenberg, and Éric Tanter
--arxiv-2021
Kleene Algebra Modulo Theories Michael Greenberg and Ryan Beckett and Eric Campbell
--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

--fall-2021
CS 515 — Fundamentals of Computing
--pomona
archived course websites from pomona college
CS 054 F2020, S2020, S2018 CS 055 S2017 CS 105 S2021 CS 131 S0218, F2017, S2017, F2016, F2015 CS 181-N S2020 (FP), S2016 (SF) CS 190 S2021, F2020, F2017, F2016

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

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

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.

AUTHOR

I can be reached at michael.greenberg@stevens.edu. I'll put my office information here once they tell me what it is. It'll be somewhere in the Gateway Academic Center.

(END)