How to start studying type systems?

[Lauri Alanko]

Hello there.

I've found the study of programming languages fascinating, especially of
late type systems. There is a wealth of intriguing research papers
available on the net, but I find them slightly too involved for me for
now. Also, I'm not entirely familiar with the formal notation for
defining the semantics of type systems. I do understand basic predicate
logic, but formal type systems seem to require knowing the notations for
some additional concepts.

So could someone please give pointers on where to start to acquire a
literacy for those more theoretical POPL, PLDI and OOPSLA papers? I'm
not sure they even teach those things where I study...

Thanks.

Lauri Alanko
l...@iki.fi

[andrewj...@my-deja.com]

In article <slrn83mh...@la.pp.htv.fi>,
l...@iki.fi (Lauri Alanko) wrote:

> So could someone please give pointers on where to start to acquire a
> literacy for those more theoretical POPL, PLDI and OOPSLA papers? I'm
> not sure they even teach those things where I study...

You could try Luca Cardelli's "Type Systems" survey. See

http://www.luca.demon.co.uk/Bibliography.html

There are a number of good textbooks on the formal semantics of
programming languages that you would find useful background for POPL-
like papers. Try Winskel's "Formal Semantics of Programming Languages"
(MIT Press) or Gunter's "Semantics of Programming Languages" (also MIT
Press) or Mitchell's "Foundations of Programming Languages" (MIT Press
yet again).

- Andrew.

Sent via Deja.com http://www.deja.com/
Before you buy.

[Shin-Cheng Mu]

Hi,

Lauri Alanko wrote:
> I've found the study of programming languages fascinating, especially of
> late type systems. There is a wealth of intriguing research papers
> available on the net, but I find them slightly too involved for me for
> now. Also, I'm not entirely familiar with the formal notation for
> defining the semantics of type systems. I do understand basic predicate
> logic, but formal type systems seem to require knowing the notations for
> some additional concepts.

Among other things, you could start from some of Luca
Cardelli's paper. He wrote many things about types.
In particular, "Basic polymorphic typechecking" serves
as a good tutorial explaining how type checking works
from both an operational and a formal point of view.

http://www.luca.demon.co.uk/Bibliography.html

sincerely,
Shin-Cheng Mu

[/bin/csh]

l...@iki.fi (Lauri Alanko) writes:
> Hello there.

> I do understand basic predicate
> logic, but formal type systems seem to require knowing the notations for
> some additional concepts.
>

> So could someone please give pointers on where to start to acquire a
> literacy for those more theoretical POPL, PLDI and OOPSLA papers? I'm
> not sure they even teach those things where I study...

When I started fooling with these things I was inspired by the book
"Realistic Compiler Generation" by Peter Lee. He wrote it from
his doctoral thesis (IIRC), and it provides (indirectly) an excellent
introduction to denotational semantics (which is the voodoo that you
see in many of the papers) by showing how to build a compiler that is
driven by the semantic specification of the language (NOTE TO COMPILER
GEEKS: he is *not* using attribute grammars). He used a lot of
examples comparing code fragments with a fairly intuitive operational
semantics and denotational semantics. And his code generator was
written in SML! (which was my first inspiration for learning the
language. I could read and understand his code without even knowing
the language it was written in! I thought that any language that was
that clear and concise had to be worth learning...)

From there I got into Tennent, Scott & Strachey, whose papers are
referenced from Lee's book. If you can get this far, you'll know that
you can read anything if you care to spend the time to decipher
it. Being a working-stiff engineer, I mostly read these papers for the
results, rather than the proofs. Then I try to use the results in my
code.

Happy Hackin!
david rush