
19 May
2009
19 May
'09
11:23 p.m.
From: Eugene Kirpichov
Is there any research on applying free theorems / parametricity to type systems more complex than System F; namely, Fomega, or calculus of constructions and alike?
You may be interested in this: "The Theory of Parametricity in Lambda Cube" by Takeuti Izumi http://www.m.is.sci.toho-u.ac.jp/~takeuti/abs-e.html#cube -- Masahiro Sakai