Explicit substitutions for objects and functions

Authors: Delia Kesner Pablo E Martínez López

Publish Date: 1998/9/16

Volume: , Issue: , Pages: 195-212

PDF Link

Abstract

This paper proposes an implementation of objects and functions via a calculus with explicit substitutions which is confluent and preserves strong normalization The source calculus corresponds to the combination of the ςcalculus of Abadi and Cardelli AC96 and the λcalculus and the target calculus corresponds to an extension of the former calculus with explicit substitutions The interesting feature of our calculus is that substitutions are separated — and treated accordingly — in two different kinds those used to encode ordinary substitutions and those encoding invoke substitutions When working with explicit substitutions this differentiation is essential to encode λcalculus into ςcalculus in a conservative way following the style proposed in AC96

Keywords: