Untyped Confluence in Dependent Type Theories

Abstract : We investigate techniques based on van Oostrom's decreasing diagrams that reduce confluence proofs to the checking of critical pairs in the absence of termination properties, which are useful in dependent type calculi to prove confluence on untyped terms. These techniques are applied to a complex example originating from practice: a faithful encoding, in an extension of LF with rewrite rules on objects and types, of a subset of the calculus of inductive constructions with a cumulative hierarchy of predicative universes above Prop. The rules may be first-order or higher-order, plain or modulo, non-linear on the right or on the left. Variables which occur non-linearly in lefthand sides of rules must take their values in confined types: in our example, the natural numbers. The first-order rules are assumed to be terminating and confluent modulo some theory: in our example, associativity, commutativity and identity. Critical pairs involving higher-order rules must satisfy van Oostrom's decreasing diagram condition wrt their indexes taken as labels.
Type de document :
Communication dans un congrès
Proceedings Higher-Order Rewriting Workshop, Jun 2016, Porto, Portugal. Easy-Chair, Higher-Order Rewriting Workshop, 2016, Proc. Higher-Order rewriting Workshop. 〈http://www.diku.dk/hjemmesider/ansatte/simonsen/HOR2016/〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01330955
Contributeur : Jean-Pierre Jouannaud <>
Soumis le : lundi 13 juin 2016 - 11:28:20
Dernière modification le : jeudi 10 mai 2018 - 02:06:57

Fichier

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

Identifiants

  • HAL Id : hal-01330955, version 1

Citation

Ali Assaf, Gilles Dowek, Jean-Pierre Jouannaud, Jiaxiang Liu. Untyped Confluence in Dependent Type Theories. Proceedings Higher-Order Rewriting Workshop, Jun 2016, Porto, Portugal. Easy-Chair, Higher-Order Rewriting Workshop, 2016, Proc. Higher-Order rewriting Workshop. 〈http://www.diku.dk/hjemmesider/ansatte/simonsen/HOR2016/〉. 〈hal-01330955〉

Partager

Métriques

Consultations de la notice

430

Téléchargements de fichiers

66