Complete Monitors for Gradual Types
Syntactic type soundness is too weak to tell apart different ways of running a program that mixes typed and untyped code. Complete monitoring is a stronger property that captures a meaningful distinction — a language satisfies complete monitoring iff it checks all interactions between typed and untyped code.