Relational Type Theory (All Proofs)

Aaron Stump; Benjamin Delaware; Christopher Jenkins

doi:10.48550/arxiv.2101.09655

Back

Preprint

Open access

Relational Type Theory (All Proofs)

Aaron Stump, Benjamin Delaware and Christopher Jenkins

ArXiv.org

01/24/2021

DOI: 10.48550/arxiv.2101.09655

Files and links (1)

url

https://doi.org/10.48550/arXiv.2101.09655View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

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.

Computer Science - Logic in Computer Science

Details

Title: Subtitle: Relational Type Theory (All Proofs)
Creators: Aaron Stump
Benjamin Delaware
Christopher Jenkins
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.2101.09655
ISSN: 2331-8422
Language: English
Date posted: 01/24/2021
Academic Unit: Computer Science
Record Identifier: 9984410845102771

Metrics

1 Record Views