[FOM] Are there some more pure type system checkers available?

[Askar Safin]

Hi. I am very interested in pure type systems (PTS), so I want to have some working PTS checker (for arbitrary PTSs with finite set of sorts).
Unfortunately, the only PTS checkers I was able to find are this two:

* Yarrow (  http://www.cs.kun.nl/~janz/yarrow/  )
* Pierre Corbineau's checker ( http://www-verimag.imag.fr/~corbinea/ )

Also, some articles mention CONSTRUCTOR checker by Leen Helmink, but unfortunately I was not able to find it (and Helmink didn't answer to me).

First one (Yarrow) doesn't compile with recent ghc (if anybody interested: I have a patch).

Moreover, both Yarrow and Corbineau's checker don't support non-sort constants, we need them to define PTS called \lambda^\tau, mentioned in Barendregt, "Lambda calculi with types".

Both checkers don't support non-functional (a. k. a. non-singly-sorted) PTSs.

I am not satisfied with functionality of published checkers. So, I have a question: are there some more checkers?

If there is no more checkers, I will probably have to write my own.

==
Askar Safin
http://vk.com/safinaskar