By Jean-Yves Girard,
translated and with appendices by
Paul Taylor
and Yves Lafont.
Based on a short graduate course on typed lambda-calculus given at
the Université Paris VII in the autumn term of 1986-7.
Published by Cambridge University Press
(Cambridge Tracts in Theoretical Computer Science, 7), ISBN 0 521 37181 3;
first published 1989, reprinted with corrections 1990.
By the way, Paul translated it and Yves did the LATEX, not vice versa!
Yves also chose the notation, making it consistent through the book.
Here is the story of how the translation came about: Jean-Yves had
mentioned the notes to Paul at a conference, who obtained them and
took them to read on the train on a visit to his parents. But then he
went down with 'flu. As this was his only reading material and his
French wasn't very good, he started writing out a translation.
He later showed this to Yves, who was then his office-mate. It became
a book because of the enthusiasm of Yves and of Samson Abramsky.
As the book is now out of print, we have provided it on-line in
various formats:
