Abstract
We present a unification procedure for calculi with explicit substitutions (ES) without propagation rules. The novelty of this work is that the unification procedure was developed for the calculi with ES that belong to the paradigm known as “act at a distance”,i.e. explicit substitutions are not propagated to the level of variables,as usual. The unification procedure is proved correct and complete,and enjoy a simple form of substitution,called grafting,instead of the standard capture avoiding variable substitution.
Cite
CITATION STYLE
de Moura, F. L. C. (2016). Unification for λ-calculi without propagation rules. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9965 LNCS, pp. 179–195). Springer Verlag. https://doi.org/10.1007/978-3-319-46750-4_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
