Section: Software

Cat

Participant : Yves Guiraud [correspondant] .

Cat is a library for polygraphic calculus, written in Caml. It has been used, in a joint work with F. Blanqui, to produce an automatic termination prover for first-order functional programs. It translates such a rewriting system into a polygraph and tries to find a derivation proving its termination, using the results of [6] , [39] . If possible, it seeks a derivation that proves that the program is polynomial  [29] , [3] . Cat is also at the basis of Catex.