Constructs a logical-relations security model for where-declassification in higher-order languages by halting indistinguishability enforcement after relevant declassifications, yielding stronger guarantees than prior lower-order definitions.
In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
fields
cs.PL 2verdicts
UNVERDICTED 2roles
background 1polarities
background 1representative citing papers
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.
citing papers explorer
-
Compositional security definitions for higher-order where declassification
Constructs a logical-relations security model for where-declassification in higher-order languages by halting indistinguishability enforcement after relevant declassifications, yielding stronger guarantees than prior lower-order definitions.
-
Logical Relations for Session-Typed Concurrency
Extends logical relations to recursive session types for PSNI, proves soundness/completeness via biorthogonality with observation-index stratification, and gives an IFC refinement type system with secrecy polymorphism.