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