ALF (proof assistant)
Structure editor for monomorphic Martin-Löf type theory
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 Rocq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.
Sources and credits
This article is adapted from the Wikipedia article “ALF (proof assistant)”, written by its contributors and licensed under CC BY-SA 4.0. Fathomly has changed the layout, removed citation markers, navigation and maintenance notices, and adjusted punctuation. This adapted version is shared under the same license. For references, see the original article.
Fathomly is not affiliated with or endorsed by the Wikimedia Foundation. Spotted a problem? Tell us.