Abstract

Following the dependently typed intermediate language that we presented previously, in this talk, we continue to introduce its theoretical properties. We will show that explicit type conversion makes it possible to achieve decidable type checking without normalization. This also ensures the feasibility of allowing non-termination in the language. Finally we discuss the left question last time about the related work by comparing our language with other similar ones.