Repository logo
 

Type soundness proofs with definitional interpreters

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Amin, Nada 
Rompf, Tiark 

Abstract

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculus, cannot simultaneously support key metatheoretic properties such as environment narrowing and subtyping transitivity, which are usually required for a type soundness proof. Moreover, Scala and many other realistic languages lack a general substitution property.

The first contribution of this paper is to demonstrate how type soundness proofs for advanced, polymorphic, type systems can be carried out with an operational semantics based on high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proofs in this style for System F<: and several extensions, including mutable references. Our proofs use only straightforward induction, which is significant, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require coinductive proof techniques.

The second main contribution of this paper is to show how DOT-like calculi emerge from straightforward generalizations of the operational aspects of F<:, exposing a rich design space of calculi with path-dependent types in between System F and DOT, which we dub the System D Square.

By working directly on the target language, definitional interpreters can focus the design space and expose the invariants that actually matter at runtime. Looking at such runtime invariants is an exciting new avenue for type system design.

Description

Keywords

46 Information and Computing Sciences, 4612 Software Engineering

Journal Title

POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

Conference Name

44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)

Journal ISSN

Volume Title

Publisher

ACM
Sponsorship
This research was supported by NSF through awards 1553471 and 1564207.