[Prev][Next][Index][Thread]

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.

  --dwight tuinstra
    tuinstra@sun.mcs.clarkson.edu

======================================================================
>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
  ISBN: 0-201-41667-0

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)
  ISBN: 0-077-07411-4

There's a lot more \lambda calculus in Turner's book; I find it slightly 
more difficult!

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)
  ISBN: 0-262-07143-6

And for some general papers:

  Logical Foundations of Functional Programming
  ed. Gerard Huet (Addison-Wesley, 1989)
  ISBN: 0-201-17234-8

=======================================================================
>From Roger Hindley (majrh@pyramid.swansea.ac.uk)

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. [1992] 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. [1991] Type theory as a foundation for computer
science, Lecture Notes in Computer Science, Springer Verlag, 526
(1991), 226-243.

Odifreddi, P. [1990] (editor) Logic and Computer Science, Academic
Press (Series APIC Studies in Data Processing No. 31).

============================================================================