coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Verification of GUIs in Coq

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Verification of GUIs in Coq
Date: Tue, 10 Oct 2017 08:36:03 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f45.google.com
Ironport-phdr: 9a23:F6j2rRCjfhIqJHR8AY0pUyQJP3N1i/DPJgcQr6AfoPdwSP3+ocbcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHERLmcAFxO+7dG4jIjs3x2frh1YfUZlBtjSahYbJ/MV2Nqhfcv9Re1Y5rNro4zzPMq2dUcuEQwnlncwHA1y3g79u9qcYwux9bvOgsopZN

Hi stvienna,

the closest thing I know is this paper by Neelakantan R. Krishnaswami and Nick Benton

https://dl.acm.org/citation.cfm?id=2034782 but it's about a new type theory, not really Coq

related.

Best,

-- Matthieu

On Tue, Oct 10, 2017 at 2:30 AM 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

[Coq-Club] Verification of GUIs in Coq, stvienna wiener, 10/10/2017
- Re: [Coq-Club] Verification of GUIs in Coq, Matthieu Sozeau, 10/10/2017
- Re: [Coq-Club] Verification of GUIs in Coq, Abhishek Anand, 10/10/2017
  - Re: [Coq-Club] Verification of GUIs in Coq, Jim Fehrle, 10/10/2017
  - Re: [Coq-Club] Verification of GUIs in Coq, Daniel Schepler, 10/10/2017
    - Re: [Coq-Club] Verification of GUIs in Coq, Valentin Robert, 10/10/2017
      - Re: [Coq-Club] Verification of GUIs in Coq, Pierre Courtieu, 10/11/2017
    - Re: [Coq-Club] Verification of GUIs in Coq, David MENTRÉ, 10/30/2017