Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Modularity of strong normalization and confluence in the algebraic-λ-cube (at LICS 1994)

Authors: Franco Barbanera Maribel Fernández Herman Geuvers

Abstract

Presents the algebraic-λ-cube, an extension of Barendregt's (1991) λ-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all systems in the algebraic-λ-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada (1991). This result is proven for the algebraic extension of the calculus of constructions, which contains all the systems of the algebraic-λ-cube. We also prove that local confluence is a modular property of all the systems in the algebraic-λ-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence

BibTeX

  @InProceedings{FernndezGeuvers-Modularityofstrongn,
    author = 	 {Franco Barbanera and Maribel Fernández and Herman Geuvers},
    title = 	 {Modularity of strong normalization and confluence in the algebraic-λ-cube },
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {406--415},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski