COQ - a quick introduction

Thorsten Altenkirch (University of Nottingham)

My MGS course this year introduces COQ as a tool for proof formalisation.

• The COQ homepage
• Slides (updated 17/4/08)
• COQ file from 1st lecture
• 1st set of exercises
• COQ file from 2nd lecture
• 2nd set of exercises
• COQ file from 3rd lecture
• 3rd set of exercises
• COQ file from 4th lecture
• 4th set of exercises