Gyesik  Lee, Hwajeong  Kim, 
    Locally-Named versus Nominal,
    Journal of Engineering and Applied Sciences,
    Volume 13,Issue 19,
    2018,
    Pages 7878-7883,
    ISSN 1816-949x,
    jeasci.2018.7878.7883,
    (https://makhillpublications.co/view-article.php?doi=jeasci.2018.7878.7883)
    Abstract: The main characteristic of our representation is the use of dependent families in defining expressions
such as terms and formulas. Another point is that we do not consider parameters and show that we can do the
same thing as when parameters are involved. In order to confirm the feasibility of our idea we made several
experiments using the proof assistant Coq.
    Keywords: dependent families;proof assistants;variable binding;Mechanical formalization;parameters;experiments