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

[Frédéric Blanqui]

Hello.

You can also use Dedukti (https://deducteam.github.io/) or its new 
implementation Lambdapi (https://github.com/rlepigre/lambdapi) through 
some shallow encoding. Dedukti and Lambdapi are implementations of the 
lambda-Pi-calculus modulo rewriting. So it includes simple and dependent 
types, and objects and types can be defined by rewrite rules. 
Polymorphism can be encoded using type-level rewriting. For theoretical 
details, see:

- Embedding pure type systems in the lambda-Pi-calculus modulo, D. 
Cousineau and G. Dowek, TLCA'07, http://doi.org/10.1007/978-3-540-73228-0_9.

- A framework for defining computational higher-order logics, A. Assaf, 
PhD thesis, 2015, https://tel.archives-ouvertes.fr/tel-01235303/.

- Dedukti: a Logical Framework based on the $\lambda\Pi$-Calculus Modulo 
Theory, A. Assaf and G. Burel and R. Cauderlier and D. Delahaye and G. 
Dowek and C. Dubois and F. Gilbert and P. Halmagrand and O. Hermant and 
R. Saillard, http://lsv.fr/~dowek/Publi/expressing.pdf.

Best regards,

Frédéric.


Le 30/09/2018 à 19:23, Askar Safin a écrit :
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom