HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information

On the complexity of higher-order matching in the linear $\lambda$-calculus

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 linear second-order matching in the linear $\lambda$-calculus with linear occurrences of the unknowns is NP-complete. This result shows that context matching and second-order matching in the linear $\lambda$-calculus are, in fact, two different problems.
Mots-clés :
Document type :
Conference papers
Domain :

https://hal.inria.fr/inria-00099593
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:39:07 AM
Last modification on : Friday, February 4, 2022 - 3:22:34 AM

Identifiers

• HAL Id : inria-00099593, version 1

Citation

Sylvain Salvati, Philippe de Groote. On the complexity of higher-order matching in the linear $\lambda$-calculus. International Conference on Rewriting Techniques and Applications - RTA'2003, Jun 2003, Valencia, Spain, pp.234-245. ⟨inria-00099593⟩

Record views