Curry-Howard Correspondence for Intuitionistic Propositional Logic