Home

[Redux] A Syntactic Approach to Type Soundness (1992)

A Syntactic Approach to Type Soundness (1992) Andrew K. Wright, Matthias Felleisen.

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features.

This paper does a good job of explaining the foundations of type soundness. It has been previously discussed on the forums. I'm posting it here since I'm just discovering it for the first time, and I think it would be useful for other neophytes.

I am using the "[Redux]" tag to denote front page posts which revisit older papers, tutorials, or overview paper directed at less experienced members of LtU. Feel free to send me any suggestions for the series at cdiggins @ gmail.com.

By cdiggins at 2006-12-06 19:30 | Type Theory | other blogs | 31931 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

If the papers were

If the papers were perviously discussed (especially as homepage items), please link to the old threads.

By Ehud Lamm at Wed, 2006-12-06 20:00 | login or register to post comments

Done.

I'ved updated the post to point to the old thread.

By cdiggins at Wed, 2006-12-06 20:28 | login or register to post comments

Thanks. Important papers are

Thanks. Important papers are usually best represented by the home page items dedicated to them, which often contain useful discussions (though not in this case, for some reason), so it usually better to link to those.

By Ehud Lamm at Wed, 2006-12-06 20:42 | login or register to post comments

In the future I will do so,

In the future I will do so, but in this case the forum link I feel is more informative.

I should point out that I didn't uncover the particular topic you linked to when I searched the site because the principal author's name (Wright) was omitted. I think it would be a good practice to make sure we include dates and authors in references to papers, so that people can more easily find references on the site.

By cdiggins at Wed, 2006-12-06 21:54 | login or register to post comments

An important paper indeed

I'm a huge fan of this paper. Here's a little praise from my part:

This paper is a really important paper in the type systems field. Before this paper was published proving the soundness of a type system was something of a black art. It was difficult and the techniques used where diverse and not very well structured (for references, see the paper). This all changed with this paper. Proving the soundness of a type system is now routine and easy.

A while back, during a graduate course in type systems, one of the students complained that many of the proofs where boring. I responded that this is in fact a feature. Soundness proofs are so well understood that they become boring. And that's a good thing, because we can then move on to explore new and more difficult problems instead. And the single most important paper for our solid understanding of soundness proofs is the above paper.

The technique used in the paper is borrowed from logic and is another good example of how many good ideas in computer science that originates in logic.

By Josef Svenningsson at Fri, 2006-12-08 14:52 | login or register to post comments