From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6665 Path: news.gmane.org!not-for-mail From: "Vasili I. Galchin" Newsgroups: gmane.science.mathematics.categories Subject: Re: the Church-Howard Correspondence Date: Wed, 4 May 2011 10:27:07 -0500 Message-ID: Reply-To: "Vasili I. Galchin" NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1304537093 30304 80.91.229.12 (4 May 2011 19:24:53 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 4 May 2011 19:24:53 +0000 (UTC) To: Categories mailing list Original-X-From: majordomo@mlist.mta.ca Wed May 04 21:24:48 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.4]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1QHhgj-0000Yr-PF for gsmc-categories@m.gmane.org; Wed, 04 May 2011 21:24:45 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:33198) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1QHhcW-0008FI-Q6; Wed, 04 May 2011 16:20:24 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1QHhcU-0006hw-8c for categories-list@mlist.mta.ca; Wed, 04 May 2011 16:20:22 -0300 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6665 Archived-At: 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 wro= te: > Hello, > > =A0 =A0 =A0I 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/ ]