From Tom

Jump to: navigation, search

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.



In a model checking context, Tom has been used to compute reachable terms (with respect to a given rewrite system). In particular, the classical 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.

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.


Lemuridae is a proof assistant allowing the building of proofs in the extendible sequent calculus, a.k.a. superdeduction for the sequent calculus. It is written in Tom and features super-rules derivation with focussing as well as some basic automatic tactics. The correctness is ensured by a tiny kernel checking the generated proof trees.

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 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.


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.


Éterlou is a prototype tool to parallelize programs written in a small while-language. Éterlou requires programs to be proven with separation logic and uses separation logic's "*" to detect potential parallelism.
In éterlou's implementation, Tom is used to define a rewrite system on proof trees that represent derivations of Hoare triplets. This implementation is peculiar in the sense that it does not use gom to define data structures. Instead, mappings are used to pattern match against already existing Java classes.


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.

Personal tools
Create a book