Lambda the Ultimate

inactiveTopic Introduction to (Formal) Type Systems
started 3/10/2004; 9:36:50 PM - last post 3/17/2004; 6:56:53 AM
Matt Estes - Introduction to (Formal) Type Systems  blueArrow
3/10/2004; 9:36:50 PM (reads: 285, responses: 9)
I am a graduate student in Mathematics right now, and have recently gotten interested in the formal theories of type systems. I have tried to search for a readable introduction on the net, and I have found a few books on programming languages, but I have yet to find anything that explains a good solid formal theory of "typing" in programming languages.

I am aware that such things exist, but I'm poor, and so is our library(which is why I haven't got Pierce's "Types and Programming Languages"), and so far my net searches haven't turned up anything, maybe its because I don't know the right key words, although it seems like when I do find the right words, I get something that I assumes I already have a Ph.D in the topic(which I'm not opposed to getting, I'm just not there yet).

andrew cooke - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 6:25:08 AM (reads: 251, responses: 0)
there used to be a draft of a text by pierce available on the net. is it still around anywhere?

parts of this book may be useful -

also, see the earlier posts on introductions category theory, if you don't know that (i guess you do).

andrew cooke - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 6:31:02 AM (reads: 246, responses: 0)
there's probably useful stuff here too - (presumably frank would know what to recommend).

Neel Krishnaswami - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 8:41:55 AM (reads: 238, responses: 1)
Hi Matt, I think the best introductory paper on the subject is Wright and Felleisen's A Syntactic Approach to Type Soundness. The prerequisite knowledge you need is how to read proofs by structural induction.

Ehud Lamm - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 10:26:35 AM (reads: 230, responses: 0)
I second this recommendation.

Ehud Lamm - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 10:54:16 AM (reads: 223, responses: 0)
I am not sure just how formal you want to be. Take a look at Luca Cardelli's papers.

For a deeper understanding you might want to start by reading about the simply type lambda calculus and its relationship with proof theory.

Matt Estes - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 11:04:39 AM (reads: 223, responses: 1)
I want to see how far down the rabbit hole goes. Thanks for the suggestions so far, they'll make good Spring Break reading :). I've been programming a while, and at times a lot of things seem so arbitrary and ad-hoc, it really bugs me. Since I'm doing my Masters degree in Mathematics, I'm getting the tools needed to understand really formal stuff, and I want to know why some type systems are better than others, or why some systems are more workable than others. I can appreciate intuition and personal experience, but a good formal theory can justify those experiences, so I want to see the theory, or at least know that the lack of a cohesive theory is the problem(with a language). :)

Ehud Lamm - Re: Introduction to (Formal) Type Systems  blueArrow
3/11/2004; 1:26:21 PM (reads: 225, responses: 0)
Given this background, I'd suggesting taking a look at Girard's book.

Frank Atanassow - Re: Introduction to (Formal) Type Systems  blueArrow
3/17/2004; 4:30:20 AM (reads: 123, responses: 1)
The best text on type systems that I know of is John Mitchell's Foundations for Programming Languages; it's a pretty thorough introduction to the basics, and very careful. Pierce also comes highly recommended, but I haven't read my copy yet. I also like Carl Gunter's Semantics of Programming Languages.

Ehud Lamm - Re: Introduction to (Formal) Type Systems  blueArrow
3/17/2004; 6:56:53 AM (reads: 118, responses: 0)
Pierce also comes highly recommended...

I like (most of) it.