# 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