Processing math: 100%

Posts tagged Author: Li-Yao Xia

Syntactic parametricity strikes again

::

By: Gabriel Scherer, Li-Yao Xia

In this blog post, reporting on a collaboration with Li-Yao Xia, I will show an example of how some results that we traditionally think of as arising from free theorems / parametricity can be established in a purely “syntactic” way, by looking at the structure of canonical derivations. More precisely, I prove that α.List αList α is isomorphic to Π(n:N).List (Fin n) where Fin n is the type of integers smaller than n, corresponding to the set {0,1,,n1}.