Generalised-reduction and explicit substitutions 8th international conference on Programming Languages: Implementations, Logics and

Abstract. Extending the -calculus with either explicit substitution or generalised reduction has been the subject of extensive research recently which still has many open problems. Due to this reason, the properties of a calculus combining both generalised reduction and explicit substitu-tions have never been studied. This paper presents such a calculus sg and shows that it is a desirable extension of the -calculus. In partic-ular, we show that sg preserves strong normalisation, is sound and it simulates classical -reduction. Furthermore, we study the simply typed -calculus extended with both generalised reduction and explicit substi-tution and show that well-typed terms are strongly normalising and that other properties such as subtyping and subject reduction hold