[Agda] LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025

[Andrei Popescu]

*LMS/BCS-FACS Seminar 2025*


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

*https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2025
<https://www.lms.ac.uk/events/lms-bcs-facs-seminar-2025>*



In association with the British Computer Society Formal Aspects of
Computing Science (BCS-FACS <http://www.bcs.org/server.php?show=nav.12459>),
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.



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://www.lms.ac.uk/civicrm/event/info?reset=1&id=139>. 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.chalmers.se/pipermail/agda/attachments/20241216/7cc7b83c/attachment.html>