Abstract

Constructive logic codifies the principles of mathematical reasoning where a proposition is judged true with a proof, and is judges false with a refutation. It associates with programs with proposition as type and proof as expression. In this talk, I will give an brief introduction of constructive logic together with a little mention of classical logic and their relationship.