Reconciling positional and nominal binding
This work addresses a foundational issue in programming language theory for researchers and developers, though it appears incremental as it builds on existing lambda calculus frameworks.
The authors tackled the problem of reconciling positional and nominal binding mechanisms in lambda calculus by defining an extension where both coexist, with positional binding corresponding to static binding and nominal binding to dynamic binding.
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.