Article View: comp.lang.functional
Article #406Re: System F
From: Philip Wadler
Date: Mon, 30 Jul 1990 12:18
Date: Mon, 30 Jul 1990 12:18
20 lines
1236 bytes
1236 bytes
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
Technical Details
Message-ID:
<5923@vanuata.cs.glasgow.ac.uk>Path:
arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!uunet!mcsun!ukc!strath-cs!cs.glasgow.ac.uk!wadlerReferences:
<3477@goanna.cs.rmit.oz.au>Show Full Headers
Complete Article Headers
Path: arc1-ca.pugleaf.net!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