ALF (proof assistant)
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 , Agda, Cayenne and Coq proof assistants and dependently typed programming languages. It was the first language to support inductive families and .[1][2]
References[]
- ^ Thierry Coquand (1992). "Pattern Matching with Dependent Types". In , , and Gordon Plotkin (editors), Electronic Proceedings of the Third Annual BRA Workshop on Logical Frameworks (Båstad, Sweden).
- ^ Thorsten Altenkirch, Conor McBride and (2005). "Why Dependent Types Matter".
Further reading[]
- Lena Magnusson and . "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 computer science article is a stub. You can help Wikipedia by . |
Categories:
- Computer science stubs
- Academic programming languages
- Dependently typed languages
- Proof assistants