[TYPES] Please give me a link. Is alpha-conversion easy or not?

[Sergei Soloviev]

Dear George,

I'd like to cite (for historical reasons) my old paper - it does not
contain the answers to your questions in exactly such terms as you
formulate them (it is of 1981) but is shows how the connection between
lambda-calculus and cartesian closed categories was understood at
this time, and it contains references to even earlier papers.

The papers contains the results later understood as the results about
isomorphism of types, and also a version of "Statman's finite completeness
theorem" obtained independently about the same time.

The paper nowadays is downlodable in .pdf, you can find it
via google (maybe needing institutional subscribtion) - 
I can do it in our university (university of Toulouse-3).

Zap. Nauchn. Sem. LOMI, 1981, Volume 105, Pages 174–194        

The category of finite sets and Cartesian closed categories 

S. V. Solov'ev 

There is English translation (Journal of Soviet Mathematics/J. of Math. Sciences)


Best regards,

Sergei Soloviev
 
 
On Sunday, November 4, 2012 21:43 CET, George Cherevichenko <george.cherevichenko at gmail.com> wrote: 
 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> Hi
> Where can I find a precise description how to interpret typed lambda
> calculi with named variables in cartesian closed categories? Or how to
> interpret lambda calculi with named variables in lambda calculi with De
> Brujn indices? I know how to do that, but I need a link. I need proofs of
> the following facts:
> 1) Alpha-equal terms correspond to the same term with De Brujn indices (or
> the same arrow in CCC).
> 2) Substitutions with named variables correspond to substitutions with De
> Brujn indices.
> I read Altenkirch "Alpha-conversion is easy", should I only refer to this
> article?
> Please, no nominal logic.
> George