A Syntactic Approach to Type Soundness

by: Andrew K Wright, Matthias Felleisen

Information and Computation, Vol. 115, No. 1. (1994), pp. 38-94.

View FullText article

CiteSeer (at Penn State), CiteSeer (at MIT), CiteSeer (at Zurich), CiteSeer (at Singapore)

Reviews [Write a review of this article]

There are no reviews of this article

Find related articles from these CiteULike users

vkp, greenrd, tautologico, bunge, tov, KarlKlose, glaubersp, SRG_at_UCD (group), mvermaat, gkuan, mcclurmc, Lambda the Ultimate (group), sclv, nominolo

Find related articles with these CiteULike tags

hindley-milner, history, icfp08, no-tag, pl, programming-language-design, proofs, proof-techniques, proof-theory, semantics, soundness, type-inference, types, type-soundness, type-theory, verification

Abstract

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. We illustrate the ...

@article{citeulike:1155, abstract = {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. We illustrate the ...}, author = {Wright, Andrew K. and Felleisen, Matthias }, citeulike-article-id = {1155}, journal = {Information and Computation}, keywords = {history, icfp08, pl, types}, number = {1}, pages = {38--94}, posted-at = {2008-03-27 20:53:25}, priority = {0}, title = {A Syntactic Approach to Type Soundness}, url = {http://citeseer.ist.psu.edu/wright92syntactic.html}, volume = {115}, year = {1994} }

RIS record

TY - JOUR ID - citeulike:1155 L3 - citeulike-article-id:1155 TI - A Syntactic Approach to Type Soundness JF - Information and Computation VL - 115 IS - 1 SP - 38 EP - 94 N2 - 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. We illustrate the ... KW - history KW - icfp08 KW - pl KW - types AU - Wright, Andrew AU - Felleisen, Matthias PY - 1994/// UR - http://citeseer.ist.psu.edu/wright92syntactic.html ER -

RIS BibTeX