 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 
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
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 - http://www-2.cs.cmu.edu/~rwh/plbook/
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
3/11/2004; 6:31:02 AM (reads: 246, responses: 0)
|
|
|
|
Neel Krishnaswami - Re: Introduction to (Formal) Type Systems
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
3/11/2004; 10:26:35 AM (reads: 230, responses: 0)
|
|
|
|
Ehud Lamm - Re: Introduction to (Formal) Type Systems
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
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
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
3/17/2004; 4:30:20 AM (reads: 123, responses: 1)
|
|
|
|
Ehud Lamm - Re: Introduction to (Formal) Type Systems
3/17/2004; 6:56:53 AM (reads: 118, responses: 0)
|
|
|
Pierce also comes highly recommended...
I like (most of) it.
|
|
|
|