mailing-list for TeXmacs Users

[Joris van der Hoeven <address@hidden>]

On Thu, 23 Oct 2003, Paulo Jorge de Oliveira Cantante de Matos wrote:
> Has anyone ever tried to interface texmacs with the Isabelle logical
> framework? I'd like to know if it is even possible, which I'm not sure
> since Isabelle is not a CAS.

This is certainly going to be possible. Logical frameworks are
a bit more complex than computer algebra systems from the interfacing
point of view (especially since I am not a specialist), but we definitely
do *want* to support such systems. Philippe Audebaud has done some
pioneering work with Coq (cf. next mail), although he chose to limit
himself (for the moment) to the document generation side.

Personally, I recently started a collaboration with the Omega team in
Saarbrucken and they have several students which should be working
on the project. Our work plan is at follows:
  1) Write parsers and pretty printers for sufficiently customizable
     mathematical grammars.
  2) Use this to provide mathematical input with context dependent
     semantics.
  3) Write converters for OMDoc which incorporate 2, theorem-like markup
     and sectional markup.
  4) Start writing the real interface for Omega using plug-ins and Scheme.
Of course, any help and suggestions are welcome. In any case,
if the question is whether it is possible and whether we want to support
logical frameworks and whether, then the answer is definitely: yes.

Best wishes, Joris