Mechanized logical relations for termination-insensitive noninterference

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review


We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic model of this type system and show that well-typed programs satisfy termination-insensitive noninterference. Our semantic approach supports compositional integration of syntactically well-typed and syntactically ill-typed-but semantically sound-components, which we demonstrate through several interesting examples. We define our model using logical relations on top of the Iris program logic framework; to capture termination-insensitivity, we develop a novel language-agnostic theory of Modal Weakest Preconditions. We formalize all of our theory and examples in the Coq proof assistant.

Original languageEnglish
Article number10
JournalProceedings of the ACM on Programming Languages
Publication statusPublished - Jan 2021

Bibliographical note

Funding Information:
This work was supported in part by a Villum Investigator grant (no. 25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation. Amin Timany was a postdoctoral fellow of the Flemish research fund (FWO) during parts of this project.

Publisher Copyright:
© 2021 Owner/Author.

Copyright 2021 Elsevier B.V., All rights reserved.

    Research areas

  • Information-Flow Control, Iris, Logical Relations, Program Logics

See relations at Aarhus University Citationformats

ID: 208206520