Encoding Abstract Syntax without Fresh Names (Abstract)
This paper introduces a variant of nominal abstract syntax in
which bindable names are represented by normal meta-variables as
opposed to a separate class of globally fresh names. Distinct
meta-variables can be instantiated with the same concrete name,
which we call aliasing. The possible aliasing patterns are
controlled by explicit constraints on the distinctness (freshness)
of names. This approach has already been used in the nominal
meta-programming language αML. We recap that language and
develop a theory of contextual equivalence for it. The central
result of the paper is that abstract syntax trees (ASTs) involving
binders can be encoded into αML in such a way that
α-equivalence of ASTs corresponds with contextual
equivalence of their encodings. This is novel because the encoding
does not rely on the existence of globally fresh names and fresh
name generation, which are fundamental to the correctness of the
pre-existing encoding of abstract syntax into FreshML.