We propose a lambda calculus λ→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 λ→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 λ→env is proved by Hardin's interpretation method which is originally used for proving confluence of λ σ-calculus. We proved strong normalizability of λ→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.
Cite this article
Shin-ya Nishizaki, Simply Typed Lambda Calculus with First-Class Environments. Publ. Res. Inst. Math. Sci. 30 (1994), no. 6, pp. 1055–1121DOI 10.2977/PRIMS/1195164948