The two most important directories are:
toy contains a toy proof-of-concept implementation of a language with refinement types that compiles to Idris.