May-must testing in PCF and beyond

Add to your list(s) Download to your calendar using vCal

• Ayberk Tosun (University of Birmingham)
• Wednesday 23 February 2022, 16:00-17:00
• LG23, Computer Science // Zoom.

If you have a question about this talk, please contact Tom de Jong.

Zoom details

• Link: https://bham-ac-uk.zoom.us/j/83640356951?pwd=M2c0LzRudFZ6dEJlZ0tnUzh0bFZZQT09
• Meeting ID: 836 4035 6951
• Password: 218

Abstract

In [Esc09], Martín Escardó investigates an extension of PCF with four powertypes that admit certain kinds of nondeterministic testing operators: the (1) Hoare, (2) Smyth, and (3) Plotkin powertypes, and (4) the probabilistic powertype. This language is regarded as an executable program logic for semidecidable properties and it is shown that this logic is semidecidable. This result is somewhat surprising in that must testing involves quantification over an infinite set of possible outcomes. Escardó obtains this result through the fact that the Cantor space is searchable and thus Escardó’s semidecidability result can be considered an application of his work on exhaustible and searchable sets [Esc08].

In this talk, we will provide a self-contained introduction to Escardó’s work on may-must testing in PCF and to the notion of a powerdomain that forms the basis of the semantic considerations that motivate Escardó’s augmentation of PCF with powertypes. Time permitting, we will briefly outline our planned thesis work in which we aim to construct an analogue of this result in the setting of total computation (as opposed to the partial setting of PCF ), using the Escardó-Xu topos (of sheaves over the “uniform-continuity site”), specifically, its subcategory consisting of C-spaces.

• [Esc08] Escardó, M.H. 2008. Exhaustible sets in higher-type Logical Methods in Computer Science. Volume 4, Issue 3, (Aug. 2008). DOI : https://doi.org/10.2168/LMCS-4(3:3)2008.
• [Esc09] Escardó, M.H. 2009. Semi-decidability of May, Must and Probabilistic Testing in a Higher-type Setting. Electronic Notes in Theoretical Computer Science. 249, (Aug. 2009), 219–242. DOI : https://doi.org/10.1016/j.entcs.2009.07.092.

This talk is part of the Bravo series.

This talk is included in these lists:

• Bravo
• LG23, Computer Science // Zoom

Note that ex-directory lists are not shown.