Curry-Howard Correspondence in Coq What is Curry-Howard Correspondence and how does the type system of Coq implement it. 2023/04/05 comp @pl @logic en #type-theory #coq