The Barendregt cube with definitions and generalised reduction

In this paper, we propose to extend the Barendregt Cube by generalisingß-reduction and by adding definition mechanisms. Generalised reduction allows contracting more visible redexes than usual, and definitions are an important tool to allow for a more flexible typing system. We show that this extension satisfies most of the original properties of the Cube including Church-Rosser, Subject Reduction and Strong Normalisation