A second-order pattern matching algorithm for the cube of typed \(\lambda\)-calculi. (English) Zbl 0764.68045
Mathematical foundations of computer science, Proc. 16th Int. Symp., Kazimierz Dolny/Pol. 1991, Lect. Notes Comput. Sci. 520, 151-160 (1991).
Summary: [For the entire collection see Zbl 0753.00030.]
G. Huet, [Résolution d’Équations dans les Langages d’Ordre \(1,2,\dots,\omega\), Thèse de Doctorat d’État, Université de Paris VII (1976)] and G. Huet and B. Lang, [Acta Inf. 11, 31-35 (1978; Zbl 0389.68008)] gives an algorithm for second-order pattern matching in the simply typed \(\lambda\)-calculus. We generalize this algorithm to the calculi of Barendregt’s cube [H. Barendregt, Introduction to Generalized Type Systems, To appear in Journal of Functional Programming]. The same result is presented in a longer paper where proofs are given [G. Dowek, A Second-Order Pattern Matching Algorithm for the Cube of typed \(\lambda\)-Calculi, Rapport de Recherche INRIA (1991)].
G. Huet, [Résolution d’Équations dans les Langages d’Ordre \(1,2,\dots,\omega\), Thèse de Doctorat d’État, Université de Paris VII (1976)] and G. Huet and B. Lang, [Acta Inf. 11, 31-35 (1978; Zbl 0389.68008)] gives an algorithm for second-order pattern matching in the simply typed \(\lambda\)-calculus. We generalize this algorithm to the calculi of Barendregt’s cube [H. Barendregt, Introduction to Generalized Type Systems, To appear in Journal of Functional Programming]. The same result is presented in a longer paper where proofs are given [G. Dowek, A Second-Order Pattern Matching Algorithm for the Cube of typed \(\lambda\)-Calculi, Rapport de Recherche INRIA (1991)].
