Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!cs.utexas.edu!samsung!munnari.oz.au!goanna!ok
From: ok@goanna.cs.rmit.oz.au (Richard A. O'Keefe)
Newsgroups: comp.lang.functional
Subject: System F
Message-ID: <3477@goanna.cs.rmit.oz.au>
Date: 28 Jul 90 10:19:01 GMT
Organization: Comp Sci, RMIT, Melbourne, Australia
Lines: 27

I recently bough a copy of
	Logical Foundations of Functional Programming
	ed. Gerard Huet
	Addison-Wesley 1990
	ISBN 0-201-17234-8
which is one of the Austin "Year of Programming" series.
There's a paper in the "The system F of variable types, 15 years later"
by Jean-Yves Girard, and J.C.Reynolds' introduction to that section says
that it's essentially the same second-order typed lambda calculus that
he came up with.  In Reynolds' introduction, he says that
	- every expression describes a termination computation
	- every function from natural numbers to natural numbers
	  which can be proved total using second-order arithmetic
	  is expressible in it
This is all very interesting.  The trouble is that while I would like
to know more about it, Girard's article requires rather more category
theory than I can remember in order to read it.  Is there are much
simpler explanation of this stuff anywhere?

Huet, in the preface, speaks of "toning down category theory, at least
in the title, in order not to discourage practically minded computer
scientists with too much abstract intellectual terrorism".  I wish he
_hadn't_ toned down the title; then I might have known what I was in for.

-- 
Science is all about asking the right questions.  | ok@goanna.cs.rmit.oz.au
I'm afraid you just asked one of the wrong ones.  | (quote from Playfair)