University of Birmingham > Talks@bham > Bravo > May-must testing in PCF and beyond

May-must testing in PCF and beyond

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

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

Zoom details

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.