Computer Science – Programming Languages
Scientific paper
2011-03-25
Computer Science
Programming Languages
Scientific paper
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 refinement types wherein the typing relation is itself a predicate in the refinement logic. System D coordinates SMT-based logical implication and syntactic subtyping to automatically typecheck sophisticated dynamic language programs. By coupling nested refinements with McCarthy's theory of finite maps, System D can precisely reason about the interaction of higher-order functions, polymorphism, and dictionaries. The addition of type predicates to the refinement logic creates a circularity that leads to unique technical challenges in the metatheory, which we solve with a novel stratification approach that we use to prove the soundness of System D.
Chugh Ravi
Jhala Ranjit
Rondon Patrick M.
No associations
LandOfFree
Nested Refinements for Dynamic Languages does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Nested Refinements for Dynamic Languages, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Nested Refinements for Dynamic Languages will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-571485