Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!strath-cs!cs.glasgow.ac.uk!wadler
From: wadler@cs.glasgow.ac.uk (Philip Wadler)
Newsgroups: comp.lang.functional
Subject: Re: System F
Message-ID: <5923@vanuata.cs.glasgow.ac.uk>
Date: 30 Jul 90 12:18:45 GMT
References: <3477@goanna.cs.rmit.oz.au>
Reply-To: wadler@cs.glasgow.ac.uk (Philip Wadler)
Organization: Comp Sci, Glasgow Univ, Scotland
Lines: 20

In article <3477@goanna.cs.rmit.oz.au> ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe) writes:
>There's a paper "The system F of variable types, 15 years later"
>by Jean-Yves Girard ... Is there are much
>simpler explanation of this stuff anywhere?

Two handy references:

J.-Y.\ Girard, Y. Lafont, and P. Taylor,
{\em Proofs and Types}.
Cambridge University Press, 1989.

J. C. Reynolds,
Three approaches to type structure.
In {\em Mathematical Foundations of Software Development},
LNCS 185, Springer-Verlag, 1985.

The Reynold's paper is perhaps the best introduction to type
theory for computer scientists in existence.  Girard's book provides
a more thorough introduction to System F and related systems, including
strong normalisation and coherrence semantics.  - Phil