Alfa is a successor of the proof editor ALF, i.e., an editor for direct manipulation of proof objects in a logical framework based on Per Martin-Löf's Type Theory. It allows you to, interactively and incrementally, define theories (axioms and inference rules), formulate theorems and construct proofs of the theorems. All steps in the proof construction are immediately checked by the system and no erroneous proofs can be constructed.
Alternatively, you can view Alfa as a syntax-directed editor for a small purely functional programming language with a type system that provides dependent types. In fact, the language is very similar to the functional language Cayenne by Lennart Augustsson.
There are no reported vulnerabilities
30 Day SummaryMar 23 2025 — Apr 22 2025
|
12 Month SummaryApr 22 2024 — Apr 22 2025
|