5th International School on Rewriting

3 – 8 July 2010, Drift 21, Utrecht, Netherlands

Coq and Rewriting

Lecturer

Adam Koprowski (R&D MLstate, Paris, France)

Introduction

(advanced track, 3 sessions, mixed theoretical and practical)

Coq is an interactive theorem prover. On the one hand it allows to express mathematical theorems and mechanically check correctness of their proofs. On the other hand it encompasses a functional programming language, allowing to write programs within the system and reason about their correctness, hence providing a software verification platform. This course will:

• introduce Coq as a tool;
• present recent work in the term rewriting community on using theorem proving technology to certify termination proofs for term rewriting systems; and
• include lab sessions, where students will be presented with a number of exercises, giving them an opportunity to have a hands-on experience with the system.

• Material

  • preparation: install coq (Coq 8.2pl1)
    please see this web-site for informaton on the Coq installation required for this course.