[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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 <[email protected]> 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
