Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
summary
Tool extracts Type Racket’s boundary contracts, runs the SCV symbolic verifier on the untyped client code, and selectively bypasses only those runtime checks proven impossible to fail. Implemented as SCVCR, the system is modular and handles proxying, struct-field contracts, and partial verification of mixed configurations. Evaluated on 12 benchmarks, it eliminates almost all overhead (zero in most cases) and yields a worst-case slowdown of about 1.6× versus fully untyped execution.
AI-written summary · about
chapters (20)
- 0:00Introduction
- 0:36Problem description
- 1:57Performance Cost Graph
- 3:03SCVCR
- 3:51Runtime Enforcement
- 4:53What can be done
- 5:53Running example
- 9:10From
- 12:34From Function
- 14:04Contract of Stream
- 14:27Main module
- 14:48Sift
- 15:15Abstract Semantics
- 15:49Eliminate Contracts
- 17:02Implementation Differences
- 18:41Optimization
- 19:44Evaluation
- 20:40Benchmarks
- 21:24Benchmark Summary
- 21:42Conclusion
related talks
21mGradual Typing is the best!
33mTyped Clojure: From Optional to Gradual Typing
23mHow Type-Driven Development Can Turbocharge your Contract's Security
24mType Checking with Sorbet
15mTypestate via Revocable Capabilities
41mTyped Clojure
34mType Your Business
37mTyping the Untyped: Soundness in Gradual Type Systems