A very modal model of a modern, major, general type system

Andrew W. Appel; Paul André Melliès; Christopher D. Richards; Jérôme Vouillon

doi:10.1145/1190215.1190235

A very modal model of a modern, major, general type system

Andrew W. Appel, Paul André Melliès, Christopher D. Richards, Jérôme Vouillon

Research output: Contribution to journal › Article › peer-review

47 Scopus citations

Abstract

We present a model of recursive and impredicatively quantified types with mutable references. We interpret in this model all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and functional languages. We establish in this purely semantic fashion a soundness proof of the typing systems underlying these TILs and TALs - ensuring that every well-typed program is safe. The technique is generic, and applies to any small-step semantics including λ-calculus, labeled transition systems, and von Neumann machines. It is also simple, and reduces mainly to defining a Kripke semantics of the Gödel-Löb logic of provability. We have mechanically verified in Coq the soundness of our type system as applied to a von Neumann machine.

Original language	English (US)
Pages (from-to)	109-122
Number of pages	14
Journal	ACM SIGPLAN Notices
Volume	42
Issue number	1
DOIs	https://doi.org/10.1145/1190215.1190235
State	Published - Jan 2007

All Science Journal Classification (ASJC) codes

General Computer Science

Keywords

Impredicative polymorphism
Kripke models
Mutable references
Recursive types

Access to Document

10.1145/1190215.1190235

Cite this

@article{63e69e0247094703adf9d3f797d34946,

title = "A very modal model of a modern, major, general type system",

abstract = "We present a model of recursive and impredicatively quantified types with mutable references. We interpret in this model all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and functional languages. We establish in this purely semantic fashion a soundness proof of the typing systems underlying these TILs and TALs - ensuring that every well-typed program is safe. The technique is generic, and applies to any small-step semantics including λ-calculus, labeled transition systems, and von Neumann machines. It is also simple, and reduces mainly to defining a Kripke semantics of the G{\"o}del-L{\"o}b logic of provability. We have mechanically verified in Coq the soundness of our type system as applied to a von Neumann machine.",

keywords = "Impredicative polymorphism, Kripke models, Mutable references, Recursive types",

author = "Appel, {Andrew W.} and Melli{\`e}s, {Paul Andr{\'e}} and Richards, {Christopher D.} and J{\'e}r{\^o}me Vouillon",

year = "2007",

month = jan,

doi = "10.1145/1190215.1190235",

language = "English (US)",

volume = "42",

pages = "109--122",

journal = "ACM SIGPLAN Notices",

issn = "1523-2867",

publisher = "Association for Computing Machinery (ACM)",

number = "1",

}

TY - JOUR

T1 - A very modal model of a modern, major, general type system

AU - Appel, Andrew W.

AU - Melliès, Paul André

AU - Richards, Christopher D.

AU - Vouillon, Jérôme

PY - 2007/1

Y1 - 2007/1

N2 - We present a model of recursive and impredicatively quantified types with mutable references. We interpret in this model all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and functional languages. We establish in this purely semantic fashion a soundness proof of the typing systems underlying these TILs and TALs - ensuring that every well-typed program is safe. The technique is generic, and applies to any small-step semantics including λ-calculus, labeled transition systems, and von Neumann machines. It is also simple, and reduces mainly to defining a Kripke semantics of the Gödel-Löb logic of provability. We have mechanically verified in Coq the soundness of our type system as applied to a von Neumann machine.

AB - We present a model of recursive and impredicatively quantified types with mutable references. We interpret in this model all of the type constructors needed for typed intermediate languages and typed assembly languages used for object-oriented and functional languages. We establish in this purely semantic fashion a soundness proof of the typing systems underlying these TILs and TALs - ensuring that every well-typed program is safe. The technique is generic, and applies to any small-step semantics including λ-calculus, labeled transition systems, and von Neumann machines. It is also simple, and reduces mainly to defining a Kripke semantics of the Gödel-Löb logic of provability. We have mechanically verified in Coq the soundness of our type system as applied to a von Neumann machine.

KW - Impredicative polymorphism

KW - Kripke models

KW - Mutable references

KW - Recursive types

UR - http://www.scopus.com/inward/record.url?scp=33846518318&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33846518318&partnerID=8YFLogxK

U2 - 10.1145/1190215.1190235

DO - 10.1145/1190215.1190235

M3 - Article

AN - SCOPUS:33846518318

SN - 1523-2867

VL - 42

SP - 109

EP - 122

JO - ACM SIGPLAN Notices

JF - ACM SIGPLAN Notices

IS - 1

ER -

A very modal model of a modern, major, general type system

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this