Date/Time
Date(s) - 28/08/2013
2:00 pm - 3:00 pm
Location
School of Computing Science, Sir Alwyn Williams Building, Lilybank Gardens, University of Glasgow
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. I will also discuss the conditions under which each interpretation can be reversed.
