Explicit environments

• Autorzy: Sato, M , Sakurai, T. , Burstall, R.
• Języki publikacji: EN

Abstrakty

EN

We introduce le, a simply typed calculus with environments as first class values. As well as the usual constructs of l and application, we have e\lbrack\lbrack a\rbrack\rbrack which evaluates term a in an environment e. Our environments are sets of variable-value pairs, but environments can also be computed by function application and evaluation in some other environments. The notion of environments here is a generalization of explicit substitutions and records. We show that the calculus has desirable properties such as subject reduction, confluence, conservativity over the simply typed lb-calculus and strong normalizability.

Słowa kluczowe

EN

explicit environments; simply typed calculus; confluence; conservativity; strong normalizability

• Czasopismo: Fundamenta Informaticae
• Rocznik: 2001
• Tom: Vol. 45, nr 1,2
• Strony: 79-115
• Opis fizyczny: bibliogr. 21 poz.

Twórcy

autor

Sato, M

autor

Sakurai, T.

autor

Burstall, R.

• Graduate School of Informatics, Kyoto University, Kyoto, Japan,