The Coq mailing list

[Erik Palmgren <palmgren AT math.su.se>]

There are some models of constructive set theory CZF formalized in Coq
and related systems. Adding an axiom for classical logic to Coq allows
to model ZF  (since ZF=CZF+PEM)  - "some assembly required"

[6] Jason J. Hickey. The MetaPRL Logical Programming Environment. PhD thesis, 
Cornell University, Ithaca, NY, January 2001.

[12] Nax P. Mendler. Note: An Implementation of Constructive Set Theory in 
the LEGO System. Department of Computer Science, Manchester University 1991.

A more recent formalization of the model is in

https://arxiv.org/pdf/1408.1364.pdf
http://staff.math.su.se/palmgren/coq/czf_and_setoids/



________________________________________
Från: 
coq-club-request AT inria.fr
 
<coq-club-request AT inria.fr>
 för Bas Spitters 
<b.a.w.spitters AT gmail.com>
Skickat: den 8 oktober 2017 16:57
Till: Coq Club
Ämne: Re: [Coq-Club] Importing (translating) Mizar into Coq

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