We present a formalization of the λσ ⇑-calculus[9] in the Coq V5.8 system[6]. The principal axiomatized result is the confluence of this calculus. Furthermore we propose a uniform encoding for many-sorted first order term rewriting systems, on which we study the local confluence by critical pairs analysis.
CITATION STYLE
Saïbi, A. (1995). Formalization of a λ-calculus with explicit substitutions in Coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 996, pp. 183–202). Springer Verlag. https://doi.org/10.1007/3-540-60579-7_10
Mendeley helps you to discover research relevant for your work.