Explicit substitutitions for constructive necessity

Abstract

This paper introduces a λ-calculus with explicit substitutions, corresponding to an S4 modal logic of constructive necessity. As well as being semantically well motivated, the calculus can be used (a) to develop abstract machines, and (b) as a framework for specifying and analysing computation stages in the context of functional languages. We prove several syntactic properties of this calculus, which we call xDIML, and then sketch its use as an interpretation of binding analysis and partial evaluation which respects execution of programs in stages.