著者

Shin-ya Nishizaki

出版者

Research Institute forMathematical Sciences

雑誌

Publications of the Research Institute for Mathematical Sciences (ISSN:00345318)

巻号頁・発行日

vol.30, no.6, pp.1055-1121, 1994 (Released:2009-04-24)

参考文献数

15

被引用文献数

11

---

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.