From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6670 Path: news.gmane.org!not-for-mail From: soloviev@irit.fr Newsgroups: gmane.science.mathematics.categories Subject: Re: Re: the Church-Howard Correspondence Date: Fri, 6 May 2011 18:57:03 +0200 (CEST) Message-ID: References: Reply-To: soloviev@irit.fr NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain;charset=utf-8 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1304801072 15672 80.91.229.12 (7 May 2011 20:44:32 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Sat, 7 May 2011 20:44:32 +0000 (UTC) Cc: "Vasili I. Galchin" , "Categories mailing list" To: "Philip Scott" Original-X-From: majordomo@mlist.mta.ca Sat May 07 22:44:26 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 1QIoMR-00066F-Hu for gsmc-categories@m.gmane.org; Sat, 07 May 2011 22:44:23 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:37078) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1QIoKR-0000O1-3A; Sat, 07 May 2011 17:42:19 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1QIoKN-0001Y2-H4 for categories-list@mlist.mta.ca; Sat, 07 May 2011 17:42:15 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6670 Archived-At: 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 i= n 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/ ]