coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Final call for participation: LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025
Chronological Thread
- From: Andrei Popescu <andrei.h.popescu AT gmail.com>
- To: cl-isabelle-users <cl-isabelle-users AT lists.cam.ac.uk>, coq-club AT inria.fr, lean-user AT googlegroups.com, agda AT lists.chalmers.se
- Subject: [Coq-Club] Final call for participation: LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025
- Date: Thu, 9 Jan 2025 01:21:20 +0000
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=andrei.h.popescu AT gmail.com; spf=Pass smtp.mailfrom=andrei.h.popescu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f50.google.com
- Ironport-data: A9a23:PA3gCKMkiVgAqbDvrR0Mk8FynXyQoLVcMsEvi/4bfWQNrUoh32BRx mYYC2GAa6qCZ2enetolatvgoEoCucPUx9UyTHM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/vgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5OZYQXNNwJcaDpOtvra8EM355wehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGXFLiHM5tZuKXsfNKgS+8ksHmdr5 9kXfWVlghCr34pawZq+Q+how8khdYzlYdtZtXZnwjXUS/0hRPgvQY2QvY4ejGp23JkeW6uGD yYaQWIHgBDoahtDIFoWTpJ4hOCwi2L0bhVXrVuUoew85G27IAlZieCwYIeMJoTVLSlTtmqZj 0bnwGbdOAwxM/ay832H6HWAvvCayEsXX6pJSeTgqa806LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1i1oifBsENEHdVXFOI+5UeGza+8Dxul6nYsTWMbSPkFtOoMbDUP3 F6mxMzvIC5Kv+jAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj33ojqf4zQMaIYs3JJN3m/ 9ydQMEDa1g7iMcK0+C2/wmCjW/04JfOSQEx60PcWWfNAuJFiGyNNtXABbvztKkowGOlor+p4 iVsdy+2srxmMH11vHbRKNjh5Znwjxp/DBXSgER0A74q/Cm39niocOh4uW4lehw3a5xcJWWyO ic/XD+9ArcDbRNGiocnM+qM5zgCl/CI+SnND6+EPoQROMAZmPGvoHk0Ph7Jt4wSrKTcufpiY M/EIJjE4YcyBqNgwz67D+Yb2vlD+8zN7TK7eHwP9Dz+ieD2TCfNF98taQLSBshntv/siFuOq L53aZDVoyizpcWkM0E7B6ZIdQhSdRDWxPne96RqSwJ0ClA+Rjt8V66KnO1Jlk4Mt/09q9okN 0qVAidwoGcTT1WeQelTQik7M++9boU1tn8hIy0nMHCh3nVpM87l774Se9FzNfMr/fBqh6w8B fQUWdSyMtIWQBT++hMZccbcqq5mf0+Vng6gBXeuTwU+WJ9CfDb33OHYUDHhzwQwKxamlNAfp uSg3zzLQJBYSAVFCt3XWc2VzFiwnCY8nbtyVnTXPutsf1XIz7kzDgesiPVtcscGBije92HLy yeXHhYqiu3fqKAl8NTypP6lrqX4N8BcD0ZlD23gwrLuDhbj/02n2p1lfNeTWzLWREfY2fyFS 71O7vfeNPYnog57g7BkGew28ZNktsrdmbBK6y9FQlPJVg2PIZF9KCCk2cJviPV89oVBs1HrZ nPVq8hoApTXCsbLC1VLGREEaN6E3vQqmjX/y/Q5DUH5xS1v9oq8TkRgEEiQuRNZMYdKHtsp8 cU5tO4Szj6PuB4gH9KFryJTrkCnDHgLVYc5vZA7Xq7vrCcWyW95XJ+NMR+uvamzaOhNPHI6f R6Spq7J3IpHymT4LnEcKHnq3Mhmv6oohixk9lE4Ggm2qoL3vcNvhBx12hYrfztR1SRCgr5SO HA0FkhbJpeu3jZPhepFVV+CAwtqWR+ToBTw73Arl2TpaVaieUKQDW86OMeLpFs49UAFdBdl3 bio8kTXehe0Q9PQhwwZRlxAh8H4a+BI5inuuZyCDtuUOZsXeh/nifKeXnUJoB7ZHs8Bvk3Li u109uJWa6egFyovj4AkKoudx5ICYQulITFcfPRf4685J2HQVzWs0zyoKUrqWMdsJeTPwHCoG f5VOcNDeBSv5hmg9glBK/Y3HIZ1u/o16P4pWLDhfzcGuoTCiAtZisvb8yymiVI7R9lrr90GF brQUDC/CU2Vu2pfnj7cjctDO1fgW+I+Wi/H4LmX/tkKRrU5i8M9VWEp07CxgWeZDxs/wTKQo zH4RvH3y85M9N1SurXCQ4R5KSe6E9fRbNiz0RuSto1OZOzfMM2VuAIyrELmDjtsPrAQeopWk LiRgeHzx2fAmqg8aEHCupy7D6ISz96DbOlWFcPWLXdhgiqJXvH30SYD42yVLZ9okstXw8uaG y+UTdSWTsFMfftw31hXZDp6PzdHLp/of4HyoS+ZhNadOCg3iADoAouuyi70UDt9aCQNBazbN ib1nPSLvfVzs4VGAU4/NcFMWpNXDgfqZvo7SofXqzKdM2iPh2GCsJvEkT4Ly2nCKluAIfbAz aP1fDrMXzXsh/iQ1/BciZJ4gTMPBnUkgeUQQFMUy+Qrtx+EVlw5PcYvGrRYLKpLkx7C9oDyP xDMS2oANR/Tfxp5dTfE3dCyeTvHW8IvPI71KAV8qgnQI22zCZibCbRsyjZ47j0kMnH/xeWgM pcF9me2IhG1xYpzSP0O4uCgx91q3e7e2mlC7HWVfxYe2PrCKe5iOL1d8AtxuejvFsjMkADGJ zFwSz0cBk68TkH1HIBrfHs99NT1et/w521AUMtN6I+3V0anIClox/j2OuW12boGBCjPDKBbX mv5HgNh/EjPskH+esIVVxYBjqp9CPbNFc+/REMmqcv+gInoglka0wg+cebjgS3sFMOz078Qq 9V030UDOQ==
- Ironport-hdrordr: A9a23:Q6/gR6xMYA15yqA82Q4vKrPw5L1zdoMgy1knxilNoH1uA7Slfq WV9sjzuiWE7Qr5NEtQ++xoW5PwIk80l6QFhrX5VI3KNGLbUQCTXedfBOXZskTdMhy72ehHy6 96fqRyTPH2B0NrlNv37WCDf+oI8Z2o9OSGie/C02xgV2hRGsVdxjY8JALePEMefmd77FkCe6 Z0JPArm9NtQxUqhw2AZkU4Yw==
- Ironport-phdr: A9a23:o+V6Mx+a1sZd7P9uWQu1ngc9DxPPW53KNwIYoqAql6hJOvz6uci5Z QqGuagm1wSBdL6YwswHotKViZyoYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2/9YDfbx9ViDeyYb5+I xu7oAvMvcQKnIVuLbo8xRTOrnZUYepawn9mK0yOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ 7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8 qlmRAP0hCoBKjU09nzchM5tg6JBuB+uqBxxzYDXbo+IKvRxYrjQcskGSWdbRMtdSzBND4G6Y oASD+QBJ+FYr4zlqlYSqxuxGBOsC/3uyjRVnHH22rU63Po6EQ7awQwrAtUDv27SrNroLqcdT +G1wLPIzTnZd/NW3i/955bTch89vPGBRr1wcc/LxkkuEwPJlEmfqYvgPz6M0OkGrmeU4fZ6W +21l24ntx9+oiKpxso0hIfEm4YYx1DA+Clk3Io4KsG0RVB7bNOnH5ZdtSGUOYVrT84iTG9lu jo2xLIJtJO7fCUH1pAqyRHDZ/GJc4aF4hTuX/ufLzd/gXJqYrO/hxCq/Eikz+38TdO430xWo SZfj9nMtXYA3AHQ5MifUvZx4Fut1DKV2w3Q6uxIO144mbfYJpI7wrM8ipweulndEy/yhUX2l 7OWeVs++ua16uTmY6vpq4eAO4JylwrwKL4hmtalDuQ9KgUOX3aU+eC71LD7+E32WrRKjvkvn qbHspDWON0XpqC5DgNJyIoj5BG/DzCp0NQcg3YLNk5KeBWCj4TxOlHOJu73DeunjliyjDtmw +rKM77hD5nXMHTPjbTscax95kJA0AYzyMpQ55NQCrEPOvLzXUrxucTCAR8/LgO02fjoCNRn2 oMeQ26PGqiZMLvMvl+T+u0vPvKBZIAQuDnnKvgl4+TigmM+mV8YZaWp24AYZ2iiHvt6O0WZf WbsgtAZHGsXpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWH XfpcYWEQfYMZziILs9viDxXHYSmHoQlkBC1vQX3z75qa/fP9zcD/cbo0J10/OTZmBU2+HlpF MmHyEmJTnpohSUDTjpw1as5vE8rjh+I1rE9iPhFH/RS4elIW0E0L9qUy+FzDZXvQQ/bVtiOT 1miT9q8BiwpVZQ6xNpKK09yF9yKihHYwzHsCL8ck7mGHody6a+P8WL2IpNUzXrc2ahpt14+T 9BEKCXyj6hz7QXSQY6Pi0KBmr2haIwT2SfM8CGIym/Y7xIQaxJ5TaiQBSNXXUDRt9msvisqL perALUjaU5azNKab7BNcpvvhElHQ/HqPJLfZXiwkiG+H0XA3auCOaztfWhVxyDBEA4ciQlG9 HCKLwU/QCfnu2XGASdlCHrgZkrt9a91r3boBlQswVSyZlZ6n6Gw5gZTgPWdT/0J2bdRsSEts Th1Wlb7x9XOBsGLuiJueaxdZZU251IUnXnBuVlbOZqtZ7tnmkZYcwlzuBb20A5rD4xbjcUwh HYjzQ43JKDBlV0cL3WX2pf/PrCRIW73lPy2Q4jR3FyWkNOf+6NUre89t02mpwaxUEwr73Rg1 dBRlXqa/JTDSgQIA9r3VQ4s+h52qqu/AGF17p7I1XBqLai/syPTk9MvCuw/zx+8ftBZeKqaH Q72GsceCoCgMusv01SuaxsFOqhV+stWd4uvcfec1a/tPKB4myqrlm9ayI9420OIsSF7T6+A3 poIxe2ZwhrSTy313zLD+oj8nYFJYy1XH3Lqk3C1Qt4MIPcrLcBWUTTLQYX/3Nh1ip/zVmQN8 VeiAwhDw8q1YV+JaES72wRM1EMRqHjhmC2izjUynSt6y8jXlCHI3enmcwIKf2BRQ2w3x17qL ZK5jpYaGlCvdwUynwaN6kPzxqwdr6N6ZTq2Iw8Ab23tImduX7Hl/LOEb9RC6dUo9z1QSOmna k2yRbv0oh9c2CTmVTg7pnhzZ3ShvZP3mAZ/gWSWISNorXbXTsp3wA/W+N3WQfM5MiMufCBjk nGXA1G9O4Ls5tCIj9LYtfj4UWu9V5pVeC2tzIWatSL963c4SRG4mvmynJXgH21YmWfy0dVwW CSOrFDkZZHmzK+nGe1id0hsQlT77oJ2F5p/nY05mJwLkSJC19PFoDxdyDe1bI0T0LmbDjJFX TMRxt/J/AXpkFZuKH6E3cOxV3mQxNdge8jvZ2oX3iwn6MUZQKyQ7bFCgW50ug/i9VOXMaU7x G5Nj6Z2uxt4y6kTtQEgzzuQGOUXFEhcZmn3kgiQqsu5tONRbXqudr650Ax/m8qgBfeMuFI5O j6xd5E8ECt39sg6PkjL1Si544foYtTRK9JVrhqMngzLksBaLZswkrwBgi8tagef9TU1jvU2i xBjx8TwtY6LMWhsuqL/GhlAOyb+eusc/zjsieBVmcPcjOXNVt1xXz4MWpXvV/ehFjkf4O/mO wi5Gzo5sn6HGLDbEFzX+AJ8onnICZzuK2CPKSxT04B5XBfEbh864khcTHAgk5U+DAzv2MHxb BIz+GUK/lCh4hpUlrAzal+mAz+Z/lv3LG9zEsTXLQIKvF8eoR2OaorHsLo1R2YBr/jD5ESMM jDJOVoOVDlTHBTCXxe5ZvGv/YWSrbbeXLbvaauWJ+3J87QWVu/Ul831lNI6uW/dbIPXeSAya p9zkktbASImR4KAwWhJE2pP0HuTJ8+D+EXlon0x95/gtqStAEW1vMOOE+cAaIo0vUnn3eHbc bbX3XgcS34Q14tQlyWQmf5PgRhL0XEoL370TvwBrXKfFvuO3PIHSUdKMWUrc5IZp6MkglsXY JCd0IikkOUiyKZyUgYgNxSpjMitYYZiz3iVElTBCQ7LMb2HIWaO2MTreeanTqUWiuxIthq2s DLdEkn5Pz3FmSO7HxaoefpBii2WJnk88Mm0bwptBG7/TdnndgzzMdl5iiczyKE1gXWCPHAVM Dx1eUdA5rOK6iYQjvJ6Em1Hpn1rSIvM0z6e9PXdI40KvOFDBy11k6dX4i1/xeYNqi5DQ/Nxl W3Zqdsv61Cqn++TyyZ2BRpDrjEY4eDD9U5mOKjf6txBQSOepENLvTjWUU1a4YY9WbiN8+hKx 9PClbz+MmJH+tPQpo4HAtTMbdmAKDwnOAboHzjdCE0ESySqPCfRnR848rna+3uLo5w9spWpl oAJT+oRXVo5DP4bTEQjBNsaLYx8QxsrlLeaiIgD4n/0/3yzDI1K+4vKUP6fG6ClMDGCkbxNf AcF25v9JIUXc4D5gglsNwE8k4PNFE7dG9tKp2cyC2186FUI+394QGop3kvjYQ74+34fG8m/m Rsugxd/a+AgnN8Jy1gyL1vO4iA3lRtp8T0KqT+UeT/1aqy3WNMPY8IVn004M5e+TgQsKAPvx QprMzDLQ78XhLxlJzgDtQ==
- Ironport-sdr: 677f249c_4n3F8cmEengZkuHEHf/FceWqS0nk7KYIZoMBSSc97jGIh2r UIgsgcwt3OK4+7bQe37G9VvtDpdL2v7AMuK6x0A==
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
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://www.lms.ac.uk/civicrm/event/info?reset=1&id=139
Wednesday 15 January 2025, from 19:00 (GMT)
Online via Zoom
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), 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:
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.
For all queries regarding the seminar, please contact lmscomputerscience AT lms.ac.uk.
- [Coq-Club] Final call for participation: LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025, Andrei Popescu, 01/09/2025
Archive powered by MHonArc 2.6.19+.