Существует ли поддержка для интерпретации и проверки доказательств Coq в другой среде (например, Java, C ++), отличной от Coq? Очевидный подход состоит в том, чтобы создать с нуля весь интерпретатор, скажем, на Java, но мне интересно, что нужно сделать как можно меньше.