Higher-order Matching in the Linear lambda-calculus with Pairing

Philippe De Groote 1 Sylvain Salvati 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We prove that higher-order matching in the linear $\lambda$-calculus with pairing is decidable. We also establish its NP-completeness under the assumption that the right-hand side of the equation to be solved is given in normal form.
Mots-clés : linear logic filtrage matching linear lambda-calculus lambda-calcul linéaire logique linéaire
Type de document :
Communication dans un congrès
Jerzy Marcinkowski, Andrzej Tarlecki. 18th International Workshop on Computer Science Logic - CSL'2004, Sep 2004, Karpacz, Poland, Springer, 3210, pp.220-234, 2004, Lecture notes in Computer Science
Liste complète des métadonnées
https://hal.inria.fr/inria-00100082
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 10:13:58
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48

Identifiants

  • HAL Id : inria-00100082, version 1

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Philippe De Groote, Sylvain Salvati. Higher-order Matching in the Linear lambda-calculus with Pairing. Jerzy Marcinkowski, Andrzej Tarlecki. 18th International Workshop on Computer Science Logic - CSL'2004, Sep 2004, Karpacz, Poland, Springer, 3210, pp.220-234, 2004, Lecture notes in Computer Science. 〈inria-00100082〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

210

Contact


archive-ouverte@inria.fr