After thinking about my English, please let me add to my previous posting. I believe the author of the paper is proving an equivalence of an informal notion (Curry-Howard "Isomorphism) with a formal mathematical notion (the equivalence of categories). Regards, Vasili On Tue, May 3, 2011 at 4:18 PM, Vasili I. Galchin <vigalchin@gmail.com> wrote:
Hello,
I started reading a paper www.math.uchicago.edu/~may/VIGRE/VIGRE2010/REUPapers/Berger.pdf entitled "A Categorical Approach to Proofs-As-Programs" by Carson Berger. He seems to be giving a formal equivalence of the various sides of this famous Correspondence using equivalence of categories. Have any members of this forum read this paper and if so, what significance do you give this paper?
Thank you,
Vasili
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]