CSC535: Coq: The Coq Proof Assistant [18/21]

• Developed at the INRIA research lab near Paris over the past 20 years
• Based on an extremely expressive logical foundation
  • The Calculus of Inductive Constructions
  • (hence the name!)
• Has been used to check a wide range of significant mathematical results
  • Gonthier's fully verified proof of the four-color theorem
  • Leroy's verified certifying compiler