CS 789 THEORY SEMINAR [home]

Speaker:  Dexter Kozen  
Affiliation:  Cornell University
Date:       Monday, 4pm, September 6, 2004
Place:       5130 Upson Hall
Title:       Toward the Automation of Category Theory

Abstract: 

Since its invention in 1945 by Samuel Eilenberg and Saunders Mac Lane, category theory has had a profound impact in many areas of mathematics and computer science. Unfortunately, many basic category-theoretic facts, although easy to state, can be quite tedious to verify formally.

For example, consider the well-known fact that the category Cat of (small) categories is cartesian-closed, or more generally, that there exists a natural isomorphism of functor categories

Fun[CxD,E] == Fun[C,Fun[D,E]].

This statement is deceptively concise in that it contains a huge amount of compressed information. A complete formal verification by hand would be quite onerous due to the enormous number of low-level details that must be checked. This task is not very interesting, and one would like to automate as much of it as possible.

In print, authors often do not bother to provide formal details of the constructions that establish such basic facts, let alone proofs of correctness. Those arguments that are explicitly given are typically expressed in terms of commuting diagrams, and verification amounts to visual arrow chasing. This is adequate for humans, but does not lend itself well to automation.

In this talk I will introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. I will describe the system and illustrate its use by showing pieces of a complete formal proof of the above isomorphism. I will also pose several interesting open questions regarding implementation, proof theory, and complexity of the system.