Applications

Since Tom is an extension of C or Java, it is naturally a general purpose language that can be used to implement a large class of applications.

The main contribution of Tom is to add pattern matching facilities to C and Java. The application domain of Tom becomes naturally related to the manipulation of structured tree/term based objects.

By introducing high-level, typed and structured constructs, Tom brings C or Java closer to algebraic and functional style programming languages.

Rewriting

In a model checking context, Tom has been used to compute reachable terms (with respect to a given rewrite system). In particular, the Needham Schroeder public-key protocol has been encoded and verified one more time. The originality of the Tom approach is to use, on one hand, rewrite rules to describe the possible transitions of the system. On the other hand, several strategies (deep-first, breadth-first, parallel, etc.) can described and executed efficiently.

In a proving context, Tom has been used to describe a family of (decidable) propositional provers. In a current project, Tom is used to certify that the code generated by the Tom compiler is correct

Tom has been used to implement a first implementation of the Rho-calculus.

Tom is currently used to study how production rule systems can be encoded by rewriting systems. The preliminary results are encouraging.

XML

Tom has been used in several industrial and academic projects to handle and manipulate complex data-structures represented by XML documents. Recently, Tom has been used in the development of a prototype for mHTML, which performs transformation on XML trees to produce (X)HTML code. For more detail on mHTML see the paper and download the prototype.

We are currently studying how Tom could help to compile efficiently XQuery programs.

Compilation

Tom has been used in various projects related to program/AST transformation. The most famous application is the Tom compiler itself.

Tom is a compiler implemented in a pure functional style: it takes an Abstract Syntax Tree (AST) which represents the parsed program, and returns another AST which corresponds to the generated program, just before the pretty-printing phase. This complex transformation is of course composed of several layered transformation phases, from type-inference to optimization of intermediate abstract code.

In this project, we have discovered that Tom is not only a technical extension of C or Java, but also an invitation to think at a more abstract level: in terms of abstract data-type and pattern matching.

Simulation

In collaboration with the MGS group, Tom has been used to describe dynamical systems. In this context, we have implemented an applet that illustrates how the gravity rule of the BoulderDash game can be implemented.

We also have studied how L-Systems can be encoded in Tom.

Downloads

Most of these applications are available on the Tom Downloads page.