Summary: Type Theory text/reference
I recently posted the following question to the types list:
Can anyone recommend a good graduate-level introduction to type
theory, suitable for reference & self-study? I will be looking
into extensions of ML's typing system from both theoretical and
practical perspectives. I would appreciate anything that would
work as a handbook and reference to the issues, techniques, and
results of type theory in general. All the better if it applies
these to ML in particular.
Replies came from James Powers and Roger Hindley; their repies
follow. I believe there may have been another reply or two that were
lost in my email system; if so, please accept my apologies (and I am
still interested in your response).
David Schmidt graciously provided a draft copy of his book
``The Structure of Typed Programming Languages,'' forthcoming from
MIT Press. It looks to be very useful.
Thanks also to Philip Wadler, the moderator, who directly answered
several other questions and put me in touch with David Schmidt.
>From James Power (James.Power@compapp.dcu.ie)
The book I'd choose would be:
Type Theory and Functional Programming
By Simon Thompson, Addison-Wesley 1991
Despite its title, there's not really a whole lot of functional programming
in here, but the type theory isn't bad at all.
Another book worth taking a look at would be:
Constructive Foundations for Functional Languages
by Raymond Turner (McGraw-Hill, 1991)
There's a lot more \lambda calculus in Turner's book; I find it slightly
Specifically on ML-ish type systems, the following might be worth a look,
but don't expect *too* much type theory:
Semantics of Programming Languages
by Carl A. Gunter (MIT 1992)
And for some general papers:
Logical Foundations of Functional Programming
ed. Gerard Huet (Addison-Wesley, 1989)
>From Roger Hindley (email@example.com)
Actually I'm writing one now, on the basic arrow-type
simple type theory! But unfortunately it won't be finished for
another 11 months, so it isn't much help to you.
There's a good one by Krivine in French,
"Lambda-Calcul, Types et Modeles", publ. by Masson.
Other possibly useful titles:
Barendregt, H.P.  Lambda calculi with types, in Handbook of
Logic in Computer Science, Vol.2, ed. S. Abramsky et al., Clarendon
Press, Oxford, England 1992, pp. 118-309.
Constable, R. L.  Type theory as a foundation for computer
science, Lecture Notes in Computer Science, Springer Verlag, 526
Odifreddi, P.  (editor) Logic and Computer Science, Academic
Press (Series APIC Studies in Data Processing No. 31).