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...
Main Authors: | , , |
---|---|
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 |