First login?
Lost password?
 
 
 
mailing-list for TeXmacs Users

Text archives Help


Re: [TeXmacs] Interfacing texmacs with Isabelle


Chronological Thread 
  • From: Joris van der Hoeven <address@hidden>
  • To: Paulo Jorge de Oliveira Cantante de Matos <address@hidden>
  • Cc: TeXmacs-users ML <address@hidden>
  • Subject: Re: [TeXmacs] Interfacing texmacs with Isabelle
  • Date: Thu, 23 Oct 2003 17:07:44 +0200 (CEST)

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


Archive powered by MHonArc 2.6.19.

Top of page