Аннотация:We propose a lambda calculus λ^→_{\mathit{env}} where it is possible to handle first-class environments. This calculus is based on the idea of explicit substitution , that is λ σ -calculus. Syntax of λ^→_{\mathit{env}} is obtained by merging the class of terms and the one of substitutions. Reduction is made from the weak reduction of λ σ -calculus. Its type system also originates in the one of λ σ -calculus. Confluence of λ^→_{\mathit{env}} is proved by Hardin's interpretation method which is originally used for proving confluence of λ σ -calculus. We proved strong normalizability of λ^→_{\mathit{env}} by reducing it to strong normalizability of a simply typed record calculus. Finally, we propose a type inference algorithm which produced a principal typing for each typable term.
