Metatheoretic Results for a Modal lambda-Calculus

Abstract: This paper presents the proofs of the strong normalization, subjectreduction, and Church-Rosser theorems for a presentation of the intuitionisticmodal -calculus S4. It is adapted from Healfdene Goguen'sthesis, where these properties are shown for the simply typed -calculus and for Luo's type theory UTT. Following this method, weintroduce the notion of typed operational semantics for our system.