Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification

Cameron Moy, Phúc C. Nguyen, Sam Tobin-Hochstadt +1

Gradually-typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries betwe…