ALF (proof assistant)

{{Short description|Structure editor for monomorphic Martin-Löf type theory}}

{{for|the programming language|Algebraic Logic Functional programming language}}

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.Thierry Coquand (1992). [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.37.9541&rep=rep1&type=pdf#page=69 "Pattern Matching with Dependent Types"]. In Bengt Nordström, Kent Petersson, and Gordon Plotkin (editors), Electronic Proceedings of the Third Annual BRA Workshop on Logical Frameworks (Båstad, Sweden).Thorsten Altenkirch, Conor McBride and James McKinna (2005). [http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf "Why Dependent Types Matter"].