Reconciling positional and nominal 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...

Full description

Bibliographic Details
Main Authors: Davide Ancona, Paola Giannini, Elena Zucca
Format: Article
Language:English
Published: Open Publishing Association 2013-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1307.8207v1