TY - GEN

T1 - Formalizing soundness of contextual effects

AU - Pratikakis, Polyvios

AU - Foster, Jeffrey S.

AU - Hicks, Michael

AU - Neamtiu, Iulian

PY - 2008/12/5

Y1 - 2008/12/5

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

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

UR - http://www.scopus.com/inward/record.url?scp=57049152977&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=57049152977&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-71067-7-22

DO - 10.1007/978-3-540-71067-7-22

M3 - Conference contribution

AN - SCOPUS:57049152977

SN - 3540710655

SN - 9783540710653

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 262

EP - 277

BT - Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings

T2 - 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008

Y2 - 18 August 2008 through 21 August 2008

ER -