Sciweavers

32
Voted
TLCA
2009
Springer

A Logical Foundation for Environment Classifiers

14 years 4 months ago
A Logical Foundation for Environment Classifiers
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fragments and variable declarations are annotated, and their scoping mechanism is used to ensure statically that certain code fragments are closed and safely runnable. In this paper, we investigate the Curry-Howard isomorphism for environment classifiers by developing a typed λ-calculus λ⊲ . It corresponds to multi-modal logic that allows quantification by transition variables—a counterpart of classifiers—which range over (possibly empty) sequences of labeled transitions between possible worlds. This interpretation will reduce the “run” construct—which has a special typing rule in λα —and embedding of closed code into other code fragments of different stages—which would be only realized by the cross-stage persistence operator in λα —to merely a special case of classifier application...
Takeshi Tsukada, Atsushi Igarashi
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where TLCA
Authors Takeshi Tsukada, Atsushi Igarashi
Comments (0)