A Type-Free Context Calculus

This paper develops a type free context calculus lxc. The calculus lxc includes contexts as first-class values andhole-filling as an explicit operation. In lxc holes arerepresented by ordinary variables and hole-filling is represented bythe usual application together with a new abstraction mechanism whichrepresents the variables intended to be bound after filling in thehole. We show that this calculus has desirable properties such asconfluence conservativity over lambda beta calculus and has thepreservation of strong normalization (PSN) property.This paper develops a type free context calculus lxc. The calculus lxc includes contexts as first-class values andhole-filling as an explicit operation. In lxc, holes arerepresented by ordinary variables and hole-filling is represented bythe usual application together with a new abstraction mechanism whichrepresents the variables intended to be bound after filling in thehole. We show that this calculus has desirable properties such asconfluence, conservativity over lambda beta calculus and has thepreservation of strong normalization (PSN) property