== Praktische Anwendungen == Verfügbare und benutzbare Beweisassistenten/Programmiersprachen wie Coq, Epigram und Agda machen vom Curry-Howard-Isomorphismus Gebrauch, indem sie es gestatten, Beweise als Programme, und Aussagen als Typen anzugeben. Der Typprüfer übernimmt dabei die Aufgabe, die angegebenen Beweise zu verifizieren. == Quellen == ...