HOT

HOT is an automated termination prover for higher-order rewriting, based on the notion of computability closure (see papers below).

It accepts as input termination problems in the termination competition format XTC and also a simpler home-made text format.

On 29 June 2012, HOT won the international termination competition in the category "higher-order rewriting".

On 14 June 2012, on the competition platform, it can prove in 171s the (non) termination of 130/156=83% of the higher-order termination problems of the termination competition database TPDB 8.0.1.

Scientific background:

• Decidability of type-checking in the Calculus of Algebraic Constructions with Size Annotations, CSL'05, LNCS 3634, 17 pages.
• A type-based termination criterion for dependently-typed higher-order rewrite systems, RTA'04, LNCS 3091, 15 pages.
• Definitions by rewriting in the Calculus of Constructions, MSCS 15(1), 57 pages, 2005.
• Termination and confluence of higher-order rewrite systems, RTA'00, LNCS 1833, 15 pages.

Contact: Frédéric Blanqui.