A Logical Foundation for Environment Classifiers

Taha and Nielsen have developed a multi-stage calculus {\lambda}{\alpha} witha sound type system using the notion of environment classifiers. They arespecial identifiers, with which code fragments and variable declarations areannotated, and their scoping mechanism is used to ensure statically thatcertain code fragments are closed and safely runnable. In this paper, weinvestigate the Curry-Howard isomorphism for environment classifiers bydeveloping a typed {\lambda}-calculus {\lambda}|>. It corresponds tomulti-modal logic that allows quantification by transition variables---acounterpart of classifiers---which range over (possibly empty) sequences oflabeled transitions between possible worlds. This interpretation will reducethe "run" construct---which has a special typing rule in{\lambda}{\alpha}---and embedding of closed code into other code fragments ofdifferent stages---which would be only realized by the cross-stage persistenceoperator in {\lambda}{\alpha}---to merely a special case of classifierapplication. {\lambda}|> enjoys not only basic properties including subjectreduction, confluence, and strong normalization but also an important propertyas a multi-stage calculus: time-ordered normalization of full reduction. Then,we develop a big-step evaluation semantics for an ML-like language based on{\lambda}|> with its type system and prove that the evaluation of a well-typed{\lambda}|> program is properly staged. We also identify a fragment of thelanguage, where erasure evaluation is possible. Finally, we show that the proofsystem augmented with a classical axiom is sound and complete with respect to aKripke semantics of the logic