Alfa är en efterföljare till beviseditorn ALF, dvs en editor för direktmanipulering av bevisobjekt i ett logiskt ramverk baserat på Per Martin-Löfs typteori. Med Alfa kan man, interaktivt och inkrementellt, definiera teorier (axiom och härledningsregler), formulera satser och konstruera bevis av satser. Alla steg i beviskonstruktionen kontrolleras direkt av systemet, så det är omöjligt att konstruera felaktiga bevis.
Man kan också se Alfa som ett syntaxorienterad redigeringsprogram för ett litet, rent funktionellt programmeringsspråk med ett typsystem som har beroende typer. Det funktionella språket är i själva verket mycket likt språket Cayenne av Lennart Augustsson.
Alfa utvecklas av några av medlemmarna i
Programmeringslogikgruppen vid Chalmers.
Alfa utnyttjar ett beviskontrollprogram som ursprungligen skrevs
av Thierry Coquand (V3) och sedan vidareutvecklades
av Catarina Coquand
(Agda).
De senaste förbättringarna av Agda har gjorts av
Makoto Takeyama. Han har lagt till
idata-konstruktionen, för att få tillbaka en del av den
uttryckskraft som fanns i de induktiva datadefintionerna i det gamla
ALF-systemet.
Alfa har också visst stöd för att arbeta med översättningar av bevis till naturligt språk, genom att koppla ihop Alfa med Aarne Rantas Grammatiska Ramverk, GF.
Det grafiska användargränssnittet och infrastrukturen som kopplar samman alltihop implementeras av Thomas Hallgren. Alla programdelar skrivs i språket Haskell.
Vill du ladda ner Alfa, se nedan.
Alfa har testats och fungerar på bland annat följande system (oktober 2000):
Uppdatering 2020-10-26: uppdaterade källkodpaket för Fudgets och Alfa är nu tillgängliga, för att göra det lättare att kompilera Alfa med de senaste versionerna av GHC. Det binära installationspaketet för macOS som nämns ovan finns också kvar.