822 B
822 B
| title | chunk | source | category | tags | date_saved | instance |
|---|---|---|---|---|---|---|
| ALF (proof assistant) | 1/1 | https://en.wikipedia.org/wiki/ALF_(proof_assistant) | reference | science, encyclopedia | 2026-05-05T11:30:45.794613+00:00 | kb-cron |
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.
== References ==
== 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