ALF (proof assistant)
From HandWiki
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, 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
 |  |
