Re: Re: the Church-Howard Correspondence

[soloviev@irit.fr]

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