Research Interests

I study the foundations of programming: how we construct programs and how we reason about them. My thesis is that advances in type systems empower programmers to create better-written, better-understood programs.  More precise type systems better characterize program behavior. For example, I have studied the use of substructural type systems to guarantee lock freedom in concurrent programs. More expressive type systems enable powerful, generic abstractions. For example, I have studied the use of qualified types to capture a uniform description of a variety of methods for composing records, variants, and program modules. These advances form a virtuous cycle. More precise types enable better abstractions, while expressive abstractions make precise type systems easy to use.

I am a co-director of the Computational Logic Center with Professors Aaron Stump, Cesare Tinelli, and Omar Chowdhury.

Recent Publications

• Mark Jones, J. Garrett Morris, and Richard Eisenberg. "Partial Type Constructors; Or, Making ad hoc datatypes less ad hoc". Proc. ACM Program. Lang., 4, POPL (January 2020). [dl.acm.org/doi/10.1145/3371108]
• J. Garrett Morris and James McKinna. "Abstracting Extensible Data Types; Or, Rows By Any Other Name." Proc. ACM Program. Lang., 3, POPL (January 2019). [doi.org/10.1145/3290325]
• Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. "Exceptional Asynchronous Session Types: Session Types without Tiers." Proc. ACM Program. Lang., 3, POPL (January 2019). [doi.org/10.1145/3290341]
• Jack Williams, J. Garrett Morris and Philip Wadler. "The Root Cause of Blame: Contracts for Intersection and Union Types". Proc. ACM Prog. Lang. 2, OOPSLA (October 2018). [doi.org/10.1145/3276504]
• J. Garrett Morris and Richard A. Eisenberg. "Constrained Type Families". Proc. ACM Prog. Lang. 1, ICFP, Article 42 (September 2017). [doi.org/10.1145/3110286]
• J. Garrett Morris. "The Best of Both Worlds: Linear Functional Programming Without Compromise". In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, Japan, 2016. [doi.org/10.1145/2951913.2951925]
• Sam Lindley and J. Garrett Morris. "Talking Bananas: Structural Recursion for Session Types". In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Nara, Japan, 2016. [doi.org/10.1145/2951913.2951921]
• Sam Lindley and J. Garrett Morris. “A Semantics for Propositions as Sessions.” In ESOP 2015. Lecture Notes in Computer Science, vol 9032. Springer, Berlin, Heidelberg.  2015. [doi.org/10.1007/978-3-662-46669-8_23]
• J. Garrett Morris and Mark P. Jones. "Instance Chains: Type Class Programming Without Overlapping Instances." In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming (ICFP '10), Baltimore, Maryland. 2010. [doi.org/10.1145/1863543.1863596]