ISR 2010

5th International School on Rewriting

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

Coq and Rewriting


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


(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: