Title: Proofs and Programs

Abstract:

The Curry-Howard correspondence is one of (if not the) most significant foundational result in the study of programming languages and logics.

At its most fundamental, the Curry-Howard correspondence describes a deep connection between (predicative intuitionistic) logic with (simply-typed functional) programming: logical propositions are types, proofs of those propositions are functions inhabiting those types, and simplification of those proofs is evaluation of the corresponding functions. In this way, Curry-Howard gives one answer to the intuitionist challenge that mathematical statements should correspond to concrete truth conditions.

The power of Curry-Howard is not in a single connection, however, but in the template that it establishes for further propositions-as-types correspondences. Quantification is connected to dependent typing, giving both powerful tools for describing mathematical theories and for stating and proving program correctness. The treatment of assumptions in proofs is connected to the use of resources in programs, leading to principled approaches to resource management like Rust's ideas of ownership and borrowing. Generalizing the ideas of "and" and "or", and their relationship, has a strong connection to models of concurrent and parallel programming. And there are many more.

This talk will give a high-level introduction to the Curry-Howard correspondence, assuming a minimal background in either logic or programming languages. I'll describe the foundational concerns in logic, the generalization of quantifiers to give dependent types, and how this laid the framework for modern approaches to interactive theorem proving. While the talk itself will be retrospective, it also describes the foundation for a just-beginning project here to develop a new propositions-as-types correspondence between generic programming, which abstracts over the structure of data, and theory reuse and extension in mathematics, and indeed in logic itself.

Short 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 Ph.D. 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.

If you want add or delete your email from our mailing list on future announcements of colloquiums, send your request to math-colloquium@uiowa.edu