Relational Type Theory (All Proofs)
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.
Cite
@article{arxiv.2101.09655,
title = {Relational Type Theory (All Proofs)},
author = {Aaron Stump and Benjamin Delaware and Christopher Jenkins},
journal= {arXiv preprint arXiv:2101.09655},
year = {2021}
}