coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Any proof assistant for Observational Type Theory?

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Any proof assistant for Observational Type Theory?
Date: Tue, 21 Mar 2017 17:38:23 +0100
Authentication-results: mail3-smtp-sop.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-qk0-f181.google.com
Ironport-phdr: 9a23:ZsP3WByM6dsZS4zXCy+O+j09IxM/srCxBDY+r6Qd2+seIJqq85mqBkHD//Il1AaPBtSGrawVwLqH+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZPebgFIiTanYL5/KBq6oAbVu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8rxmQwH0higZKzE58XnXis1ug6JdvBKhvAF0z4rNbI2IKPZyYqbRcNUHTmRDQ8lRTTRMDYGyb4UPAeQPPvtWoZfhqFUBtha+GRCsCfnzxjNUmnP736s32PkhHwHc2wwgGsoDvWnOo9XuKawcTPi1zKjUzTXfcfxWwyz945XPfx86u/2DR6h8cMTLxUk0DwPFj0mQqZD7MDOPzeQAqGeb7+96WuKuj24rsR1+oj+qxso1jITCm4wbylfB9SpjwYY1I8W1SEF6Yd64EJtQqjqVO5FqTcMlRmFlvjsxxL4euZOjYiQG1JAqywTcZvGHaYSE/AzvWPqLLTtlh39pZbSyjAuo/0e60O3zTMy03U5KriVbltnMsWgA1xnJ5ciGTvtx516h2TWT2wzK5OFIPEM5mbfBJ54uxb4wkZUTsUDdESPshEr2i6qWel0l+uiu9evnfq3rqoGAO4JwkA3zMaQjltahDegmLgQCRXWX9Oeh2LH7+E32WrRKjvk4kqnDt5DaINwWqbWjDwBPyIoi5QyzDyy+0NQZgXkHMExKeAicj4XyNFHOJer3Dfa7g1i2jDhrwPXGMqX7AprRNnjDjKvhfbFl5kFAzwoz1MlT6I5QCrEcO/3+QVTxtdzdDh8hKQO42efnCNNn1oMfQ22DGKGZMLmB+WOPs8koOqGnYJIf8GL2LOFg7Przh1c4n0UcdO+nx81ERmq/G6FMKl7RWmLtnssMC3xC6gB4Rar1zkaaUCJPamypd6057zA/TomhCNGQFciWnLWd0XLjTdVtbWdcBwXJSC+weg==

Cubical is another implementation of a type theory with functional
extensionality (and more).
https://github.com/mortberg/cubicaltt

On Tue, Mar 21, 2017 at 5:08 PM, Ilmārs Cīrulis
<ilmars.cirulis AT gmail.com>
wrote:
> 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