 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 Alfa, Agda, Cayenne and Coq proof assistants and dependently typed programming languages.