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. It was the first language to support inductive families and dependent pattern matching.

For the programming language, see Algebraic Logic Functional programming language.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.