A way to extend the simply-typed lambda-calculus $\lambda_\to$ is to consider recursive types of the form $\mu\alpha.\tau$ (see for example http://www-verimag.imag.fr/~iosif/LogicAutomata07/type-systems-slides.pdf). The type of lists of integers would be $\mu\tau.Unit+Int\times\tau$.
Does this correspond to one of three directions in the lambda cube? If not, what would be the corresponding extension to propositional logic?