Journal Article
@Article
Artikel in Fachzeitschrift


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | 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