coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Alex Meyer <alex153 AT outlook.lv>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Importing (translating) Mizar into Coq
Date: Sun, 8 Oct 2017 14:42:51 +0000
Accept-language: lv-LV, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex153 AT outlook.lv; spf=Pass smtp.mailfrom=alex153 AT outlook.lv; spf=Pass smtp.helo=postmaster AT EUR03-VE1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:3EU4ZBFHYkXhjvXYEw8y9J1GYnF86YWxBRYc798ds5kLTJ76oMiwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVT1/0MhMwLeDoEKbTid623qa84debNw5PnX+2Za54BBSwtwTY8McM19hMMKE0nzLNr2sAXulHyHkgcVuXkgalu5yY+4N/9yNXuLQl6ZgTAu3BY60kQOkAX3wdOGcv6ZizuA==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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