Journal Article
@Article
Artikel in Fachzeitschrift

Show entries of:

this year (2024) | last year (2023) | two years ago (2022) | Notes URL

Action:

login to update
Options:








Author, Editor(s)
Author(s):
Delahaye, David
Jaume, Mathieu
Prevosto, Virgile		dblp
dblp
dblp
Not MPG Author(s):
Delahaye, David
Jaume, Mathieu

BibTeX cite key*:

DelahayeJaumePrevosto2005

Title

Title*:

Coq, un outil pour l'enseignement

Journal

Journal Title*:

Technique et Science Informatiques
Journal's URL:


Download URL
for the article:


Language:

French

Publisher

Publisher's
Name:

Hermès Science
Publisher's URL:


Publisher's
Address:


ISSN:


Vol, No, pp, Date

Volume*:

24
Number:

9

Publishing Date:

2005

Pages*:

1139-1160
Number of
VG Pages:


Page Start:


Page End:


Sequence Number:


DOI:


Note, Abstract, ©

Note:


(LaTeX) 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.

URL for the Abstract:


Categories,
Keywords:

teaching, semantics of programming languages, formal conception, Coq, Focal

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Intranet

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography, VG Wort


BibTeX Entry:
@ARTICLE{DelahayeJaumePrevosto2005,
AUTHOR = {Delahaye, David and Jaume, Mathieu and Prevosto, Virgile},
 TITLE = {Coq, un outil pour l'enseignement},
 JOURNAL = {Technique et Science Informatiques},
 PUBLISHER = {Hermès Science},
 YEAR = {2005},
 NUMBER = {9},
 VOLUME = {24},
 PAGES = {1139--1160},
}

Entry last modified by Christine Kiesel, 01/28/2008
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Uwe Waldmann		Created
04/22/2005 01:44:56 PM
Revisions
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Virgile Prevosto
Virgile Prevosto
Uwe Waldmann
Edit Dates
25.04.2006 20:13:53
11/18/2005 01:09:30 PM
10/26/2005 03:43:44 PM
04/22/2005 01:44:56 PM