TY  - JOUR
T1  - Locally-Named versus Nominal
AU - Lee, Gyesik AU - Kim, Hwajeong 
JO  - Journal of Engineering and Applied Sciences
VL  - 13
IS  - 19
SP  - 7878
EP  - 7883
PY  - 2018
DA  - 2001/08/19
SN  - 1816-949x
DO  - jeasci.2018.7878.7883
UR  - https://makhillpublications.co/view-article.php?doi=jeasci.2018.7878.7883
KW  - dependent families
KW  -proof assistants
KW  -variable binding
KW  -Mechanical formalization
KW  -parameters
KW  -experiments
AB  - 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.
ER  -