ABSTRACT
We can categorize programming languages into two groups; one is a group of statically-typed programming languages and another that of dynamically- typed programming languages. Gradual typing enables us to integrate static and dynamic typing in a single programming language, which was proposed by Siek et al. They formalize gradual typing as the gradually typed lambda calculus, GTLC and gives cast insertion and the internal cast calculus, which are formulated cast-insertion technique in compiling programs in a gradually-typed programming language.
In this paper, we study gradual typing in the environment calculus, a lambda calculus with first-class environment. We propose a gradually typed environment calculus, a cast internal environment calculus, and cast insertion.
