We characterize those terms which are strongly normalizing in a composition-free calculus of explicit substitutions by defining a suitable type system using intersection types. The key idea is the notion of available variable in a term, which is a generalization of the classical notion of free variable.
CITATION STYLE
Dougherty, D., Lengrand, S., & Lescanne, P. (2002). An improved system of intersection types for explicit substitutions. IFIP Advances in Information and Communication Technology, 96, 511–523. https://doi.org/10.1007/978-0-387-35608-2_42
Mendeley helps you to discover research relevant for your work.