Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01330955
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Monday, June 13, 2016 - 11:28:20 AM
Last modification on : Tuesday, July 7, 2020 - 11:52:46 AM

File

HOR_2016_paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01330955, version 1

Collections

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. ⟨hal-01330955⟩

Share

Metrics

Record views

603

Files downloads

112