We propose a locally nameless representation for Launch-bury's natural semantics for lazy evaluation. Names are reserved for free variables, while bound variable names are replaced by indices. This avoids the use of α-conversion and Barendregt's variable convention, and facilitates proof formalization. Our definition includes the management of multi-binders to represent simultaneous recursive local declarations. We use cofinite quantification to express the semantic rules that require the introduction of fresh names, but we show that existential rules are admissible too. Moreover, we prove that the choice of names during the evaluation of a term is irrelevant as long as they are fresh enough.
展开▼
