A special seminar on TeXmacs and Isabelle/Scala/jEdit will take place on Wednesday, March 30, 2011 at the conference room of LIX Laboratory of Ecole Polytechnique.

• Title: GNU TeXmacs, a scientific text editor by Joris van der Hoeven

  Time: 14h00

  We will present the GNU TeXmacs scientific editor (see www.texmacs.org). In a similar way as LaTeX, this software allows for the preparation of structured documents with mathematical formulas. However, the editor comes with a user friendly wysiwyg (what you see is what you want) interface. TeXmacs has many other features: it includes a presentation mode, a small technical image drawer, and the ability to incorporate and execute sessions of computer algebra inside the documents. The software is also extensible in different ways: style sheets, Scheme extension language, plug-ins, etc.

• Title: Isabelle/Scala/jEdit as Prover IDE by Makarius Wenzel

  Time: 15h30

  Interactive theorem provers in the LCF tradition (such as HOL, Coq, and Isabelle) have traditionally posed significant challenges for integration with sophisticated front-end technology. The most successful prover interface of all time is still Proof General / Emacs, although it merely provides a thin layer for the command-line, and thus fits to many provers as lowest common denominator. So provers and prover interfaces appear to be stuck in mutual restriction of their full potential.

  Many aspects of prover interaction and integration have been reworked for Isabelle in the past few years, after observing inherent technical problems with Emacs (and Emacs Lisp) on the one hand, and advances in parallel prover technology on the other hand. Our approach is based on Isabelle/Scala as system integration layer that provides a relatively simple document-oriented API of the prover on the Scala/JVM platform. Behind the scenes there is a private protocol for high-performance interaction with the parallel Isabelle/ML process, which operates on a persistent repository of document versions in a stateless / timeless fashion.

  In current Isabelle2011 (see isabelle.in.tum.de), there is already an experimental Prover IDE built on top of Isabelle/Scala, as plugin for the popular jEdit editor framework on the JVM. Thus we leverage sophisticated editor functionality for our purposes of continuous proof checking with IDE-style feedback on the source text (such as squiggly underline, tooltips, hyperlinks). The general look-and-feel is more like a powerful IDE for programming languages, than a scientific editor. This is partly a consequence of the general plan, and partly imposed by technical restrictions of available JVM frameworks.