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.