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 metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Monday, June 13, 2016 - 11:28:20 AM
Last modification on : Thursday, January 20, 2022 - 4:13:47 PM


Files produced by the author(s)


  • HAL Id : hal-01330955, version 1


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⟩



Les métriques sont temporairement indisponibles