Computing with Contexts |
| |
Authors: | Ian A Mason |
| |
Affiliation: | (1) School of Mathematical and Computer Sciences, University of New England, NSW, Australia, 2351 |
| |
Abstract: | We investigate a representation of contexts, expressions with holes in them, that enables them to be meaningfully transformed, in particular -converted and -reduced. In particular we generalize the set of -expressions to include holes, and on these generalized entities define -reduction (i.e., substitution) and filling so that these operations preserve -congruence and commute. The theory is then applied to allow the encoding of reduction systems and operational semantics of call-by-value calculi enriched with control, imperative and concurrent features. |
| |
Keywords: | -calculus" target="_blank">gif" alt="lambda" align="BASELINE" BORDER="0">-calculus contexts operational semantics theorem proving |
本文献已被 SpringerLink 等数据库收录! |
|