9 March 2004

2:30 - 4:00   J. Seldin
Relating Church-style Typing and Curry-style Typing: Preliminary Report

Abstract: There are two versions of type assignment in $\lambda$-calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called ``domain free''), in which it is not. As an example, in Church-style typing, $\lambda x : A . x$ is the identity function on type A, and it has type $A \rightarrow A$ but not $B \rightarrow B$ for a type $B$ different from $A$. In Curry-style typing, $\lambda x . x$ is a general identity function with type $C \rightarrow C$ for \emph{every} type $C$.
In this talk, I will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style. (This generalizes some unpublished work with Garrel Pottinger.) I will then show how to interpret in a system of the Church-style (a modified PTS) every PTS-like system in the Curry style.