In ((

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 substitutions have never been studied. This paper presents such a calculus sg and shows that it is a desirable extension of the -calculus. In particular, 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 substitution and show that well-typed terms are strongly normalising and that other properties such as subtyping and subject reduction hold