The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Dear Steve,

The state of the declarative/mathematical/mizar-like proof mode of Coq is pretty much that of the 2008 article by Pierre Corbineau. There is no ongoing work to improve it at the moment (I've got a few plans, haven't had time to look into it). The version which shipped in Coq v8.4 didn't work quite right as was pointed to me recently, so I'm working to get a fully functioning version for the upcoming Coq v8.5. It never had many users, though, so it probably has a few warts (but, overall, it works fine).

The best person to write to is probably Pierre Corbineau is you have specific questions which do not fit in this list.

Best,

Arnaud Spiwack

On 4 April 2015 at 16:18, stvienna wiener <stvienna AT gmail.com> wrote:

Hello,

I have been reading papers about a declarative proof language for Coq[1], which is similar to Mizar. It is also referred to as a “mizar mode” for Coq[2].

Is there ongoing work on this declarative language / mizar mode for Coq? Where can I find the latest information, papers and possibly also a contact person?

Thanks,

Steve (from Vienna)


[1] Corbineau, Pierre. "A declarative language for the coq proof assistant." Types for Proofs and Programs. Springer Berlin Heidelberg, 2008. 69-84.

[2] Giero, Mariusz, et al. "MMode, a mizar mode for the proof assistant coq." (2003).