/smalftt

🍰 (WIP) a small logical framework based on dependent type theory

Primary LanguageKotlinMIT LicenseMIT

smalf(on)tt: a small logical framework based on dependent type theory

WIP...

This project is meant to be an implementation of a logical framework like Twelf, while also allowing me to practice dependent type theory.

The surface syntax aims to be compatible with the prospective SMT-LIB v3 standard. The file extension of smalf source code is .sl, corresponding to the conventional file extension for SMT-LIB.