“In gradual typing, different languages perform different dynamic type checks for the same program. … This raises the question of whether, given a gradually typed language, the combination of the translation that injects checks in well-typed terms and the dynamic semantics that determines their behavior sufficiently enforce the static type system of the language. … In response, we present vigilance, a semantic analytical instrument that defines when the check-injecting translation and dynamic semantics of a gradually typed language are adequate for its static type system.”

Find the paper and authors list inthe ACM Programming Languages proceedings.