This paper presents the proofs of the strong normalization, subjectreduction, and Church-Rosser theorems for a presentation of theintuitionistic modal lambda-calculus S4. It is adapted fromHealfdene Goguen's thesis, where these properties are shown for thesimply typed lambda-calculus and for Luo's type theory UTT. Following this method, weintroduce the notion of typed operational semantics for our system. Wedefine a notion of typed substitution for our system, which has contextstacks instead of the usual contexts. This latter peculiarity leads to themain difficulties and consequently to the main original features inour proofs. The techniques elaborated in this work have already been found useful in recent works [DesLel98,DesLel99] and should be further exploited to prove the properties of other systems based on modality.
展开▼
