The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi James,

James Smith 
<jecs AT imperial.ac.uk>
 writes:

> I have a collaborative proof assistant (I use these last two words
> very reservedly) here:
>
> http://florence-cpa.org

It looks fantastic, thanks for the link!

> I've been reaching out to a few academics lately to see if I can find
> a way to possibly use Florence as a front end for an existing proof
> assistant and one of them suggested I subscribe to this
> list. Literally the second email I've received is about JsCoq. I'm
> glad to learn that there is at least one JavaScript implementation of
> an established proof assistant out there.

> There is much I could write, however it's probably best instead that
> anyone who is interested in the possibility of another front end for
> JsCoq should just get in touch.

I am definitively very interested officially supporting your front-end
in jsCoq if that's OK for you!

I'll be a bit busy until July 2nd (in fact I'll be at User Interfaces
for Theorem Proving, UITP 2016), but I suggest we either chat a bit in
private or you if prefer to discuss in public please open an issue in
the jsCoq github web tracker [1].

Best regards,
Emilio

[1] https://github.com/ejgallego/jscoq