[sci.logic] info on category theory and type theory

raymond@cs.ruu.nl (Raymond Hoofman) (06/13/91)

In <1991Jun12.173237.4944@informatik.uni-ulm.de> ruess@theorie.informatik.uni-ulm.de (Harald Ruess) writes:

>Are there any good introductory books, reports, lecture
>notes etc. out there relating category theory with
>type theory. Once more, I'm looking for introductory
>but non-trivial material.

I would recommend the following book:

J. Lambek and P.J. Scott
"Introduction to higher order categorical logic"
Cambridge studies in advanced mathematics 7
Cambridge University press 1988
-- 
----------------------------------------------------------------------------
| Raymond Hoofman       |            "Love without pain is like            |
| raymond@cs.ruu.nl     |             pain without love."                  |
----------------------------------------------------------------------------

mueck@unipas.fmi.uni-passau.de (Andreas Mueck) (06/14/91)

In article <1991Jun12.173237.4944@informatik.uni-ulm.de> ruess@theorie.informatik.uni-ulm.de (Harald Ruess) writes:
>Are there any good introductory books, reports, lecture
>notes etc. out there relating category theory with
>type theory. Once more, I'm looking for introductory
>but non-trivial material.
>
>Harald Ruess

On type theory I can recommend you the book "Proofs and Types" from Girard J.Y.,
Taylor P. and Lafont Y (Cambridge Tracts in Theoretical Computer Science).

   ..... andy mueck
         mueck@unipas.fmi.uni-passau.de
         p.o. box 2540
         d-8390 passau
             frg
         phone: ++49 851 509 353
         fax:   ++49 851 509 497