Skip to Content.
Sympa Menu

coq-club - [Coq-Club] LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 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, agda AT lists.chalmers.se, lean-user AT googlegroups.com
  • Subject: [Coq-Club] LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025
  • Date: Mon, 16 Dec 2024 21:44:49 +0000
  • Authentication-results: mail2-smtp-roc.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-f53.google.com
  • Ironport-data: A9a23:IHbJ2qksD5EA718gJ6kpc0bo5gwvIkRdPkR7XQ2eYbSJt1+Wr1Gzt xJJX2GGOa2PNmbyeNxwaIjn/E5UucPSx99mHARtqiw0EFtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayazh8B56r8ks14K2o4W1A5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN1PXWAxPqcG6t9HGD9t/ O4jGBUnSBmq0rfeLLKTEoGAh+wmJcjveY4d4zRukGqfAvEhTpTOBa7N4Le03h9q3pEITauYP ZNJL2c0BPjDS0Un1lM/AZQyhuqpwHm5azpApUmeuII45mHSyEp6172F3N/9I43bGZQEzhjJz o7A13moDVZdMO6+9TWErnuQjMrotCHhfp1HQdVU8dYx3QTLmT1NYPEMbnOwpuD8gUqjUfpEO kkM82wvq7Iz/QqlVLHAswaQpXeFulsRWYMVHbBhrg6KzaXQ7kCSAW1soiN9hMIOlZ4XQj8Ay E+wr8q3JjV9i42wY1SU3+LBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zT8ZZafWlSVnNL yC2kcQou1kEYSc2O0iT+FnGh3ehpMGMQFNuoArQWW2h40VyY4vNi22UBbrzvKwowGWxFwbpU J04dy62srtm4XalynHlfQn1NOv1j8tpyRWF6bKVI7Ev9i6251modp1K7Td1KS9Ba5lfJWW5P xOC5VkPufe/2UdGi4cnPOpd7Ox6nMDd+SjND6G8gidmO8chJFHYpnkGibC4hDC0zhN3+U3AB XtrWZ3xVC5FWPoPIMueSOAa3rsmjiE4ziW7eHwI50XP7FZqX1bMEe1tGALWMIgRtfrYyC2Lq Yo3H5XRkH13DrauChQ7BKZJcTjm21BhWMiu86S6t4erfmJbJY3WI66Imul5J9Y+xcy4VI7gp xmAZ6OR83Kn7VWvFOlAQikLhGrHBM4k8SAILmY3MEy22nMuR4+q4e1NP9E0ZLQrvqgrh/J9U /BPKY3KD+VtWwb33W0XTaD8i4h+KzWtpwaFZBS+bBYFIpVPeg3u+/3fRDXJyhUgNCSNiJYBk +WS7T+DGZsnbCZ+PfnSc8Oqng+Qv2BCuedcXHnoA9h0eWfq+rdEMyba0/09eZkNDT7hxTKq8 RmcLjlFhOvKoq4zqMLog4LdpaiXMuJOJGhoNEiF0qSXbA7x4XiG7bJbdtqxbRTxdT/R6bqzQ +d41NT+O6A3p0lLuI9CDLpb96IyyN/xrbt8zA4/PnH0Q3m0K7FnMF+U9NJus/BT+7pnpgeGY EKD1d1EM7GvOsm+MlowJhIgX9uTx8MvhTjewvQkEnrUvBYt0uK8bnxTGB2QhAh2Drh/atoly Nh8nv8m0VW0jx5yP+uWiixRyX+3EUUBdKcarbAfPp7gj1s661NFYKGEMBTM3rO0V4xuPHUpc xiuv4iTo5RHx0HHTWg/KmiV48pZmqY1mU5ryH0sGg23v+Tr194N4Q1p0DUoTw5q4A1N/MBtN 0NKaUBkB6W80A15pcpEXmqTNRlLL0Sd807c12kLqX/9SkW2XDbBN18GZOSHphgY10l+fTFr2 q6S50i4cDTtfeD3hjATX2w8odPdbNVBzC/ws+H5INagAL87fmDDkIK1QGg19yvcHsI6gXPYq dlQ/OpfbbPxMQgSqfYZD7a2+KsxShfeAkB/WtBkob00GF/DdAGI2TShL167fuVPLafo9W66E 8lfGdJdZS+h1SqhriEpOoBUGuVaxMUW3dslfq/nAUUksLHF9zpgj8/2xxjE3WQuR41jrNY5J obvbAm9K223h0ZPumrzvcJBa3uZY94FWVXG59qL0t41TrANjOI9VnsJ8OqQn26UOw5Z7R6rr Fv9R6vJ/ddDl6VovaXRS5tmOSvlCOndduqy9CKLj+9vdvLKaMfHiBMUoALoPiNQJrogZO50n rWs7v/y0F/0g7Itd2X/hZO6NrJo4P+qV7F9KfPHL3h9nAqDVvTz4hAFxXuKFJxRnP5Z5eilX wGdavbsUfIwRPFm2yRzRwVFNhQSGYDbT/3FnjysieaIBjw28x31HPn++VDHNWhkJzI1YbvgA QrKitOSz9F/rqEXITQbBvtjUqRKEHW6VYQIL9TO5CSlVE+2iVa/u5znpxoqyRfPLlKmSM/aw 5b0diLSRSSImpPj7Y9m6tRpnxgtEnxCr/E6fRsd9/5ImjmKNjM6AtpHA6oWKKN/s3LU7475V gHvfWF5KCTaXBZ4SzvezunnfD+iAr0pBo+kCB0vpk+aUnLjTsfISr5s7Txp7HpKayPuhrPvY 80X/nrreAO92Nd1TOIU/ea2mvpj2uic/H8T5EThiIbnNn7y21nROKBJR2KhlBArEv0hUG3OL GkxAG1GGQS1FBW3HsFndHpYXhoeuVsDCtnugTinmL7iV0ezlYWsC8ET/8n817QCaIIBI7tmq bbfWT6W+27PspAMkfJBhj/q6JOYzdqEG8G7KOnoQgh6c2RcLIg4F5tqoBfjh/3ONOKS/50xW 9VsD7UD6Jy5FX1s
  • Ironport-hdrordr: A9a23:7/ljdqjf4+Ray9o88RipcAKHs3BQXv8ji2hC6mlwRA09TyX4rb HWoB1/73XJYVkqKRQdcLy7Scu9qBDnhP1ICOsqTNOftWDd0QPCEGgI1/qE/9SPIVyZysdtkY hnaLZ3E9D9ABxXiszg8BCkH9tI+rW62ZHtq+Ob4XkFd29XgmJbgDuRyDz3LqS7fmh77FMCdK ah2g==
  • Ironport-phdr: A9a23:XFacQRT3J0h3olff/Z8EJNNujNpsoqGWAWYlg6HPa5pwe6iut67vI FbYra00ygOSBMOKsLkd1rae8/i5HzBbudDZ6DFKWacPfiFGoP1VpTBoONSCB0z/IayiRA0BN +MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55I AmroQnLucQbj5ZuJrw1xxbHrXdEZuRbyGx1Ll6Xgxrw+9288ZFt/ihMof4t69JMXaDndKkkU LJUCygrPG8y6MD3rxfPSheB6GUBWWsMiBpIBAbF7BD+Xpjvtybxq/Rw1iqHM8DoVL44QTut4 btlRx/ukycHKiU28HrLhcxqjaJUuwyuqhpiyIPJeo6VNf5+fqTAfdMGQGdKQ8hcWzBdDo66c oACCfcKM+RFoInnv1YBohuwCwevCu3y1DFHmmT70rcm3+k7CwzKwBAsEtAIvX/JrNv1LqASU eWtwaTUyzXMculW1in86IPVaB4hpumMUqxrccXN1EkkCgTIgU+WqYP4JTOayOUNv3Kb7+Z6T eKvjHYnpB9qojez28chkYbJhocPxVDF8SV12po6Jdq9SENiZ9OvDZRfuT2AOYRsXsMiX39nu Dw8yrAeuJO3YSgExZYmyhLBdfGJfYuF7BLsWeqNLjp1hm9oday/ihu27ESs1PPwW9Sq3VtWo CRIk8fBumwN2hHR5cWLV/1w9Vqv1zaI0gDc8OBEIUYsmKrfLp4h2aQ8mYAPvkjZAy/2m136g 7SKeUU/4OSo7P7nYrrgq5SBNIF0khnzProylsG7G+g1MQgDU3KF9eih17Dv5030TbtMg/Yrj KTZtI3aJd8HpqGnGQ9bz4cj6hehADq+zNgVm2QMIkhfdxKdlYfpPknDIPDmAve7hFShiDJry OrHPr3lG5nCMHrDnKr4cbZz60NRxhA/zd9Y55JTBbEBJOz8VlXtu9zfCx81Kw20w+D5B9Vhz o4SR36DD6uDPK7RsVKE/PwjL/SPaYMPuDvwJeAp5/v0gn84nV8dc7Op3ZwSaH2gBPtmJViWY WDyjdcAC2sKvhAyTPTtiF2aTzFTfGq9X78n6zE0DYKpF4bDRoS3jLOd2ye7G4VaZmZdBV+UC 3fna52EW+sQaCKVOsJtjyQIVaK9RI85yRGuqAj6xqJ7IerT4y0UrI7s1Nxo5+LIjhwy7jx1D 8GF026XVW10n2UIRyU33K9lu0B9xE2DguBEhKlTEZlS/PpDXwM+ONvB1OFgEJimUQaEf8yAQ luiRtjjHCo8VMkZx94Vf107ENynyBnImTepVftdnLuSQZcw76j03n7rJs87xWyCnKAug1AOR spUKXbgja528w3eHZWPiEjd36KnfKJZwTXA7k+Mym2BuExXSgltSb6DVncaNWXMqtGsz0XOV bKvQYwgKgZawtPKfqJMZsfkjBNGAu/kINnFaH+ZlGK5BBLOzbSJOtm5M14B1TnQXRBX2zsY+ myLYFBW7kaJpmvfCGYrDlfzewb29uI4rnqnT0gyxgXMbkt71rPz9ARGzeeERaY12bQJ8Dwkt y0yBEy0itvQB8CNpkxhOr1bed4m60pv2mfQtgg7NZulfOh5nlBLSw1spAv10glvTIBJkMwkt nQvmQN0JbiV0RVBMSufxZ3rMaD/JWz7/RTpYKnTiRnFyNjD3KAJ5bwjrkn7+gGkEk1363J8z 9xcyGeR/L3PBQsWFJ/zCwM5qkM8qLbdbS0woYjT0BWAKIGStTnPk5IsDeohkFO7estHdbmDH 0n0GtEbAM6nLKornUKoZ1QKJrIa8ql8JM6ge/acvczjdO99gDKri3hG64FhwwqN8SR7UOvBw 5cCxbmRwAKGUz72iFrpvNrwnMhIYjQbH2z3ziaBZsYZb6t+Z4sKT2foO8qvy851mrbiXndZ8 BioAFZHkM6ldByObkDsiBVK3BdywzTvki+5wjpo1jAx+/DHjWqenqK4LUpBZzUYIQsqxU3hK oW1kd0ACU2hbgxz0QCg+V6/3a9Q4qJ2M2jUR05MOSnwNWBrFKWq5d/gK4ZC7o0ltSJPXaGye 1efH/T0pRcA3iKlHy1Gwyg2bDq3kpr8lh1+zmmaKTwgyRiRMdE13hrZ6NHGELRY2DYcSSg+i X/PAUCxJNK01dqRnpbH9Ou5UijyM/8bOTmuxoSGuiyh4GRsChDqhPG/lOrsFg0i2DP63d1nP cnRhC71eZKjl6GzMOY9O1JtGEe58c1xXId3joo3gpgUn3kcnJScu3Qdwy//NtBS2KS2a3RoJ 3ZDytjZ+gXknk0lNnWRypnyS12Sx8JgY5+xZWZe1i8m7s9MAbuZ9/QexXoz8gf+91uBJ6Um1 j4GrJlmoGYXmeQIpBYgwm2GD7YeEFMZdS3gmhKU7syv+aBeZWKha7+1hwJ1mdGsCq3HoxkJA i6oPMd/W3UpvoMiawGpsjW78IzvddjOYMhGsxSVl02FlO1JMNcrkfFMgyN7OGX7tHljyughj BUo04vp2erPY2hr4q+9BQZVczPvYMZGsDjrgbxTn4CWmZioBph6ESgjU57hTPbuGzUX/6eCV U7GAHgnp3GXFKCKVwaZ5F1rrjTPVYisL3yML2QxwtBrRR3bL0taylNxPn1yjtsyEQakw9bke UFy62UK51L2nRBLz/phKxj1VmqM7BftcDo/T4KTaQZH9gwXrVmAKtSQt6ggekMQto3ktgGGL XaXIhhFHX1cEFLRHEjtZ/Gv/YWSqLXeX7vmaaGSPvPW7rYCH/aQmcDxjs08pG3Kb5vXeCElV qxeuAILXGglSZqH3WxXEWpP0XqKNZbTpQ/gqHMp6JrjobK7AES3otHXQ7pKbYcwoVbv3eHaZ rTW3GEgeVM6ntsN3SOal+RZhQRPzXkoL370T/wBrXKfFfqA3PYIUFhLLXs0bpIA7rpgjFASY oiC24+zjvggyadrbjUNHV35xpPzPZ1Mczz7bQmXQh7MbevOJCWXkZuuP+XhGfsJ3b8S71rp6 H6aCxOxZG3d0WOyBlb0a6cUy3jKWX4W8Je0dhInYYT6ZPThbBDzcNp+jDlshKYxmmuPL2kXd z51b0JKqLSUqyJemPR2XWJbvDJjKqGfliCV4vO9SN5euOZ3Ailyi+NR4Wgrg7pT4iZeQfVpm SzU5tdwqlCim+OLx3JpSh1L4jpMgYuKuw1lN8C7vtFYXm3Y+RsW8WiKIxEDpt8gB9+2/q4Nk Z7Ak6X8LDoE+NXRvIMdC8XSNMObIS8hPB7uS1u2REMOST+mM32ahlQIyqnDsC3I6MJj+t6xw 8lrKPcTTlE+G/IEB14wGdUDJM0yRTY4ifuBi8VO43OirR7XTcEcv5bdV/vUD++8TVTRxbRCe RYMxqv1aIoJMYiukUVkZkN3ncLKXVLXRd1WqTBJYQo9oUEL+397BD5WuQqteka27XkfGOTh1 AYxkRd7aP8x+S3E5l42Ih/HpnJ1nhRq39rihj+VfXj6K6L6DuQ0Q2Lk8kM2NJ38WQN8awa/y FdlODnzTLVUl7J8dGpvhWc0VrNAHPddSetPZxpCnJl/ht0t2FVY7yilnApJuLCDBpxlmw8nN 5WrqiAYs+qGRNEwLK3UYqFOywoI7p8=
  • Ironport-sdr: 67609f5d_AIJ/9rXzE5zHxvR2Bpq/4X6uqprjGG6nt9MvPGmds5IVid2 VwX81y0n1934ijkcr2iZ/xgq+3Inx4FDgM8H89w==

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.

 

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.



  • [Coq-Club] LMS/BCS-FACS Online Seminar, Annabelle McIver, 15 January 2025, Andrei Popescu, 12/16/2024

Archive powered by MHonArc 2.6.19+.

Top of Page