Michael Greenberg (mgreenbe)

Michael Greenberg

Assistant Professor

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

Department of Computer Science

Gateway Center S447
(201) 216-5332
Website

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.

Institutional Service

  • DEI Committee Member
  • DEI Committee Chair
  • TT Hiring Committee Member

Professional Service

  • PaSh Technical Steering Committee (2021-) Member
  • PLDI PC member
  • POPL Steering Committee Member (2021-2024)
  • ACM SIGPLAN ICFP PC member
  • IFIP 2.16 Working Group on Language Design Local Chair/Organizer
  • 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)

Professional Societies

  • ACM SIGOPS Member

Selected Publications

Book

  1. Greenberg, M. (2023). Logical Foundations (Vol I) and Programming Languages Foundations (Vol II). Software Foundations. University of Pennsylvania.
    https://softwarefoundations.cis.upenn.edu/.

Conference Proceeding

  1. Liargkovas, G.; Kallas, K.; Greenberg, M.; Vasilakis, N. (2023). Executing Shell Scripts in the Wrong Order, Correctly. Proceedings of the 19th Workshop on Hot Topics in Operating Systems. ACM.
    https://doi.org/10.1145%2F3593856.3595891.
  2. Bembenek, A.; Greenberg, M.; Chong, S.; Alviano, M.; Pieris, A. (2022). Formulog: Datalog + SMT + FP. Proceedings of the 4th International Workshop on the Resurgence of Datalog in Academia and Industry (Datalog-2.0 2022) co-located with the 16th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2022), Genova-Nervi, Italy, September 5, 2022 (vol. 3203, pp. 48--53). CEUR-WS.org.
    http://ceur-ws.org/Vol-3203/short2.pdf.
  3. Vazou, N.; Greenberg, M.; Polikarpova, N. (2022). How to safely use extensionality in Liquid Haskell. Haskell '22: 15th ACM SIGPLAN International Haskell Symposium, Ljubljana, Slovenia, September 15 - 16, 2022 (pp. 13--26). ACM.
    https://doi.org/10.1145/3546189.3549919.
  4. Greenberg, M.; Beckett, R.; Campbell, E. H.; Jhala, R.; Dillig, I. (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.
  5. Kallas, K.; Mustafa, T.; Bielak, J.; Karnikis, D.; Dang, T. H.; Greenberg, M.; Vasilakis, N.; Aguilera, M. K.; Weatherspoon, H. (2022). Practically Correct, Just-in-Time Shell Script Parallelization. 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022 (pp. 769--785). USENIX Association.
    https://www.usenix.org/conference/osdi22/presentation/kallas.
  6. 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.
  7. Greenberg, M.; Kallas, K.; Vasilakis, N.; Angel, S.; Kasikci, B.; Kohler, E. (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.
  8. Greenberg, M.; Kallas, K.; Vasilakis, N. (2021). Unix shell programming. Proceedings of the Workshop on Hot Topics in Operating Systems. ACM.
    https://doi.org/10.1145%2F3458336.3465294.
  9. Greenberg, M.; Lerner, B. S.; Rastislav Bod\'\ik; Krishnamurthi, S. (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.
  10. Greenberg, M.; Marr, S.; Sartor, J. B. (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.
  11. Arashloo, M. T.; Koral, Y.; Greenberg, M.; Rexford, J.; Walker, D.; Barcellos, M. P.; Crowcroft, J.; Vahdat, A.; Katti, S. (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.
  12. Beckett, R.; Greenberg, M.; Walker, D.; Krintz, C.; Berger, E. 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.
  13. Greenberg, M.; Fisher, K.; Walker, D.; Ball, T.; Rastislav Bod\'\ik; Krishnamurthi, S.; Lerner, B. S.; Morrisett, G. (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.
  14. Schlesinger, C.; Greenberg, M.; Walker, D.; Jeuring, J.; Chakravarty, M. M. (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.
  15. 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.
  16. Johannes Borgstr\"om; Gordon, A. D.; Greenberg, M.; Margetson, J.; Van Gael, J.; Barthe, G. (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.
  17. Jo\~ao Filipe Belo; Greenberg, M.; Igarashi, A.; Pierce, B. C.; Barthe, G. (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.
  18. Greenberg, M.; Pierce, B. C.; Weirich, S.; Hermenegildo, M. V.; Palsberg, J. (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.
  19. Barbosa, D. M.; Cretin, J.; Foster, N.; Greenberg, M.; Pierce, B. C.; Hudak, P.; Weirich, S. (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.
  20. Meyerovich, L. A.; Guha, A.; Baskin, J. P.; Cooper, G. H.; Greenberg, M.; Bromfield, A.; Krishnamurthi, S.; Arora, S.; Leavens, G. T. (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.
  21. Mary F. Fern\'andez; Fisher, K.; Foster, J. N.; Greenberg, M.; Mandelbaum, Y.; Hudak, P.; Warren, D. S. (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.
  22. Krishnamurthi, S.; Fisler, K.; Greenberg, M.; Taylor, R. N.; Dwyer, M. B. (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. Bembenek, A.; Greenberg, M.; Chong, S. (2023). From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems. Proceedings of the ACM on Programming Languages (POPL ed., vol. 7, pp. 185--217). Association for Computing Machinery (ACM).
    https://doi.org/10.1145%2F3571200.
  2. Cassano, F.; Gouwar, J.; Nguyen, D.; Nguyen, S.; Phipps-Costin, L.; Pinckney, D.; Yee, M. H.; Zi, Y.; Anderson, C. J.; Feldman, M. Q.; Guha, A.; Greenberg, M.; Jangda, A. (2022). A Scalable and Extensible Approach to Benchmarking NL2Code for 18 Programming Languages. CoRR (vol. abs/2208.08227).
    https://doi.org/10.48550/arXiv.2208.08227.
  3. Vazou, N.; Greenberg, M. (2021). Functional Extensionality for Refinement Types. CoRR (vol. abs/2103.02177).
    https://arxiv.org/abs/2103.02177.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  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. (2020). Executable formal semantics for the POSIX shell. Proceedings of the ACM on Programming Languages (POPL ed., vol. 4, pp. 1--30). Association for Computing Machinery (ACM).
    https://doi.org/10.1145%2F3371111.
  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