Speaker
J. Garrett Morris, Assistant Professor, Department of Computer Science at the University of Iowa

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, their connection to Church's initial account of computation, and (time permitting) the subsequent generalization of quantifiers giving dependent types. 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.

Learn more about
J. Garrett Morris