Simply Typed Lambda Calculus with First-Class Environments

  • Shin-ya Nishizaki

    Okayama University, Japan


We propose a lambda calculus where it is possible to handle first-class environments. This calculus is based on the idea of explicit substitution, that is -calculus. Syntax of 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 is proved by Hardin's interpretation method which is originally used for proving confluence of -calculus. We proved strong normalizability of 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–1121

DOI 10.2977/PRIMS/1195164948