Events Calendar

Speaker

Garrett Morris

Abstract

This talk will introduce my research on programming languages, exemplified by some recent results on modularity and extensible data types. My research into programming languages and their type systems is guided by two overarching goals. On the one hand, types should precisely specify program behavior, allowing programmers to rule out classes of erroneous behavior. On the other, types should enable expressive tools, allowing programmers to build modular, re-usable software and software components. My work inhabits the intersection of these ideas, refining generic programming mechanisms both to better enforce intended program behavior and to support more expressive abstractions.

Extensibility is an evergreen problem in programming and programming language design. The goal is simple: specifications of programs and their data should support the addition of both new kinds of data and new operations on data. Despite this problem having been identified as early as 1975, modern languages lack effective solutions. Object-oriented languages require programmers to adopt unintuitive patterns like visitors, while functional languages rely on encodings of data types. Lower-level languages, where similar problems arise, rely on textual substitution. I will present recent work which proposes a unified approach to extensible data and program specification. I will show how this work both encompasses existing approaches to extensible data types and captures examples inexpressible in all existing systems. Our approach naturally generalizes, providing a single account of extensible objects, effects, and bit-level specifications.

Bio

J. Garrett Morris is an assistant professor and the inaugural Emeriti-Faculty Scholar in the Department of Computer Science at the University of Iowa. He received his PhD from Portland State University in Oregon, and post-doctoral training at the University of Edinburgh, Scotland. His research focuses on the development of type systems for higher-order functional programming languages, with the twin aims of improving expressiveness and modularity in high-level programming and supporting safe concurrent, low-level, and effectful programming. His work has appeared in top venues in programming language theory and functional programming, and is supported by NSF.