Another Logical Framework (ALF)

ALF is an interactive theorem prover (a proof editor) based on Martin-L\"{o}f's type theory with explicit substitution.

NOTE: The proof engine of ALF is written in SML, and the window interface is done by interviews.