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 journalArticlepeer-review

45 Scopus citations


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)
Pages (from-to)109-122
Number of pages14
JournalACM SIGPLAN Notices
Issue number1
StatePublished - Jan 2007

All Science Journal Classification (ASJC) codes

  • General Computer Science


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


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