View source for ALF (proof assistant)

{{Short description|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 (programming language)|Agda]], [[Cayenne (programming language)|Cayenne]] and [[Software:Coq|Coq]] [[Proof assistant|proof assistant]]s and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.<ref>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 [[Biography:Gordon Plotkin|Gordon Plotkin]] (editors), ''Electronic Proceedings of the Third Annual BRA Workshop on Logical Frameworks (Båstad, Sweden)''.</ref><ref>[[Biography:Thorsten Altenkirch|Thorsten Altenkirch]], [[Biography:Conor McBride|Conor McBride]] and James McKinna (2005). [http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf "Why Dependent Types Matter"].</ref>

== References ==
{{reflist}}

== Further reading ==
* Lena Magnusson and Bengt Nordström. [http://www.cs.chalmers.se/~bengt/papers/alfengine.pdf "The ALF proof editor and its proof engine"].
* [[Biography:Thorsten Altenkirch|Thorsten Altenkirch]], Veronica Gaspes, Bengt Nordström and Björn von Sydow. [http://www.cs.chalmers.se/~bengt/papers/usersguidetoalf.pdf "A user's guide to ALF"].

== External links ==
* [http://www.cse.chalmers.se/~hallgren/Alfa/ Alfa]


[[Category:Academic programming languages]]
[[Category:Dependently typed languages]]

{{Sourceattribution|ALF (proof assistant)}}