The Coq mailing list

[stvienna wiener <stvienna AT gmail.com>]

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).