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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

44 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 languageEnglish (US)
Title of host publicationConference Record of POPL 2007
Subtitle of host publicationThe 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Papers Presented at the Symposium
Pages109-122
Number of pages14
DOIs
StatePublished - Sep 3 2007
Event34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - Nice, France
Duration: Jan 17 2007Jan 19 2007

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
CountryFrance
CityNice
Period1/17/071/19/07

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Impredicative polymorphism
  • Kripke models
  • Mutable references
  • Recursive types

Fingerprint Dive into the research topics of 'A very modal model of a modern, major, general type system'. Together they form a unique fingerprint.

Cite this