A Simple Proof Technique for Certain Parametricity Results

10 years 3 months ago
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 parametricity theorem. However, Reynolds's theorem can be di cult to show in some settings, particularly ones involving computational e ects. I present an alternative technique for proving some parametricity results. This technique is considerably simpler and easily generalizes to e ectful 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.
Karl Crary
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 1999
Where ICFP
Authors Karl Crary
Comments (0)