Skip to Main content Skip to Navigation
Journal articles

Strong Normalization in two Pure Pattern Type Systems

Benjamin Wack 1 Clement Houtmann 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Pure Pattern Type Systems (P 2 T S ) combine in a unified setting the frameworks and capabilities of rewriting and λ-calculus. Their type systems, adapted from Barendregt's λ-cube, are especially interesting from a logical point of view. Strong normalization, an essential property for logical soundness, had only been conjectured so far: in this paper, we give a positive answer for the simply-typed system and the dependently-typed system. The proof is based on a translation of terms and types from P 2 T S into the λ-calculus. First, we deal with untyped terms, ensuring that reductions are faithfully mimicked in the λ-calculus. For this, we rely on an original encoding of the pattern matching capability of P 2 T S into the System Fω. Then we show how to translate types: the expressive power of System Fω is needed in order to fully reproduce the original typing judgments of P 2 T S . We prove that the encoding is correct with respect to reductions and typing, and we conclude with the strong normalization of simply-typed P 2 T S terms. The strong normalization with dependent types is in turn obtained by an intermediate translation into simply-typed terms.
Document type :
Journal articles
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Clement Houtmann <>
Submitted on : Monday, November 12, 2007 - 3:25:58 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Monday, September 24, 2012 - 3:10:16 PM


Files produced by the author(s)




Benjamin Wack, Clement Houtmann. Strong Normalization in two Pure Pattern Type Systems. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2008, Rewriting calculi, higher-order reductions and patterns, 18 (3), pp.431-465. ⟨10.1017/S0960129508006749⟩. ⟨inria-00186815⟩



Record views


Files downloads