Article · Wikipedia archive · Last revised Jul 3, 2026

ALF (proof assistant)

ALF 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 Rocq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.

Last revised
Jul 3, 2026
Read time
≈ 1 min
Length
126 w
Citations
2
Source
Wikipedia ↗

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 Rocq proof assistants and dependently typed programming languages. It was the first language to support inductive families and dependent pattern matching.12

References

References

  1. 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).
  2. Thorsten Altenkirch, Conor McBride and James McKinna (2005). "Why Dependent Types Matter".
Further reading

Further reading

External links