Logic Foundation and Machine-checked Proofs

2.0 credits

This seminar teaches the theoretical equivalence between programming languages and mathematical logic. Topics include functional programming, proof by induction, proof tactics, logic, inductively defined propositions, and the Curry-Howard Correspondence. The interactive theorem prover called Coq is used to write machine-checked proofs. Students enrolling in the course are expected to have advanced knowledge in either programming languages (CSC 253, 254 or 255) or mathematical logic.