The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I am curious what you want to prove about GUIs. 

In the healthcare domain, I guess privacy is the biggest concern. 

I think that a pragmatic approach is to push these concerns to the backend, whose semantics seem much easier to define than the frontends (GUIs) that interact with humans who are too complex creatures to formally reason about.

For example, it may be possible to just argue that the backend, when communicating with the frontend, never reveals sensitive information. Thus, the frontend, in whatever ways it renders the graphics, cannot reveal sensitive information.

I guess the following work is an example:

http://goto.ucsd.edu/quark/

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Mon, Oct 9, 2017 at 8:30 PM, stvienna wiener <stvienna AT gmail.com> wrote:

Hello everyone,


We are verifying GUI applications from the healthcare domain (e.g.,
healthcare processes) in Agda. Is there any related work in Coq? My
searches mostly return papers on how to write GUI front-ends to
theorem provers/Coq but not how to verify GUIs.


Thanks & best regards,
Stephan