Reconciling positional and nominal binding

TL;DR

This paper introduces an extended lambda calculus that unifies positional and nominal binding mechanisms, enabling static and dynamic binding to coexist within a formal framework.

Contribution

It presents a novel formal system combining positional and nominal bindings, bridging static and dynamic binding paradigms in lambda calculus.

Findings

Formalizes coexistence of positional and nominal binding

Enables static and dynamic binding within a unified calculus

Provides theoretical foundation for mixed binding mechanisms

Abstract

We define an extension of the simply-typed lambda calculus where two different binding mechanisms, by position and by name, nicely coexist. In the former, as in standard lambda calculus, the matching between parameter and argument is done on a positional basis, hence alpha-equivalence holds, whereas in the latter it is done on a nominal basis. The two mechanisms also respectively correspond to static binding, where the existence and type compatibility of the argument are checked at compile-time, and dynamic binding, where they are checked at run-time.