Michael Greenberg (mgreenbe)

Michael Greenberg

Assistant Professor

Charles V. Schaefer, Jr. School of Engineering and Science

Computer Science

Education

  • PhD (2013) University of Pennsylvania (Computer and Information Science)
  • BA (2007) Brown University (Computer science)
  • BA (2007) Brown University (Egyptology)

Research

Michael's research focuses on directly applying formalism to practical problems. Much of his work takes place in the emerging field of semantics engineering, where he scales PL techniques up to work on real systems.

His primary focus is on improving the POSIX shell and building tools to support it and its ecosystem, but he works in a variety of other areas, too: 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.

Experience

Michael received BAs in Computer Science and Egyptology from Brown University (2007) and his PhD in Computer Science from the University of Pennsylvania (2013); previously, he was an assistant professor at Pomona College. His work ranges from functional-reactive JavaScript (with Shriram Krishnamurthi at Brown) to runtime verification of higher-order programs (with Benjamin Pierce at Penn) to software-defined networking (with Dave Walker at Princeton) to present activities focused on the POSIX shell and executable formalism.

Professional Service

  • PaSh Technical Steering Committee (2021-) Member
  • POPL Steering Committee Member (2021-2024)
  • POPL 2023 Program committee member
  • DLS 2022 Program committee member
  • NJPLS Spring 2022 Organizer and program chair
  • PADL 2022 Program committee member

Honors and Awards

Distinguished Paper Award (Kleene Algebras Modulo Theories at PLDI 2022)
Most Influential Paper Award (Flapjax, from OOPSLA 2009, awarded 2019)
Best Student Paper Award (Flapjax, from OOPSLA 2009)

Selected Publications

Conference Proceeding

  1. Greenberg, M.; Beckett, R.; Campbell, E. H. (2022). Kleene algebra modulo theories: a framework for concrete KATs. PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022 (pp. 594--608). ACM.
    https://doi.org/10.1145/3519939.3523722.
  2. Kallas, K.; Mustafa, T.; Bielak, J.; Karnikis, D.; Dang, T. H.; Vasilakis, N.; Greenberg, M.. Practically Correct, Just-in-Time Shell Script Parallelizaton. OSDI. Usenix.
    https://www.usenix.org/conference/osdi22/presentation/kallas.
  3. Greenberg, M. (2021). Files-as-Filesystems for POSIX Shell Data Processing. PLOS '21: Proceedings of the 11th Workshop on Programming Languages and Operating Systems, Virtual Event, Germany, October 25, 2021 (pp. 17--23). ACM.
    https://doi.org/10.1145/3477113.3487265.
  4. Greenberg, M.; Kallas, K.; Vasilakis, N. (2021). The future of the shell: Unix and beyond. HotOS '21: Workshop on Hot Topics in Operating Systems, Ann Arbor, Michigan, USA, June, 1-3, 2021 (pp. 240--241). ACM.
    https://doi.org/10.1145/3458336.3465296.
  5. Greenberg, M.; Kallas, K.; Vasilakis, N. (2021). Unix shell programming: the next 50 years. HotOS '21: Workshop on Hot Topics in Operating Systems, Ann Arbor, Michigan, USA, June, 1-3, 2021 (pp. 104--111). ACM.
    https://doi.org/10.1145/3458336.3465294.
  6. Greenberg, M. (2019). The Dynamic Practice and Static Theory of Gradual Typing. 3rd Summit on Advances in Programming Languages, SNAPL 2019, May 16-17, 2019, Providence, RI, USA (vol. 136, pp. 6:1--6:20). Schloss Dagstuhl - Leibniz-Zentrum f\"ur Informatik.
    https://doi.org/10.4230/LIPIcs.SNAPL.2019.6.
  7. Greenberg, M. (2018). Word expansion supports POSIX shell interactivity. Conference Companion of the 2nd International Conference on Art, Science, and Engineering of Programming, Nice, France, April 09-12, 2018 (pp. 153--160). ACM.
    https://doi.org/10.1145/3191697.3214336.
  8. Arashloo, M. T.; Koral, Y.; Greenberg, M.; Rexford, J.; Walker, D. (2016). SNAP: Stateful Network-Wide Abstractions for Packet Processing. Proceedings of the ACM SIGCOMM 2016 Conference, Florianopolis, Brazil, August 22-26, 2016 (pp. 29--43). ACM.
    https://doi.org/10.1145/2934872.2934892.
  9. Greenberg, M. (2016). Space-Efficient Latent Contracts. Trends in Functional Programming - 17th International Conference, TFP 2016, College Park, MD, USA, June 8-10, 2016, Revised Selected Papers (vol. 10447, pp. 3--23). Springer.
    https://doi.org/10.1007/978-3-030-14805-8/_1.
  10. Beckett, R.; Greenberg, M.; Walker, D. (2016). Temporal NetKAT. Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016 (pp. 386--401). ACM.
    https://doi.org/10.1145/2908080.2908108.
  11. Greenberg, M.; Rajamani, S. K.; Walker, D. (2015). Space-Efficient Manifest Contracts. Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015 (pp. 181--194). ACM.
    https://doi.org/10.1145/2676726.2676967.
  12. Greenberg, M.; Fisher, K.; Walker, D. (2015). Tracking the Flow of Ideas through the Programming Languages Literature. 1st Summit on Advances in Programming Languages, SNAPL 2015, May 3-6, 2015, Asilomar, California, USA (vol. 32, pp. 140--155). Schloss Dagstuhl - Leibniz-Zentrum f\"ur Informatik.
    https://doi.org/10.4230/LIPIcs.SNAPL.2015.140.
  13. Schlesinger, C.; Greenberg, M.; Walker, D. (2014). Concurrent NetCore: from policies to pipelines. Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014 (pp. 11--24). ACM.
    https://doi.org/10.1145/2628136.2628157.
  14. Hritcu, C.; Greenberg, M.; Karel, B.; Pierce, B. C.; Morrisett, G. (2013). All Your IFCException Are Belong to Us. 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2013 (pp. 3--17). IEEE Computer Society.
    https://doi.org/10.1109/SP.2013.10.
  15. Johannes Borgstr\"om; Gordon, A. D.; Greenberg, M.; Margetson, J.; Van Gael, J. (2011). Measure Transformer Semantics for Bayesian Machine Learning. Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\"ucken, Germany, March 26-April 3, 2011. Proceedings (vol. 6602, pp. 77--96). Springer.
    https://doi.org/10.1007/978-3-642-19718-5/_5.
  16. Jo\~ao Filipe Belo; Greenberg, M.; Igarashi, A.; Pierce, B. C. (2011). Polymorphic Contracts. Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\"ucken, Germany, March 26-April 3, 2011. Proceedings (vol. 6602, pp. 18--37). Springer.
    https://doi.org/10.1007/978-3-642-19718-5/_2.
  17. Greenberg, M.; Pierce, B. C.; Weirich, S. (2010). Contracts made manifest. Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010 (pp. 353--364). ACM.
    https://doi.org/10.1145/1706299.1706341.
  18. Barbosa, D. M.; Cretin, J.; Foster, N.; Greenberg, M.; Pierce, B. C. (2010). Matching lenses: alignment and view update. Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 (pp. 193--204). ACM.
    https://doi.org/10.1145/1863543.1863572.
  19. Meyerovich, L. A.; Guha, A.; Baskin, J. P.; Cooper, G. H.; Greenberg, M.; Bromfield, A.; Krishnamurthi, S. (2009). Flapjax: a programming language for Ajax applications. Proceedings of the 24th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009, October 25-29, 2009, Orlando, Florida, USA (pp. 1--20). ACM.
    https://doi.org/10.1145/1640089.1640091.
  20. Mary F. Fern\'andez; Fisher, K.; Foster, J. N.; Greenberg, M.; Mandelbaum, Y. (2008). A Generic Programming Toolkit for PADS/ML: First-Class Upgrades for Third-Party Developers. Practical Aspects of Declarative Languages, 10th International Symposium, PADL 2008, San Francisco, CA, USA, January 7-8, 2008 (vol. 4902, pp. 133--149). Springer.
    https://doi.org/10.1007/978-3-540-77442-6/_10.
  21. Krishnamurthi, S.; Fisler, K.; Greenberg, M. (2004). Verifying aspect advice modularly. Proceedings of the 12th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2004, Newport Beach, CA, USA, October 31 - November 6, 2004 (pp. 137--146). ACM.
    https://doi.org/10.1145/1029894.1029916.

