## Wednesday, September 12, 2018

The runtime semantics of a gradually typed language is typically given in two parts: 1) a translation to a cast calculus and 2) an operational semantics for the cast calculus. Nowadays,  I recommend using coercions to express casts because they help to constrain the design space in a good way, they are easily extended to handle blame tracking, and they can be compressed to ensure space efficiency (time too!). This paper defines an easy-to-understand coercion calculus $$\lambda C$$ and a space-efficient calculus $$\lambda S$$, proves that they are equivalent to the standard cast calculus $$\lambda B$$, and also reviews the blame safety theorem.