We introduce syntactic descriptions, an extended type system for the linear λ-calculus. With this type system checking that a linear λ-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 λ-calculus and linear context matching. It uses tabular techniques and is a practical alternative to Huet's algorithm for those equations. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Salvati, S. (2006). Syntactic descriptions: A type system for solving matching equations in the linear λ-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4098 LNCS, pp. 151–165). Springer Verlag. https://doi.org/10.1007/11805618_12
Mendeley helps you to discover research relevant for your work.