Simply typed lambda calculus with first-class environments (Q1894315)

Summary: We propose a lambda calculus \(\lambda^\to_{env}\) where it is possible to handle first-class environments. This calculus is based on the idea of explicit substitution, that is; \(\lambda \sigma\)-calculus. Syntax of \(\lambda^\to_{env}\) is obtained by merging the class of terms and the one of substitutions. Reduction is made from the weak reduction of \(\lambda \sigma\)-calculus. Its type system also originates in the one of \(\lambda \sigma\)-calculus. Confluence of \(\lambda^\to_{env}\) is proved by Hardin's interpretation method which is originally used for proving confluence of \(\lambda \sigma\)-calculus. We proved strong normalizability of \(\lambda^\to_{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.