A Modal Lambda Calculus with Iteration and Case Constructs.

An extension of the simply-typed λ-calculus, allowing iteration and case reasoning over terms of functional types that arise when using higher order abstract syntax, has recently been introduced by F. Pfenning, C. Schürmann and the first author. This thorny mixing is achieved thanks to the help of the operator '□' of modal logic S4. Here we give a new presentation of their system, with reduction rules, instead of evaluation judgments, that compute the canonical forms of terms. Our presentation is based on a modal λ-calculus that is better from the user's point of view. Moreover we do not impose a particular strategy of reduction during the computation. Our system enjoys the decidability of typability, soundness of typed reduction with respect to typing rules, the Church-Rosser and strong normalization properties and it is a conservative extension over the simply-typed λ-calculus.