Definition
Nameful scoping is an approach to well-scoped syntax with binders in which variables are represented directly by names and binders store those names explicitly.
Terms are usually identified up to alpha equivalence, so changing the name of a bound variable does not change the represented term.
Example
The term is represented using those names directly. Equality and substitution therefore need explicit side conditions about freshness and variable capture.
Related Concepts
Lexical Scope
Alpha Equivalence
Structural Substitution
De Bruijn Indices
Higher-Order Abstract Syntax
Nominal Sets
Variable