Formalizing logics using Agda Programming Language In this project, we formalize logic properties using Agda. Up to now, we have some properties for the propositional version of sequent calculus.