A Framework for Internalizing Relations into Type Theory

Abstract : 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.
Type de document :
Communication dans un congrès
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00614252
Contributeur : Assia Mahboubi <>
Soumis le : mercredi 10 août 2011 - 12:51:41
Dernière modification le : lundi 11 décembre 2017 - 11:20:19
Document(s) archivé(s) le : vendredi 11 novembre 2011 - 02:21:05

Fichier

FuAl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00614252, version 1

Collections

Citation

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, Aug 2011, Wroclaw, Poland. 2011. 〈inria-00614252〉

Partager

Métriques

Consultations de la notice

71

Téléchargements de fichiers

39