[isabelle] ML vs XML vs YXML

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.