Implementation Notes - shaolintl/fstar-type-checker GitHub Wiki
Organization
The Matita submodule contains the most up to date PTS implementations, and the ELPI submodule contains of course the ELPI sources and some other example/test programs.
ELPI Files
Once accumulated, the provide a kernel for type checking, onto which one can add type rules modularly.