[TYPES/announce] Final call for participation: LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025 Inbox

[Andrei Popescu]

LMS/BCS-FACS Seminar 2025

Wednesday 15 January 2025, from 19:00 (GMT)
Online via Zoom

https://urldefense.com/v3/__https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2025__;!!IBzWLUs!QD-oxfpCh6yAzaBOB-xpTkCq8a2uC6ypUsUGN3pVby4C5xx_166xNkTZReO_GZjoJV1IFTolTkr1zR-YV7-V0QJicd8F9yDBm9D13Bx6$ 

In association with the British Computer Society Formal Aspects of
Computing Science (BCS-FACS), the LMS hosts an annual online seminar on
aspects of the computer science–mathematics interface. These events are
free to anyone who wishes to attend and have attracted high-quality
speakers. We are happy to have this verification talk from a wonderful
speaker just one day after World Logic Day.

Speaker:

Annabelle McIver (Macquarie University)

Probabilistic Datatypes: automating verification for abstract probabilistic
reasoning

Abstract:

Datatypes - in which data is encapsulated together with methods that access
it - play an important role in the organisation of large software projects.
Correctness of datatypes has traditionally been carried out using
simulation relations to simplify the verification by separating concerns:
the datatype can be verified independently from the programs that use it,
whilst those programs themselves can be verified using the specifications
of the datatype's methods. Use of these principles enables complex programs
to be brought within reach of automated proof.

When probabilistic choice is included, however, it turns out that obtaining
similar simplifications of the verification problem will require
distinguishing between "hidden" and "observable" probabilistic behaviour -
if demonic choice is allowed in the surrounding program. And that is not
required in the non-probabilistic setting: the crucial issue is the
potential interaction of probabilistic- and demonic choice.

In the main part of this talk I will use examples to explain why the
interaction is problematic, and I will suggest how extension of existing
pGCL-based automated reasoning-tools, will by taking that interaction into
account, enable automated probabilistic abstract reasoning about "hard to
crack" probabilistic programs.

Registration:

To attend remotely via Zoom, please complete the registration form here:

https://urldefense.com/v3/__https://www.lms.ac.uk/civicrm/event/info?reset=1&id=139__;!!IBzWLUs!QD-oxfpCh6yAzaBOB-xpTkCq8a2uC6ypUsUGN3pVby4C5xx_166xNkTZReO_GZjoJV1IFTolTkr1zR-YV7-V0QJicd8F9yDBm8Pn1SNv$ 

You will receive the link to the meeting upon registration, as well as an
automated reminder email sent 24 hours before the event is scheduled to
start.

For all queries regarding the seminar, please contact
lmscomputerscience at lms.ac.uk.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20250109/4ef9288d/attachment.htm>