Journal Article

  1. Vazou, N.; Greenberg, M. (2021). Functional Extensionality for Refinement Types. CoRR (vol. abs/2103.02177).
    https://arxiv.org/abs/2103.02177.
  2. Malewski, S.; Greenberg, M.; \'Eric Tanter (2021). Gradually structured data. Proc. ACM Program. Lang. (OOPSLA ed., vol. 5, pp. 1--29).
    https://doi.org/10.1145/3485503.
  3. Campbell, E. H.; Greenberg, M. (2021). Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic. CoRR (vol. abs/2107.06045).
    https://arxiv.org/abs/2107.06045.
  4. Greenberg, M.; Kallas, K.; Vasilakis, N.; Kell, S. (2021). Report on the "The Future of the Shell" Panel at HotOS 2021. CoRR (vol. abs/2109.11016).
    https://arxiv.org/abs/2109.11016.
  5. Phipps-Costin, L.; Anderson, C. J.; Greenberg, M.; Guha, A. (2021). Solver-based Gradual Type Migration. CoRR (vol. abs/2109.05049).
    https://arxiv.org/abs/2109.05049.
  6. Phipps-Costin, L.; Anderson, C. J.; Greenberg, M.; Guha, A. (2021). Solver-based gradual type migration. Proc. ACM Program. Lang. (OOPSLA ed., vol. 5, pp. 1--27).
    https://doi.org/10.1145/3485488.
  7. Greenberg, M.; Blatt, A. J. (2020). Executable formal semantics for the POSIX shell. Proc. ACM Program. Lang. (POPL ed., vol. 4, pp. 43:1--43:30).
    https://doi.org/10.1145/3371111.
  8. Bembenek, A.; Greenberg, M.; Chong, S. (2020). Formulog: Datalog for SMT-based static analysis. Proc. ACM Program. Lang. (OOPSLA ed., vol. 4, pp. 141:1--141:31).
    https://doi.org/10.1145/3428209.
  9. Bembenek, A.; Greenberg, M.; Chong, S. (2020). Formulog: Datalog for SMT-Based Static Analysis (Extended Version). CoRR (vol. abs/2009.08361).
    https://arxiv.org/abs/2009.08361.
  10. Greenberg, M.; Blatt, A. J. (2019). Executable formal semantics for the POSIX shell. CoRR (vol. abs/1907.05308).
    http://arxiv.org/abs/1907.05308.
  11. Beckett, R.; Campbell, E. H.; Greenberg, M. (2017). Kleene Algebra Modulo Theories. CoRR (vol. abs/1707.02894).
    http://arxiv.org/abs/1707.02894.
  12. Sekiyama, T.; Igarashi, A.; Greenberg, M. (2017). Polymorphic Manifest Contracts, Revised and Resolved. ACM Trans. Program. Lang. Syst. (1 ed., vol. 39, pp. 3:1--3:36).
    https://doi.org/10.1145/2994594.
  13. Greenberg, M. (2016). Space-Efficient Latent Contracts. CoRR (vol. abs/1604.02474).
    http://arxiv.org/abs/1604.02474.
  14. Arashloo, M. T.; Koral, Y.; Greenberg, M.; Rexford, J.; Walker, D. (2015). SNAP: Stateful Network-Wide Abstractions for Packet Processing. CoRR (vol. abs/1512.00822).
    http://arxiv.org/abs/1512.00822.
  15. Greenberg, M. (2014). Space-Efficient Manifest Contracts. CoRR (vol. abs/1410.2813).
    http://arxiv.org/abs/1410.2813.
  16. Johannes Borgstr\"om; Gordon, A. D.; Greenberg, M.; Margetson, J.; Van Gael, J. (2013). Measure Transformer Semantics for Bayesian Machine Learning. Log. Methods Comput. Sci. (3 ed., vol. 9).
    https://doi.org/10.2168/LMCS-9(3:11)2013.
  17. Greenberg, M.; Pierce, B. C.; Weirich, S. (2012). Contracts made manifest. J. Funct. Program. (3 ed., vol. 22, pp. 225--274).
    https://doi.org/10.1017/S0956796812000135.

Courses

Spring 2022: CS 284 Data Structures
Fall 2021: CS 515 Fundamentals of Computing