Reconciling positional and nominal binding

Davide Ancona, Paola Giannini, Elena Zucca

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 cal…