Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

Coq edu20tsi3904 See discussions stats and author pro ?les for this publication at https www researchgate net publication Coq un outil pour l'enseignement Article January Source OAI CITATIONS READS authors including David Delahaye Laboratoire d'Informatiq

See discussions stats and author pro ?les for this publication at https www researchgate net publication Coq un outil pour l'enseignement Article January Source OAI CITATIONS READS authors including David Delahaye Laboratoire d'Informatique de Robotique et de Microélectronique de Montpellier ? PUBLICATIONS CITATIONS SEE PROFILE Virgile Prevosto Atomic Energy and Alternative Energies Commission PUBLICATIONS CITATIONS SEE PROFILE Some of the authors of this publication are also working on these related projects Relational Properties View project Automated Deduction View project All content following this page was uploaded by David Delahaye on May The user has requested enhancement of the downloaded ?le CAPPLICATION Coq un outil pour l ? enseignement Une expérience avec les étudiants du DESS Développement de logiciels sûrs David Delahaye ?? Mathieu Jaume ?? Virgile Prevosto CPR ?? CEDRIC ?? CNAM rue St Martin F- Paris Cedex France David Delahaye cnam fr SPI ?? LIP ?? Université Pierre et Marie Curie Rue du Capitaine Scott F- Paris France Mathieu Jaume lip fr Max-Planck Institut für Informatik Stuhlsatzenhausweg D- Saarbrücken Allemagne INRIA Rocquencourt BP F- Le Chesnay Cedex France prevosto mpi-inf mpg de virgile prevosto inria fr RÉSUMÉ Cet article présente l ? emploi de l ? outil d ? aide à la preuve Coq auprès d ? étudiants de DESS e cycle universitaire D ? abord dans le cadre d ? un cours de sémantique des langages Coq facilite l ? appropriation par les étudiants de notions souvent jugées abstraites en leur permettant de les relier à des termes plus concrets Ensuite un projet informatique utilise Coq pour traiter des problèmes de plus grande envergure faisant appara? tre par là-même Coq comme un véritable outil de génie logiciel En ?n la réalisation de preuves dans l ? atelier Focal a permis de fructueuses interactions avec le développement de ce système ABSTRACT 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 MOTS -CLÉS enseignement sémantique conception formelle Coq Focal KEYWORDS teaching semantics of programming languages formal conception Coq Focal RSTI - TSI ?? Langages applicatifs pages à ? C RSTI - TSI ?? Langages applicatifs Introduction Dans cet article nous présentons comment l ? assistant à la preuve Coq a été utilisé durant ces trois dernières années de à comme outil d ? enseignement auprès des étudiants du DESS DLS ??Développement de Logiciels Sûrs ? du CNAM et de l ? université Pierre et Marie Curie Le DESS DLS forme chaque année environ étudiants aux métiers de la sûreté et de la sécurité des systèmes à logiciel prépondérant