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

[George Cherevichenko]

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