[FOM] Are there some more pure type system checkers available?
safinaskar at mail.ru
Sun Sep 30 13:23:29 EDT 2018
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.
More information about the FOM