The specification:
Format specification
With examples. See also the BNF.
CICM Article
TIP: Tons of Inductive problems, presented at CICM 2015.
LPAR Article
TIP: Tools for Inductive Provers, presented at LPAR 2015.
The current version of the benchmarks:
tip-benchmarks-0.4.tar.gz
The benchmarks in TIP format. This is an extension of SMT-LIB with polymorphism and higher order functions.
tip-benchmarks-0.4-smtlib.tar.gz
The problems converted to SMT-LIB format. In this version, polymorphism is removed heuristically by monomorphisation, and higher-order functions are eliminated using defunctionalisation.
tip-benchmarks-0.4-why3.tar.gz
The problems converted to Why3ML. A few benchmarks do not pass Why3's termination checker.
The repositories:
tip-org/benchmarks
The repo containing all the benchmarks
tip-org/tools
Tools for translating from TIP itself or Haskell into other formats like WhyML.