Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear lambda-Calculus.
| hal.structure.identifier | Linguistic signs, grammar and meaning: computational logic for natural language [SIGNES] | |
| dc.contributor.author | SALVATI, Sylvain | |
| dc.contributor.editor | Frank Pfenning | |
| dc.date.accessioned | 2024-04-15T09:54:08Z | |
| dc.date.available | 2024-04-15T09:54:08Z | |
| dc.date.created | 2006 | |
| dc.date.issued | 2006 | |
| dc.date.conference | 2006 | |
| dc.identifier.uri | https://oskar-bordeaux.fr/handle/20.500.12278/198648 | |
| dc.description.abstractEn | We introduce syntactic descriptions, an extended type sys- tem for the linear lambda-calculus. With this type system checking that a linear lambda-term normalizes to another one reduces to type-checking. As a consequence this type system can be seen as a formal tool to design matching algorithms. In that respect, solving matching equations becomes a combination of type inference and proof search. We present such an algorithm for linear matching equations.In the case of second order equations, this algorithm stresses the similarities between linear matching in the linear lambda-calculus and linear context matching. It uses tabular techniques and is a practical alternative to Huet's algorithm for those equations. | |
| dc.language.iso | en | |
| dc.publisher | Springer-Verlag | |
| dc.subject.en | linear lambda-calculus | |
| dc.subject.en | higher-order matching | |
| dc.subject.en | type theory | |
| dc.title.en | Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear lambda-Calculus. | |
| dc.type | Communication dans un congrès | |
| dc.subject.hal | Informatique [cs]/Informatique et langage [cs.CL] | |
| bordeaux.page | 151-165 | |
| bordeaux.volume | LNCS 4098 | |
| bordeaux.hal.laboratories | Laboratoire Bordelais de Recherche en Informatique (LaBRI) - UMR 5800 | * |
| bordeaux.institution | Université de Bordeaux | |
| bordeaux.institution | Bordeaux INP | |
| bordeaux.institution | CNRS | |
| bordeaux.conference.title | 17th International Conference on Rewriting Techniques and Applications, RTA 2006 | |
| bordeaux.country | US | |
| bordeaux.conference.city | Seattle | |
| bordeaux.peerReviewed | oui | |
| hal.identifier | inria-00334006 | |
| hal.version | 1 | |
| hal.invited | non | |
| hal.proceedings | oui | |
| hal.popular | non | |
| hal.audience | Internationale | |
| hal.origin.link | https://hal.archives-ouvertes.fr//inria-00334006v1 | |
| bordeaux.COinS | ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.date=2006&rft.volume=LNCS%204098&rft.spage=151-165&rft.epage=151-165&rft.au=SALVATI,%20Sylvain&rft.genre=unknown |
Fichier(s) constituant ce document
| Fichiers | Taille | Format | Vue |
|---|---|---|---|
|
Il n'y a pas de fichiers associés à ce document. |
|||