Type soundness proofs with definitional interpreters
View / Open Files
Authors
Amin, Nada
Rompf, Tiark
Publication Date
2017-01-21Journal 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)
Publisher
ACM
Pages
666-679
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Amin, N., & Rompf, T. (2017). Type soundness proofs with definitional interpreters. POPL 2017 Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 666-679. https://doi.org/10.1145/3009837.3009866
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.
Sponsorship
This research was supported by NSF through awards 1553471 and 1564207.
Identifiers
External DOI: https://doi.org/10.1145/3009837.3009866
This record's URL: https://www.repository.cam.ac.uk/handle/1810/292533
Rights
Licence:
http://www.rioxx.net/licenses/all-rights-reserved
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.