coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Applications to medicine

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
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 08:23:11 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-6.mit.edu
Ironport-phdr: 9a23:4piCERXx0ObUTjDZJZUi4gxlCB3V8LGtZVwlr6E/grcLSJyIuqrYYxCOt8tkgFKBZ4jH8fUM07OQ7/i+HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9zIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W7YhMx/jqJVrhyiqRJi3YDbfJqYO+Bicq7HZ94WWXZNU8RXWidcAo28dYwPD+8ZMOhGsYb9pUYFoAW+BQa2BuPg1CJHjWLx0K0mz+shERvJ3A4+EN0Tq3nUqdT1NLsIXe+r0abI0CzOYvVL0jnz74jIdwouofCKXb9of8ve01IvFwPEjlWWpozlIzSV1uIXv2eF8uVgSOSigHMkpQFpujWj28QhhpPLi44Py13J9j91zYg1KNGgVkJ3fdqpHIFTuiyaLYd6XN0uT31ytConyLALt5i2dzUQxps93R7QcfmHfpCI4h39UOaRJi91i29geLO+nhqy9FKvyuz4VsmvzllFsjNJksLQuX8X0RzT7NaISuFk8kqgwzqP0gHT6v1eLU8qiKXbNoYtwr82lpUNrUTOBjL6lUbsgKKUbEkp++ul5/7pb7jmvpOcMpV7igD6MqQggMy/BuE4PxASX2eH+eSzzr/j8lPkT7hRi/02k7XZvIrEKssGu661GxVV3Zo76xajEzem18wVkmUALFJcYR6Ik4zpO0zVL/3jFve+g1GskC9xyPzcP73hBI/NLnnZn7v7c7Z98R0U9A1mxtdGoplQF7tJdPn0Qwr6sMHSJh4/KQ29hej9XoZTzIQbDF6CAOeyMKrQvFPAsv4kI+COaYM9vTfhbfUp+qi93jcChVYBcPzxjtMsY3eiE6E+ehTLUT/Xmt4EVFwykE87Re3uhkeFVG8BYneuGa8w+2NiUd70PcL4XomoxYe58mKjBJQHNGVHFhaBHWq6L9zZCcdJUzqbJ4paqhJBVbWlTNR4hx2rpkr/wrtjNeffvzYTvJTl2cIwuavWlA10+DBpXZyQ

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