5 papers
Logical Relations for Session-Typed Concurrency
Stephanie Balzer, Farzaneh Derakhshan, Robert Harper +1
Program equivalence is the fulcrum for reasoning about and proving properties of programs. For noninterference, for example, program equivalence up to the secrecy level of an obser…
Mechanizing a Proof-Relevant Logical Relation for Timed Message-Passing Protocols
Tesla Zhang, Asher Kornfeld, Rui Li +3
Semantic typing has become a powerful tool for program verification, applying the technique of logical relations as not only a proof method, but also a device for prescribing progr…
A Language-Agnostic Logical Relation for Message-Passing Protocols
Tesla Zhang, Sonya Simkin, Rui Li +2
Today's computing landscape has been gradually shifting to applications targeting distributed and *heterogeneous* systems, such as cloud computing and Internet of Things (IoT) appl…
Semantic Logical Relations for Timed Message-Passing Protocols (Extended Version)
Yue Yao, Grant Iraci, Cheng-En Chuang +2
Many of today's message-passing systems not only require messages to be exchanged in a certain order but also to happen at a certain \emph{time} or within a certain \emph{time wind…
Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency
Farzaneh Derakhshan, Stephanie Balzer, Yue Yao
Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. Information flow control (IFC) type systems assert noninterference by tracking the l…