On Mon, Sep 15, 2014 at 4:38 PM, Stefan Israelsson Tampe <
stefan.itampe@gmail.com> wrote:

> I have been wondering if one could speed proofs myself, and especially for
> type provers.
>

What do you mean by 'type provers'? Do you mean type inference? I did a
purely functional implementation of Hindley-Milner type inference:
http://prooftoys.org/ian-grant/hm/ and its performance is good. It can
infer the types of pathalogical examples such as Mairson's, in less than a
minute. This is a type expression which takes 50,000 lines of output on a
80-column terminal:

*let fun pair x y = fn z => z x y **    val x1 = fn y => pair y y **
 val x2 = fn y => x1 **(x1 y)**    val x3 = fn y => x2 **(x2 y)**
val x4 = fn y => x3 **(x3 y)**    val x5 = fn y => x4 **(x4 y)**in**
x5 **(fn z => z)**end*