ALF (proof assistant)

ALF ("Another logical framework") is a structure editor for monomorphic Martin-Löf type theory developed at Chalmers University. It is a predecessor of the , Agda and Cayenneproof assistants and dependently typed programming languages. It was the first language to support inductive families and .