Bridging Curry and Church's typing style

There are two versions of type assignment in the λ  -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, λx:A.xλx:A.x is the identity function on type A  , and it has type A→AA→A but not B→BB→B for a type B different from A  . In Curry-style typing, λx.xλx.x is a general identity function with type C→CC→C for every type C. In this paper, we will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style without losing any typing information. We will also prove a kind of conservative extension result for this interpretation, a result which implies that for most consistent PTSs of the Church-style, the corresponding Curry-style system is consistent. We will then show how to interpret in a system of the Church-style (a modified PTS, stronger than a PTS) every PTS-like system in the Curry style.