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.