--- a/paper/abstract_eng.tex	Wed Feb 08 17:37:08 2017 +0900
+++ b/paper/abstract_eng.tex	Wed Feb 08 17:39:12 2017 +0900
@@ -9,5 +9,5 @@
 On the other hand method veriy programs with proofs.
 Proposition and proofs have isomorphic relation to typed $\lambda$ calculus by Curry-Howard Isomorphism.
 We define the CbC type system with subtype for proving CbC itself.
-Agda proves properties of translated CbC programs using proposed subtype definition.
+Dependent-typed language Agda proves properties of translated CbC programs using proposed subtype definition.
 \end{abstract_eng}