Relational Type Theory (All Proofs)

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 re...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2021-01
Main Authors: Stump, Aaron, Delaware, Benjamin, Jenkins, Christopher
Format: Article
Language:English
Subjects:
Polymorphism
Principles
Realizability
Semantics
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422