Abstract

Gradual typing semantics are usually given as a translation from a gradually typed calculus to a statically-typed calculus with casts. In this work, we extend this to move from a gradually-typed source language to C with cast support. Along the way, we discuss efficiency concerns and implementation approaches, explaining our decisions and how they impact the final product: a compiler for the gradually-typed lambda calculus (extended with common features).