JournalsprimsVol. 30 , No. 6DOI 10.2977/prims/1195164948

Simply Typed Lambda Calculus with First-Class Environments

  • Shin-ya Nishizaki

    Okayama University, Japan
Simply Typed Lambda Calculus with First-Class Environments cover


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.