coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Any proof assistant for Observational Type Theory?
Date: Tue, 21 Mar 2017 18:08:48 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ilmars.cirulis AT gmail.com; spf=Pass smtp.mailfrom=ilmars.cirulis AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f46.google.com
Ironport-phdr: 9a23:RRq+ThRzBSJ3io+BZibNlJvUhNpsv+yvbD5Q0YIujvd0So/mwa67bR2N2/xhgRfzUJnB7Loc0qyN4v2mBz1LsczJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rtfYZBwNjz6ga5tzKg+3pEPfrINe1YBlM+M6zgbDinpOYeVfg21ycwG9hRH5s+a0+TV56Gx7uug8889bGfH7e6ExV6ceBzU8LmQ0/+XksBDCSU2E4X5KATZeqQZBHwWQtEKyZZz2qCav7uc=

Hello!

The only one I found is https://github.com/effectfully/OTT that is a library in Agda. (Haven't tried it yet.)

Does any other exist?

Thanks you,

Ilmars

[Coq-Club] Any proof assistant for Observational Type Theory?, Ilmārs Cīrulis, 03/21/2017
- Re: [Coq-Club] Any proof assistant for Observational Type Theory?, Bas Spitters, 03/21/2017
  - Re: [Coq-Club] Any proof assistant for Observational Type Theory?, Roman, 03/24/2017
    - Re: [Coq-Club] Any proof assistant for Observational Type Theory?, Ilmārs Cīrulis, 03/24/2017