coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Applications to medicine

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>, Julio Rubio <julio.rubio AT unirioja.es>, Jónathan Heras <jonathan.heras AT unirioja.es>
Cc: cl-isabelle-users AT lists.cam.ac.uk, metamath AT googlegroups.com
Subject: Re: [Coq-Club] Applications to medicine
Date: Fri, 3 Aug 2018 15:12:46 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f52.google.com
Ironport-phdr: 9a23:hXosrxdoULHiJvFM7evVpsS/lGMj4u6mDksu8pMizoh2WeGdxcW4ZR7h7PlgxGXEQZ/co6odzbaO7ea4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYL5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTy5OAo28YYUBDOQPIPhWoJXyqVYVsRu+HBOhCP/zxjNUhHL727Ax3eQ7EQHB2QwtB88Dv27PrN7oKakSSeG1zLXUzTrddfNWwir25Y/TfRw7u/6AR7xxfdDKyUk3FgPFkkmQppL/PzOOzekNvG2b4PBhVeKrkWIotwZxoj22y8oql4LHiIUVylXe+iV4xoY4PdO5R1RgYd6kEZtQsS6aN5dxQsMkWW1npjs1yqAetZ6meigKyY0rxwLFa/yGbYeI+AjvW/uPLjp+mXlre6q/ig6s/US8zuDwTMq53VZQoiZYk9TAq2oB2hzN5sWBV/Bz5F2u2SyV2ADW8uxEIV47la7cK5M5x74/jJsTsUDaEi72lkT6kbaadksk9+S28ejnbbLmppiTN49wlA7yKLghmsu6AeggMwgOWXaU+fik2bH94UH0RK9Gg/42n6XDrZzXJNkXqrS5DgNLyooj7gywDzai0NQWh3kHK1dFdQqcgITzIV7COv75Ae2kg1S0kTdr2+zGMaP7ApXWNXXDn7Lhcqx8605Y0gY80ddf55dMBrEbPP3zQlPxtMDfDhIhLwO0xP/nBMxh2YMaRGKAGbSUMLjSsF+N/uIgOfOAZI4TuDbnKvgq/eTijXEjmQxVQa789pwOIFu8A/4ud06eeD/nhsoLOWYMpAs3CuLw3hnKcyNXZnH6Zb825zZzXIC7CYbEAJqwir2G9Dq9H4dXYWJPTF2XRzOgVR6CUusMYSSlAsJ7mydMAbqmTYY91Rio8g/30bN8BvfS+zcZspDqktVusb79jxY3oBZ9FIymy2CRU2xuhStcTXk/mr85ulR81kuOy7NQjPlRFNgV7PRMBFRpfaXAxvB3XoihEjnKec2EHRP/Go3/UGMBC+kpytpLWH5TXtCrjxTNxS2vWuZHmLmCBZhy+aXZjSGoe5RNjk3e3axktGEIB9NVPDT/1KF6/gnXQYXOlhfBzvv4ReEnxCfIsVy74y+OsUVfClMiVKzEWTUOeRKTo4mjoEzFSLCqBPIsNQ4TkcM=

Have a look at the work on image recognition in medicine by the group
of Julio Rubio.

https://dblp.uni-trier.de/pers/hd/r/Rubio:Julio

They've formalized (parts of) this in Isabelle, Coq, ACL2

On Fri, Aug 3, 2018 at 2:23 PM, Tej Chajed
<tchajed AT mit.edu>
wrote:
> Zach Tatlock's group at UW has published a couple papers on formal methods
> in medicine, both related to radiation therapy:
>
> "Investigating Safety of a Radiotherapy Machine Using System Models with
> Pluggable Checkers"
> https://homes.cs.washington.edu/~ztatlock/pubs/neutrons-pernsteiner-cav16.pdf
>
> "Automatic Formal Verification for EPICS"
> https://homes.cs.washington.edu/~ztatlock/pubs/neutrons-jacky-icalepcs17.pdf
>
> The former uses SMT-based methods while the latter includes a validator
> written in Coq (among other uses of formal methods).
>
> On Fri, Aug 3, 2018 at 7:50 AM José Manuel Rodriguez Caballero
> <josephcmac AT gmail.com>
> wrote:
>>
>> Hello, I would appreciate any published reference about the applications
>> of proof assistants to medicine (I'm mainly interested in oncology).
>>
>> Kind Regards,
>> Jose M.

[Coq-Club] Applications to medicine, José Manuel Rodriguez Caballero, 08/03/2018
- RE: [Coq-Club] Applications to medicine, Soegtrop, Michael, 08/03/2018
- Re: [Coq-Club] Applications to medicine, Tej Chajed, 08/03/2018
  - Re: [Coq-Club] Applications to medicine, Bas Spitters, 08/03/2018