2009 | OriginalPaper | Buchkapitel
A Logical Foundation for Environment Classifiers
verfasst von : Takeshi Tsukada, Atsushi Igarashi
Erschienen in: Typed Lambda Calculi and Applications
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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. We prove that
λ
⊳
enjoys basic properties including subject reduction, confluence, and strong normalization and that the execution of a well-typed
λ
⊳
program is properly staged. Finally, we show that the proof system augmented with a classical axiom is sound and complete with respect to a Kripke semantics of the logic.