* Re: the Church-Howard Correspondence
@ 2011-05-04 15:27 Vasili I. Galchin
2011-05-05 13:47 ` Philip Scott
0 siblings, 1 reply; 3+ messages in thread
From: Vasili I. Galchin @ 2011-05-04 15:27 UTC (permalink / raw)
To: Categories mailing list
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/ ]
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: the Church-Howard Correspondence 2011-05-04 15:27 the Church-Howard Correspondence Vasili I. Galchin @ 2011-05-05 13:47 ` Philip Scott 2011-05-06 16:57 ` soloviev 0 siblings, 1 reply; 3+ messages in thread From: Philip Scott @ 2011-05-05 13:47 UTC (permalink / raw) To: Vasili I. Galchin; +Cc: Categories mailing list 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/ ] ^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: Re: the Church-Howard Correspondence 2011-05-05 13:47 ` Philip Scott @ 2011-05-06 16:57 ` soloviev 0 siblings, 0 replies; 3+ messages in thread From: soloviev @ 2011-05-06 16:57 UTC (permalink / raw) To: Philip Scott; +Cc: Vasili I. Galchin, Categories mailing list Hi, I would like to add, that in lesser detail (not like in the handbook-style presentation in Lambek and Scott), but sufficient for technical applications it was described and systematically used in the papers of Grigori Mints (who was then my adviser) and my own: G. Mints. Closed Categories and the Theory of Proofs. J. of Soviet Mathematics, 15, 1, 45-62, 1982. http://www.springerlink.com/content/l84428791771mx2u/ Gregorii E. Mints. Proof theory and category theory. In Selected Papers in Proof Theory, chapter 10, pages 183-212. Bibliopolis/North-IIolland, 1992. (Russian version - 1979.) [Babaev and Soloviev, 1979] A.A. Babaev and S.V. Soloviev. A coherence theorem for canonical maps in cartesian closed categories. Zapisiki Nauchnykh SeminaTvv LOMI, 88, 1979. Russian with English summary. English translation appears in J. of Soviet Math., 20, 1982. S. V. Solov'ev. Journal of Mathematical Sciences Volume 22, Number 3, 1387-1400, 1983. DOI: 10.1007/BF01084396 The category of finite sets and Cartesian closed categories http://www.springerlink.com/content/rg33151k36414064/ All the best Sergei Soloviev > 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 > [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2011-05-06 16:57 UTC | newest] Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2011-05-04 15:27 the Church-Howard Correspondence Vasili I. Galchin 2011-05-05 13:47 ` Philip Scott 2011-05-06 16:57 ` soloviev
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).