A Simple Proof Technique for Certain Parametricity Results-

Many properties of parametric, polymorphic functions can be determined simply by inspection of their types. Such results are usually proven using Reynoldsʹs parainetricity theorem. However, Reynoldsʹs theorem can be difficult to show in some settings, particularly ones involving computational effects. I present an alternative technique for proving some parametricity results. This technique is considerably simpler and easily generalizes to effectful settings. It works by instantiating polymorphic functions with singleton types that fully specify the behavior of the functions. Using this technique, I show that callersʹ stacks are protected from corruption during function calls in Typed Assembly Language programs.