Re: the Church-Howard Correspondence

[Philip Scott <phil@site.uottawa.ca>]

Dear Vasili:  The author doesn't refer to, nor even seem to know about, my book with J. Lambek,
Introduction to Higher-Order Categorical Logic, J. Lambek and P. J. Scott, 
Cambridge Univ. Press, 1986, where all this was done in  great detail. 

In fact, the three way correspondence between categories of deductive systems,  of
cartesian closed categories, and of typed lambda calculi (which the author wishes
to explain) was first done there, with many applications.


 							Best,
   							Phil Scott



On 2011-05-04, at 4:27 PM, Vasili I. Galchin wrote:

> 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/ ]



[For admin and other information see: http://www.mta.ca/~cat-dist/ ]