Petite école de Coq au LaBRI

Cette école a pour objectif de diffuser la connaissance de Coq au sein du LaBRI tant à des fins de recherche que d'enseignement.

Elle est animée par Pierre Casteran et à lieu les lundis de 9h à 10h en salle 178 du LaBRI.

List de diffusion

Première séance 7/10/2013

Présentation générale de Coq basée sur les transparent d'Yves Bertot [pdf]

Seconde séance 14/10/2013

Travaux Pratiques [coq, html]

Lien vers la documentation de ZArith ZArith

Troisième séance 21/10/2013

Suite des travaux pratiques en logique sur le fichier [coq, html]

Quatrième séance 4/11/2013

Nouveaux travaux pratiques : [exo4.v et Reinventer_la_roue.v]

Cinquième séance 12/11/2013

Consolidations des bases vues. Nous allons essayer de refaire les exemples du TP précédents. Fichier associé tp.v

Sixième séance 19/11/2013

Suite de la séance précédente

Septième séance 25/11/2013

Propriétés inductives: slides, demo, exercices, solutions.

Huitièmes séance 2/12/2013

Suite de la séance précédente

Neuvième séance 9/12/2013

Suite sur les propriétés inductives: slides, sources des exemples des slides, exercices

Dixième séance 13/1/2014

Début de formalisation d'un petit langage de programmation. source coq

Onzième séance 20/1/2014

Séance d'exercices: Semantics1.v, Tools.v, exercise1.txt.

Douzième séance 27/1/2014

Poursuite du travail sur la sémantique: contruction d'un programme qui boucle et preuve qu'il boucle.

Treizième séance 3/2/2014

Sémantique à grands pas: Semantics_simple.v

Quatorzième séance 10/2/2014

Petite digression sur les types co-inductifs: Coninduc_simpl.v et plus difficile: Coinduc.v

Quinzième séance 17/2/2014

Systèmes de transition:LTS.v

Seizième séance 3/3/2014

Types co-inductifs suite Coninduc_simpl.v.

Dix-septième séance 17/3/2014

Propriétés inductives: exercices d'analyses proposés par le Coq'Art dyck.v

Vingtième séance 14/4/2014

Complétude de la reconnaissance pour le langage de Dyck dyck_rec.v


Quelques liens intéressants:
Sylvain Salvati