Past events


July 21

First release of Rainbow, a tool for automatically certifying termination proofs !

June 22

Abonnez-vous à la lettre d'information prix-specif pour être informé des appels à candidature et résultats du prix de thèse SPECIF !

May 10

New release of CoLoR with Adam Koprowski's formalization of simply typed lambda-calculus and higher-order recursive path ordering (HORPO)

April 28

Release of TOM 2.3 ! The release announce.

February 3

Modulogic seminar. CoLoR, CiME 3, matching, rewriting and invariants, etc.


December 21

The release of Cariboo 1.1 is now available!

October 28

Clara Bertolissi's PhD thesis defense on "The graph rewriting calculus: properties and expressive capabilities".

October 13-14

3rd Nancy-Saarbrücken Workshop on Logic, Proofs and Programs

October 7

Benjamin Wack's PhD thesis defense on the logical aspects of the rewriting calculus.

September 15

Candidatez au Prix de thèse SPECIF 2005 !

July 29

Release of TOM 2.2 !

May 30-31

Second Workshop on the Rho-Calculus, LIX, Ecole Polytechnique, Palaiseau.

May 12

QSL Workshop on Functional Programming and Verification, Nancy.

March 14

Release of the first version of CoLoR, a Coq Library on Rewriting and termination. The aim of this library is to provide the necessary formal basis for certifying the termination witnesses searched and built by tools like CiME, AProVE, TTT, Cariboo, etc. It already includes a library on vectors, a library on integer polynomials with multiple variables, a library on algebraic terms with symbols of fixed arity, a proof of the termination criterion based on polynomial interpretations, and a proof of the dependancy pairs theorem.

February 21-24

Annual Rewerse meeting at Munich.

February 7-11

Modulogic seminar at Val d'Ajol. Development of types modulo in OCaml, certification of TOM matching with Zenon, etc.


December 12

Release of TOM 2.1 !

November 25-26

2nd Nancy-Saarbrücken Workshop on Logic, Proofs and Programs at Saarbrücken.

October 28-29

Modulogic seminar at Val d'Ajol. Development of types modulo in OCaml, certification of TOM matching with Zenon, etc.

October 15

Averroes meeting in Paris.

September 22-24

2nd Workshop on Coq and Rewriting, Ecole Polytechnique. Great success: 52 participants !

September 15

Liliana Ibanescu got an award from INPL for her thesis.

September 14-17

Modulogic seminar at Val d'Ajol.

June 24

Averroes meeting in Paris.

June 18-18

1st Nancy-Saarbrücken Workshop on Logic, Proofs and Programs at Nancy.

June 14

Liliana Ibanescu's PhD thesis defense on rule-based programming and strategies for automated generation of detailed kinetic models for gas phase combustion of polycyclic hydrocarbon molecules.

June 9

Release of TOM 2.0 !

May 14

Modulogic meeting in Nancy.

March 18

Modulogic meeting in Paris on termination proof techniques, ELAN, etc.

March 11-12

Workshop on rho-calculus in Nancy.


A convention between CONACYT, UHP, ULP and INPL has been firmed for having 15 mexican students doing a PhD in a french laboratory associated with UHP, ULP or INPL. The Protheo team proposes a subject on the integration of rewriting technology in proof and program environments.

February 2-6

The third AirCube workshop will be held in Val d'Ajol (Vosges, France). The idea is to have a one-day workshop for the two teams to meet and the other days will be used to work together in smaller groups on specific topics. A preliminary program is under construction.

January 29

Modulogic meeting in Nancy on TOM and FOC.

January 27

Participation to the 11e Rencontre INRIA-Industrie: L'ingénierie du logiciel. Presentations of "formal islands" and TOM.

January 22-23

Congrès SPECIF à Lille sur le thème "valorisation de la recherche".

January 12-February 14

Visit of Anamaria Martins Moreira.


December 3

Olivier Fissore's PhD thesis defense on termination of rewrite systems under strategies, and visit of Nachum Dershowitz, Jürgen Giesl and Bernhard Gramlich.