Calculi and Logic of Environment and Context

点击翻译按钮获取中文摘要

The aim of this research project was to construct calculi containing environments and contexts as first-class objects, and to study these calculi from a logical point of view. The main results are summarized as follows.・Calculi of first-class environments and contextsWe have developed calculus systems of environments and contents. Though environments and contexts are notions outside a formal system, we can handle environments and contexts as first-class objects in these systems. We have constructed the systems as formal type systems, and proved subject reduction, confluence, strong normalizability and conservativity of the systems.・Calculi of meta-variablesWe have developed calculus systems of meta-variables. In these systems, each variable is given a level, which classifies variables into object variables (level 0), meta-variables (level 1), metameta-variables (level 2) and so on. By this notion of level, we can treat textual substitution in these systems, and express insertion of programs into holes of contexts, which may generate new variable binding. We have shown that these systems also can express composition of contexts, which the systems above cannot. We have also proved subject reduction, confluence and strong normalizability. of the systems of meta-variables.