Lecture
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.