Gallier, Jean Kripke models and the (in)equational logic of the second-order \(\lambda\)-calculus. (English) Zbl 0873.03017 Ann. Pure Appl. Logic 84, No. 3, 257-316 (1997). MSC: 03B40 18D15 03G30 PDFBibTeX XMLCite \textit{J. Gallier}, Ann. Pure Appl. Logic 84, No. 3, 257--316 (1997; Zbl 0873.03017) Full Text: DOI
Gallier, Jean Proving properties of typed \(\lambda\)-terms using realizability, covers, and sheaves. (English) Zbl 0873.68125 Theor. Comput. Sci. 142, No. 2, 299-368 (1995). MSC: 68Q55 03B40 PDFBibTeX XMLCite \textit{J. Gallier}, Theor. Comput. Sci. 142, No. 2, 299--368 (1995; Zbl 0873.68125) Full Text: DOI
Breazu-Tannen, Val; Gallier, Jean Polymorphic rewriting conserves algebraic strong normalization. (English) Zbl 0745.68065 Theor. Comput. Sci. 83, No. 1, 3-28 (1991). MSC: 68Q42 PDFBibTeX XMLCite \textit{V. Breazu-Tannen} and \textit{J. Gallier}, Theor. Comput. Sci. 83, No. 1, 3--28 (1991; Zbl 0745.68065) Full Text: DOI Link
Snyder, Wayne; Gallier, Jean Higher-order unification revisited: Complete sets of transformations. (English) Zbl 0682.03034 J. Symb. Comput. 8, No. 1-2, 101-140 (1989). Reviewer: N.Zamov MSC: 03F35 03B35 PDFBibTeX XMLCite \textit{W. Snyder} and \textit{J. Gallier}, J. Symb. Comput. 8, No. 1--2, 101--140 (1989; Zbl 0682.03034) Full Text: DOI