Coq Workshop: Introduction to Interactive Theorem Proving

This lecture introduces Coq, an interactive theorem assistant based on the Curry-Howard isomorphism. It covers the basics of doing proofs in Coq, defining inductive data types, operational semantics, and multi-step evaluation. The workshop aims to give a feel for Coq proofs and the Curry-Howard isomorphism, illustrating their applications.