TY - GEN
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érme
N1 - Copyright:
Copyright 2008 Elsevier B.V., All rights reserved.
PY - 2007
Y1 - 2007
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=34548217707&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34548217707&partnerID=8YFLogxK
U2 - 10.1145/1190216.1190235
DO - 10.1145/1190216.1190235
M3 - Conference contribution
AN - SCOPUS:34548217707
SN - 1595935754
SN - 9781595935755
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 109
EP - 122
BT - Conference Record of POPL 2007
T2 - 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Y2 - 17 January 2007 through 19 January 2007
ER -