Abstract
An encapsulated datatype collects related data together with the operations used to access them. Datatype refinement then provides a clear separation between the expectations of programs that call the operations (i.e. from outside the encapsulation) and the implementation of the operations themselves (inside the encapsulation), and it enforces consistency between the two.
In this paper we consider encapsulated probabilistic datatypes, i.e. those whose operations can “flip coins”; and we find as a result that the interface between calling programs’ expectations and their encapsulated probabilistic implementations must now provide consistency not only for functional properties but also for properties related to information flow.
In this paper we use a quantitative information-flow model for programs to give a sound basis for refinement of probabilistic datatypes.
| Original language | English |
|---|---|
| Title of host publication | Theoretical Aspects of Computing – ICTAC 2024 |
| Subtitle of host publication | 21st International Colloquium, Bangkok, Thailand, November 25–29, 2024, proceedings |
| Editors | Chutiporn Anutariya, Marcello M. Bonsangue |
| Place of Publication | Cham |
| Publisher | Springer, Springer Nature |
| Pages | 3-16 |
| Number of pages | 14 |
| ISBN (Electronic) | 9783031770197 |
| ISBN (Print) | 9783031770180 |
| DOIs | |
| Publication status | Published - 2025 |
| Event | 21st International Colloquium on Theoretical Aspects of Computing, ICTAC 2024 - Bangkok, Thailand Duration: 25 Nov 2024 → 29 Nov 2024 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 15373 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 21st International Colloquium on Theoretical Aspects of Computing, ICTAC 2024 |
|---|---|
| Country/Territory | Thailand |
| City | Bangkok |
| Period | 25/11/24 → 29/11/24 |