Email Gateway (Aug 18 2022 at 19:16): Email Gateway (Aug 18 2022 at 19:16):From: Makarius <makarius@sketis.net>
Several people have asked about it, so here it is: an OCaml version of the
ML value representation in XML, and the YXML transfer syntax. See
https://bitbucket.org/makarius/yxml (changeset 146b7018ad02 right now).
The README also contains an example with some Isabelle/HOL term in yxml
format that can be loaded into OCaml.
The general principle might turn out useful to transfer types, terms,
proofs etc. between Isabelle and Coq, HOL-Light, HOL0 etc. Maybe the
HOL-Light-Import renovation project can use it already.
Basically, this stuff should scale to some extent, but I have no
experience with constraints imposed by the OCaml runtime system (which
generally feels a bit old-fashioned).
Makarius
Last updated: Apr 24 2024 at 16:18 UTC