coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Importing (translating) Mizar into Coq

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Importing (translating) Mizar into Coq
Date: Sun, 8 Oct 2017 16:57:41 +0200
Authentication-results: mail2-smtp-roc.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-qt0-f169.google.com
Ironport-phdr: 9a23:Ll0FlRb5vI8uD9LC1PAfX7b/LSx+4OfEezUN459isYplN5qZpsW5bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76xXcoFx7+LQt4IPjuUs6X1pzvlrP6x5qGSAJRzBG5fLk6eB6xtEDastQcqYpkMKc4jBXT9ChmYeNTkElhPhqohxfg+sqq59Y3+WJZ/e1n7NZBTbn3Zb8QQrlRDTBgOGcwsp64/SLfRBeCsyNPGl4dlQBFVk2ctEn3

Have a look at the work by Bruno. Section 2.5:
http://www.lix.polytechnique.fr/~barras/habilitation/

Yes, it is possible to do Tarski-Grothendieck in Coq. However, I don't
recall having seen a syntactic translation from mizar to Coq.

Google also gave me this one:
https://www.ps.uni-saarland.de/Publications/documents/Kaiser_2012_Formal.pdf

On Sun, Oct 8, 2017 at 4:42 PM, Alex Meyer
<alex153 AT outlook.lv>
wrote:
> Hi!
>
>
> I am reading https://jfr.unibo.it/article/view/4570 and there are mentioned
> translations of HOL into Coq and Mizar, but translation of Mizar to Coq is
> lacking. Are there efforts to translation Mizar into Coq? Coq should be
> expressive enough to formalize anything that Mizar does. Or there are
> unsourmountable obstacles and Mizar will be always required for doing some
> math?
>
>
> Alex

[Coq-Club] Importing (translating) Mizar into Coq, Alex Meyer, 10/08/2017
- Re: [Coq-Club] Importing (translating) Mizar into Coq, Bas Spitters, 10/08/2017
  - SV: [Coq-Club] Importing (translating) Mizar into Coq, Erik Palmgren, 10/08/2017