Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear lambda-Calculus.
Langue
en
Communication dans un congrès
Ce document a été publié dans
17th International Conference on Rewriting Techniques and Applications, RTA 2006, 2006, Seattle. 2006, vol. LNCS 4098, p. 151-165
Springer-Verlag
Résumé en anglais
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 ...Lire la suite >
Mots clés en anglais
linear lambda-calculus
higher-order matching
type theory