文章基本信息

标题：INTERNAL PARAMETRICITY FOR CUBICAL TYPE THEORY
本地全文：下载
作者：Evan Cavallo ; Robert Harper
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2021
卷号：17
期号：4
页码：1-60
DOI：10.46298/lmcs-17(4:5)2021
语种：English
出版社：Technical University of Braunschweig
摘要：We define a computational type theory combining the contentful equality structure of cartesian cubical type theory with internal parametricity primitives. The combined theory supports both univalence and its relational equivalent, which we call relativity. We demonstrate the use of the theory by analyzing polymorphic functions between higher inductive types, observe how cubical equality regularizes parametric type theory, and examine the similarities and discrepancies between cubical and parametric type theory, which are closely related. We also abstract a formal interface to the computational interpretation and show that this also has a presheaf model.
关键词：cubical type theory;parametricity;computational type theory;modal type theory