1 points by lematheux
They are agda2, idris, lean and rocq. The benchmarks are written in a DSL that's transpiled to the target languages.