# Simply Typed Lambda Calculus with First-Class Environments

### Shin-ya Nishizaki

Okayama University, Japan

## Abstract

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–1121

DOI 10.2977/PRIMS/1195164948