A Framework for Internalizing Relations into Type Theory - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

A Framework for Internalizing Relations into Type Theory

Résumé

This paper introduces the concept of internalization struc- ture, which can be used to incorporate certain relations into FΠ , a variant of system F, while maintaining termination of the new system. We will call this process of incorporation internalization, FΠ the base system and the new system after the incorporation the internalized system. We first specify the syntax, and then the semantics of FΠ via the Tait-Girard reducibility method. We then define internalization structure. We show that we can obtain a terminating internalized system from an internal- ization structure. Finally, as motivating examples, we demonstrate how our framework can be applied to internalize subtyping, full-beta term equality and term-type inhabitation relations.
Fichier principal
Vignette du fichier
FuAl.pdf (284.62 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00614252 , version 1 (10-08-2011)

Identifiants

  • HAL Id : inria-00614252 , version 1

Citer

Peng Fu, Aaron Stump, Jeffrey Vaughan. A Framework for Internalizing Relations into Type Theory. PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Germain Faure, Stéphane Lengrand, Assia Mahboubi, Aug 2011, Wroclaw, Poland. ⟨inria-00614252⟩

Collections

PSATTT11
50 Consultations
33 Téléchargements

Partager

Gmail Facebook X LinkedIn More