A Second Order Typed Context Calculus

概要

論文の詳細を見る
In this paper we introduce a second order context calculus λ_<2xc> which has context as a first-class object and hole-filling as an explicit operation. In the representation of contexts, both the term variable and the type variable can get bound after filling in the hole. In our calculus, the holes of the contexts are represented by ordinary variables of appropriate types and hole-filling is represented by the usual application together with a new abstraction mechanism which represents the variables intended to be bound after filling in the hole. In order to avoid the unwanted-capture of variables during substitution, the push and pull techniques are used to rename free variables instead of the usual α-conversion which renames bound variables to avoid the unwanted capture of the free variables. A general definition for the push operator is introduced to avoid repeating essentially the same definitions for similar cases. We show that our calculus is confluent and the type system has the subject reduction property.
社団法人情報処理学会の論文
2001-07-15