Quasi-Open Bisimilarity with Mismatch is Intuitionistic

Horne, Ross James; Ahn, Ki Yung; Lin, Shang-wei; Tiu, Alwen

doi:10.1145/3209108.3209125

Reference : Quasi-Open Bisimilarity with Mismatch is Intuitionistic


	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	Focus Areas :	Computational Sciences
	To cite this reference:	http://hdl.handle.net/10993/37429

Title :	Quasi-Open Bisimilarity with Mismatch is Intuitionistic
Language :	English
Author, co-author :	Horne, Ross James [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
	Ahn, Ki Yung []
	Lin, Shang-wei []
	Tiu, Alwen []
Publication date :	2018
Main document title :	Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18)
Publisher :	ACM
Pages :	26-35
Peer reviewed :	Yes
Audience :	International
City :	New York
Country :	USA
Event name :	LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Event date :	July 9-12, 2018
Event place (city) :	Oxford
Event country :	United Kingdom
Abstract :	[en] Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity allows fresh names to be manufactured to provide constructive evidence that an inequality holds. The extension of quasi-open bisimilarity is canonical and robust --- coinciding with open barbed bisimilarity (an objective notion of bisimilarity congruence) and characterised by an intuitionistic variant of an established modal logic. The more famous open bisimilarity is also considered, for which the coarsest extension for handling mismatch is identified. Applications to checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella.
Permalink :	http://hdl.handle.net/10993/37429
DOI :	10.1145/3209108.3209125

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	lics.pdf		Publisher postprint	726.24 kB	View/Open

All documents in ORBi^lu are protected by a user license.

University of Luxembourg Library | Feedback | Legal notices