ASF+SDF formalism and the ASF+SDF Meta-Environment are projects of the GLT group, these projects started in 1985 and they have two complementary goals. The first one was the development of a formalism to describe the syntax and semantics of a (programming) language. This has resulted in the ASF+SDF formalism. SDF (Syntax Definition Formalism) allows the definition of the syntactical aspects of a language. It uses the latest parsing technologies in order to write down syntax definitions and it provides a parser generator and a scannerless generalized LR parser. ASF (Algebraic Specification Formalism), allows the equational definition of semantics in user-defined syntax. An efficient compiler has been developed to execute ASF specifications. The application area of ASF+SDF is targeted to language prototyping, domain specific languages, and software renovation. The second goal was the development of an integrated interactive environment to develop and test ASF+SDF specifications, this environment offers syntax-directed editing facilities, an interpreter, compiler, parser generator, parser, pretty printer, and debugger.
The Protheo project in Nancy develops concepts, methods, and tools using rewriting as the main computation and deduction paradigms. In this context, we developed ELAN as a language and environment allowing to express and execute strategy guided rewrite systems. The semantical foundation of the systems rely on the rewriting calculus and the compilation techniques developed for the language allows us to deal efficiently with associative-commutative symbols as well as with non-determinism. The application area of ELAN concerns more specifically safe program development and encompass constraint solving, theorem proving, and model checking.
The two teams share a strong core of common knowledge
and knowhow in the field of rewriting and their collaboration
benefits from complementary point of views on concepts,
implementation, applications, and potential transfers.
This common culture and common view on the general goals, together with the opportunity to share knowledge and developments lead us to initiate a collaboration starting with the organization of two workshops followed by several visits.
The ideas were ripping the last two years and the last workshop in Volkrange enlightens the strong common interest of the two groups to collaborate on the design and implementation of reusable modules for rewriting, controlling and analyzing. Since such development is quite involving both at the conceptual level and technical development level, there is a strong common commitment in pursuing and further developing the current cooperation. To this end we decided to increase our partnership in at least two ways:
OMDoc is an emerging standard format for mathematical texts based on XML, in particular on the XML based standards MathML and OpenMath. Among its aims is not only the rendering of the mathematical texts, but also a representation with well-defined semantics to facilitate interchange with computer algebra and proof systems. However, OMDoc is not suitable as an input format for humans.
LaTeX is the format that most mathematicians use for writing their articles and books, so it is natural to use it as an input format. However, it is very much oriented towards typesetting and its semantics is presentation rather than contents oriented. In the DLMF project this is mitigated by a standard set of macros, and it is conceivable to add semantical markup where needed, for example to specify types.
The powerful parsing technology of SDF combined with rewriting in ELAN promises to be suitable platform for this project. In particular we plan to use island grammars to isolate the mathematical content, to investigate how to best divide the work between parsing and rewriting, and to compare the expressiveness of ELAN with XSLT.
Similarly, the Generic Language Technology group has adopted several tools and ideas developped at Loria to support their research. For example, the TOM compiler has been used as a back-end for JJForester. Another interesting point is the influence of the Protheo group on the ASF+SDF developpment. Since January, the notion of builtins and libraries have been introduced in the ASF+SDF Meta-Environment.
The different signs clearly show the beginning of a true deep cooperation and the unification of different concepts. Furthermore, the first academic results are promising:
Nguyen Quang Huy
Mark van den Brand
Arie van Deursen
Hayco de Jong
Merijn de Jonge