ALF (proof assistant) explained

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]}

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

• Alfa

Notes and References

1. [Thierry Coquand]
2. [Thorsten Altenkirch]