%0 Generic %1 stump2021relational %A Stump, Aaron %A Delaware, Benjamin %A Jenkins, Christopher %D 2021 %K 03b15-higher-order-logic-type-theory %T Relational Type Theory (All Proofs) %U http://arxiv.org/abs/2101.09655 %X This paper introduces Relational Type Theory (RelTT), a new approach to type theory with extensionality principles, based on a relational semantics for types. The type constructs of the theory are those of System F plus relational composition, converse, and promotion of application of a term to a relation. A concise realizability semantics is presented for these types. The paper shows how a number of constructions of traditional interest in type theory are possible in RelTT, including eta-laws for basic types, inductive types with their induction principles, and positive-recursive types. A crucial role is played by a lemma called Identity Inclusion, which refines the Identity Extension property familiar from the semantics of parametric polymorphism. The paper concludes with a type system for RelTT, paving the way for implementation.

@misc{stump2021relational, abstract = {This paper introduces Relational Type Theory (RelTT), a new approach to type theory with extensionality principles, based on a relational semantics for types. The type constructs of the theory are those of System F plus relational composition, converse, and promotion of application of a term to a relation. A concise realizability semantics is presented for these types. The paper shows how a number of constructions of traditional interest in type theory are possible in RelTT, including eta-laws for basic types, inductive types with their induction principles, and positive-recursive types. A crucial role is played by a lemma called Identity Inclusion, which refines the Identity Extension property familiar from the semantics of parametric polymorphism. The paper concludes with a type system for RelTT, paving the way for implementation.}, added-at = {2023-07-01T01:23:28.000+0200}, author = {Stump, Aaron and Delaware, Benjamin and Jenkins, Christopher}, biburl = {https://www.bibsonomy.org/bibtex/2568fa634205d6f2ae6961c7a8673b61f/gdmcbain}, howpublished = {arxiv:2101.09655}, interhash = {ac7750055819efc6eb7f25b00e138423}, intrahash = {568fa634205d6f2ae6961c7a8673b61f}, keywords = {03b15-higher-order-logic-type-theory}, timestamp = {2023-07-01T01:23:28.000+0200}, title = {Relational Type Theory (All Proofs)}, url = {http://arxiv.org/abs/2101.09655}, year = 2021 }