Dear HOL users, in the old LISP days, exchange of symbolic data was really trivial, using built-in read/write functions for s-expressions. Later things became more complex in ML, and especially with XML.
The following tiny library in SML or OCaml makes things again mostly trivial: https://bitbucket.org/makarius/yxml/src/ YXML is pronounced "Why XML". It is both the question and answer to the problem of concrete transfer syntax of seemingly trivial tree expressions. The other part is a rather obvious combinator library to represent typed ML expressions over untyped XML, in the same spirit as the ML runtime would do that for untyped bits in memory. Isabelle/ML has included both as standard library functions for quite some time already. Maybe the independent versions above help to bridge over to other provers from the HOL family. Makarius ------------------------------------------------------------------------------ This SF email is sponsosred by: Try Windows Azure free for 90 days Click Here http://p.sf.net/sfu/sfd2d-msazure _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
