Simply Typed Lambda Calculus with First-Class Environments

Abstract

We propose a lambda calculus ${\lambda }_{env}^{\to }$ 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 }_{env}^{\to }$ 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 }_{env}^{\to }$ is proved by Hardin's interpretation method which is originally used for proving confluence of $\lambda \sigma$-calculus. We proved strong normalizability of ${\lambda }_{env}^{\to }$ 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.