ALF (proof assistant)
For the programming language, see 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.[1][2]
References
- ↑ Thierry Coquand (1992). "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). "Why Dependent Types Matter".
Further reading
- Lena Magnusson and Bengt Nordström. "The ALF proof editor and its proof engine".
- Thorsten Altenkirch, Veronica Gaspes, Bengt Nordström and Björn von Sydow. "A user's guide to ALF".
External links
This article is issued from Wikipedia - version of the Monday, February 15, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.