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

• Wydawca: IOS Press
• 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,