Typtheorie und der Curry-Howard-Isomorphismus: Die tiefgründige Harmonie von Aussagen = Typen und Beweisen = Programmen
