Coq, un outil pour l'enseignement : Une expérience avec les étudiants du DESS Développement de logiciels sûrs
In: Langages applicatifs : spécification, programmation, vérification, Jg. 24 (2005), Heft 9, S. 1139-1160
academicJournal
- print, 17 ref
Zugriff:
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.
Titel: |
Coq, un outil pour l'enseignement : Une expérience avec les étudiants du DESS Développement de logiciels sûrs
|
---|---|
Autor/in / Beteiligte Person: | DELAHAYE, David ; JAUME, Mathieu ; PREVOSTO, Virgile |
Link: | |
Zeitschrift: | Langages applicatifs : spécification, programmation, vérification, Jg. 24 (2005), Heft 9, S. 1139-1160 |
Veröffentlichung: | Paris: Lavoisier, 2005 |
Medientyp: | academicJournal |
Umfang: | print, 17 ref |
ISSN: | 0752-4072 (print) |
Schlagwort: |
|
Sonstiges: |
|