Syntactic Descriptions: a Type System for Solving Matching Equations in the Linear lambda-Calculus.
Idioma
en
Communication dans un congrès
Este ítem está publicado en
17th International Conference on Rewriting Techniques and Applications, RTA 2006, 2006, Seattle. 2006, vol. LNCS 4098, p. 151-165
Springer-Verlag
Resumen en inglés
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 ...Leer más >
Palabras clave en inglés
linear lambda-calculus
higher-order matching
type theory