We propose a new approach to typing Scheme programs based on the observation that programmers often have strong beliefs about the “normal” behavior of their code. Rather than forcing a binary choice between static types and runtime checks, we introduce default typing, where each program point carries a plausibility-ranked set of types. The highest-ranked type (rank 0) represents what the programmer believes will “almost always” be true, while higher ranks capture increasingly exceptional cases. By leveraging Racket’s macro-extensible type system and SMT-based constraint solving, we can verify whether a program type-checks using only the default assumptions. Success yields efficient code with no runtime overhead; failure produces a counterexample showing which assumptions are violated. We provide a precise notion of conditional soundness: programs are guaranteed type-safe only when their default assumptions hold at runtime.

I’m a PhD student in the POPV research group at Boston University, co-advised by Ankush Das and Marco Gaboardi. I develop type systems to guarantee behavioral soundness while easing the need/complexity of directly mechanizing code.