Programs written in dynamic languages make heavy use of features — run-time type tests, value-indexed dictionaries, polymorphism, and higher-order functions — that are beyond the reach of type systems that employ either purely syntactic or purely semantic reasoning. We present a core calculus, System D, that merges these two modes of reasoning into a single powerful mechanism of nested re- ï¬nement types wherein the typing relation is itself a predicate in the reï¬nement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested reï¬nements with McCarthy’s theory of ï¬nite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the reï¬nement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratiï¬cation approach that we use to prove the soundness of System D.
In the Proceedings of the 39th ACM Symposium on Principles of Programming Languages, 2012. (POPL 2012).