Noninterference through Bisimulation

April Tune; Wendy Yang; G. A. Kavvos

doi:10.1007/978-3-031-99751-8_11

Noninterference through Bisimulation

April Tune^*, Wendy Yang, G. A. Kavvos

^*Corresponding author for this work

School of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

13 Downloads (Pure)

Abstract

Noninterference properties state that data does not flow in an undesirable manner, e.g. from a high-security to a low-security setting. Within programming languages noninterference is often enforced through the use of modal type systems. Proving the property often requires non-trivial techniques, such as denotational semantics or logical relations. We show that a simple bisimulation technique (due to Choudhury, Eades, and Weirich) can be adapted to show noninterference for a variety of modal type systems

Original language	English
Title of host publication	Trends in Functional Programming
Subtitle of host publication	TFP 2025
Editors	Jeremy Gibbons
Place of Publication	Cham
Publisher	Springer, Cham
Pages	259-280
Number of pages	22
ISBN (Electronic)	978-3-031-99751-8
ISBN (Print)	978-3-031-99750-1
DOIs	https://doi.org/10.1007/978-3-031-99751-8_11
Publication status	Published - 5 Oct 2025
Event	26th International Symposium on Trends in Functional Programming - Department of Computer Science, University of Oxford, Oxford , United Kingdom Duration: 14 Jan 2025 → 16 Jan 2025 https://trendsfp.github.io/2025/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer, Cham
Volume	15652
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Symposium on Trends in Functional Programming
Abbreviated title	TFP 2025
Country/Territory	United Kingdom
City	Oxford
Period	14/01/25 → 16/01/25
Internet address	https://trendsfp.github.io/2025/

Bibliographical note

Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Research Groups and Themes

Programming Languages

Access to Document

10.1007/978-3-031-99751-8_11

Full-text PDF (accepted manuscript)
This is the accepted author manuscript (AAM) of the article which has been made Open Access under the University of Bristol's Scholarly Works Policy. The final published version (Version of Record) can be found on the publisher's website. The copyright of any third-party content, such as images, remains with the copyright holder.
Accepted author manuscript, 184 KBLicence: CC BY

Handle.net

Persistent link

Cite this

@inproceedings{272384950efd416c9a8b1b70eaed40f1,

title = "Noninterference through Bisimulation",

abstract = "Noninterference properties state that data does not flow in an undesirable manner, e.g. from a high-security to a low-security setting. Within programming languages noninterference is often enforced through the use of modal type systems. Proving the property often requires non-trivial techniques, such as denotational semantics or logical relations. We show that a simple bisimulation technique (due to Choudhury, Eades, and Weirich) can be adapted to show noninterference for a variety of modal type systems",

author = "April Tune and Wendy Yang and Kavvos, \{G. A.\}",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.; 26th International Symposium on Trends in Functional Programming, TFP 2025 ; Conference date: 14-01-2025 Through 16-01-2025",

year = "2025",

month = oct,

day = "5",

doi = "10.1007/978-3-031-99751-8\_11",

language = "English",

isbn = "978-3-031-99750-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer, Cham",

pages = "259--280",

editor = "Jeremy Gibbons",

booktitle = "Trends in Functional Programming",

address = "Switzerland",

url = "https://trendsfp.github.io/2025/",

}

TY - GEN

T1 - Noninterference through Bisimulation

AU - Tune, April

AU - Yang, Wendy

AU - Kavvos, G. A.

PY - 2025/10/5

Y1 - 2025/10/5

N2 - Noninterference properties state that data does not flow in an undesirable manner, e.g. from a high-security to a low-security setting. Within programming languages noninterference is often enforced through the use of modal type systems. Proving the property often requires non-trivial techniques, such as denotational semantics or logical relations. We show that a simple bisimulation technique (due to Choudhury, Eades, and Weirich) can be adapted to show noninterference for a variety of modal type systems

AB - Noninterference properties state that data does not flow in an undesirable manner, e.g. from a high-security to a low-security setting. Within programming languages noninterference is often enforced through the use of modal type systems. Proving the property often requires non-trivial techniques, such as denotational semantics or logical relations. We show that a simple bisimulation technique (due to Choudhury, Eades, and Weirich) can be adapted to show noninterference for a variety of modal type systems

U2 - 10.1007/978-3-031-99751-8_11

DO - 10.1007/978-3-031-99751-8_11

M3 - Conference Contribution (Conference Proceeding)

SN - 978-3-031-99750-1

T3 - Lecture Notes in Computer Science

SP - 259

EP - 280

BT - Trends in Functional Programming

A2 - Gibbons, Jeremy

PB - Springer, Cham

CY - Cham

T2 - 26th International Symposium on Trends in Functional Programming

Y2 - 14 January 2025 through 16 January 2025

ER -

Noninterference through Bisimulation

Abstract

Publication series

Conference

Bibliographical note

Research Groups and Themes

Access to Document

Handle.net

Fingerprint

Cite this