Sciweavers

Share
FLOPS
2001
Springer

A Simply Typed Context Calculus with First-Class Environments

8 years 7 months ago
A Simply Typed Context Calculus with First-Class Environments
We introduce a simply typed λ-calculus λκε which has both contexts and environments as first-class values. In λκε, holes in contexts are represented by ordinary variables of appropriate types and hole filling is represented by the functional application together with a new ion mechanism which takes care of packing and unpacking of the term which is used to fill in the holes of the context. λκε is a conservative extension of the simply typed λβ-calculus, enjoys subject reduction property, is confluent and strongly normalizing. The traditional method of defining substitution does not work for our calculus. So, we also introduce a new method of defining substitution. Although we introduce the new definition of substitution out of necessity, the new definition turns out to be conceptually simpler than the traditional definition of substitution.
Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyam
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where FLOPS
Authors Masahiko Sato, Takafumi Sakurai, Yukiyoshi Kameyama
Comments (0)
books