<!DOCTYPE html><html><head> <style type="text/css">body { font-family:'DejaVu Sans Mono'; font-size:12px}</style> </head> <body><div>Hi people out there, I'm new here.</div><div><br></div><div>May be my mind is buggy, I was sure to recall there was an OpenTheory reader/writer for Coq. Now looking at http://www.gilith.com/research/opentheory/ , I can't see it.</div><div><br></div><div>I know there is a reader for Isabell/HOL. Unfortunately, I'm rather looking for a proof environment with a writer, as I bother about saving proofs.</div><div><br></div><div>If this is useful, I may draw the picture. I'm learning to effectively use ATS, a language with dependent types, linear types, inductive definitions and proofs. It's a very nice language, however and for good reasons, not suited to prove properties of as an example, inductive definitions (it mainly target programming issues, that is, ensuring pre/post conditions, resources tracking and the likes). I'm planning to export inductive definition using the abstract syntax tree output ATS provides, then prove properties of these inductive definitions, outside of ATS and save these proofs in a standard format (luckily, OpenTheory exists). I had some short past experience with Isabelle/HOL and Coq. I like Isabelle/HOL for being HOL, but don't really like the language and even less like the editor. So I tough about Coq and CoqIDE, which seems more usable to me, as much the language and the IDE, although I don't really know its logic, seemingly a superset of HOL. Unfortunately, it does not seems to support OpenTheory. So may be HOL Light, but I never used it, and am afraid of writing proofs in a TTy like interface.</div><div><br></div><div>That's about the picture. If possible, I would prefer to use Coq, just only if it can writes OpenTheory files.</div><div><br></div><div>I welcome any comments and suggestions.</div><div><br></div><div>Have a nice day as much as possible, and happy new year 2016.</div><div><br></div><div><br></div><div id="M2Signature"><div>-- </div><div>Yannick Duchêne</div></div></body></html>