ausblenden:
Schlagwörter:
-
Zusammenfassung:
In this article, we present the use of the Coq proof
assistant with DESS (Master thesis) students. First, in the
framework of a course of programming language semantics, Coq greatly
helps the students to understand formal and abstract notions, such
as induction, by binding them to more concrete terms. Next,
a computer science project shows that Coq is also
appropriate when dealing with larger problems.
Last, we show how proofs
developed by means of the Focal toolbox made it possible to get
very valuable hints on the development of that system.
