Search

• < Previous
• 1
• Next >

---

Proving Noninterference by a Fully Complete Translation to the Simply Typed lambda-calculus

Naokata Shikuma ; Atsushi Igarashi.

Tse and Zdancewic have formalized the notion of noninterference for Abadi et al.'s DCC in terms of logical relations and given a proof of noninterference by reduction to parametricity of System F. Unfortunately, their proof contains errors in a key lemma that their translation from DCC to System F&nbsp;[&hellip;]

---

A Logical Foundation for Environment Classifiers

Takeshi Tsukada ; Atsushi Igarashi.

Taha and Nielsen have developed a multi-stage calculus {\lambda}{\alpha} 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&nbsp;[&hellip;]

---