Parametricity in Type Theory: Language Primitives and Application

Parametricity is an important property of functions in computer science, offering valuable proof techniques for reasoning about programs. This is true for pen and paper reasoning, but also for reasoning internally in dependently-typed programming languages and proof assistants. However, current support for (internal) parametricity in these languages is not satisfactory, both in terms of expressiveness (can we prove standard results of parametricity?) and for technical reasons (requireslarge amounts of meta-theoretical reasoning). The goal of this project is to devise, implement and evaluate a full fledged intensional, axiom-free and internally parametric dependent type theory, which is expressive enough for standard examples. In order to build such a type system, our approach will rely on studying language primitives capable of providing computational content for parametricity, together with their denotational semantics (specifically presheaf semantics), including the recently proposed transpension type. We will implement the system in an exisiting or purpose-built proof assistant. We will evaluate and demonstrate the power and expressiveness of the obtained system both at a practical level (by studying important examples : the embedding of standard parametric calculi and free constructions) and at a theoretical level (by proving meta-theoretical results about the resulting theory)..