lpi is a small dependently-typed language supporting dependent lists and dependent function spaces, and intends to grow into a fully featured, statically-checked programming language.