| CARVIEW |
NAME
Michael Greenberg -- assistant professor of computer scienceSYNOPSIS
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
For a full list of publications, see mgreenbe.papers(5).
TEACHING
CS 525-A Systems 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
bringing PL tools to bear on the shell and its ecosystem; visualize the POSIX shell language using the shtepper or parse dash using libdash
work with semi-structured data (like JSON) using conventional shell tools; a userspace filesystem for mounting files in tree-/semi-structured formats
a tool that uses overlayfs and namespaces to let you contain and inspect the effects of destructive commands before committing them to your system---or not
correct and automatic parallelization of shell scripts; a source-to-source compiler with a lightweight runtime
a framework for deriving sound, complete, and decidable instances of Kleene Algebras with Tests (KATs)
Formulog is a language for expressing PL concepts: Datalog defines inductive relations; functional programming yields helper functions; SMT provides logical reasoning
a textbook introducing logical principles and PL concepts using the Coq interactive theorem prover
a talk about how to give a good talk. i blogged about it and wrote about it on the SIGPLAN blog
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).
AUTHOR
I can be reached at michael@greenberg.science. I'm in Gateway Academic Center South (GS), office 447.