Formalizing Soundness of Contextual Effects

摘要: A contextual effectsystem generalizes standard type and effect systems: where a system computes the of an expression e, additionally priorand futureeffect which characterize behavior computation prior to following, respectively, evaluation e. This paper describes formalization proof soundness effects, we mechanized using Coq assistant. Contextual is unusual property because future term edepends not on eitself (or its evaluation), but rather context in eappears. Therefore, state prove must "match up" subterm original typing derivation with possibly-many evaluations that during program, way robust under substitution. We do this novel typed operational semantics. conjecture our approach could useful for reasoning about other properties derivations rely appears.