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.
Présentation générale de Coq basée sur les transparent d'Yves Bertot [pdf]
Lien vers la documentation de ZArith ZArith
Suite des travaux pratiques en logique sur le fichier [coq, html]
Nouveaux travaux pratiques : [exo4.v et Reinventer_la_roue.v]
Consolidations des bases vues. Nous allons essayer de refaire les exemples du TP précédents. Fichier associé tp.v
Suite de la séance précédente
Propriétés inductives: slides, demo, exercices, solutions.
Suite de la séance précédente
Suite sur les propriétés inductives: slides, sources des exemples des slides, exercices
Début de formalisation d'un petit langage de programmation. source coq
Séance d'exercices: Semantics1.v, Tools.v, exercise1.txt.
Poursuite du travail sur la sémantique: contruction d'un programme qui boucle et preuve qu'il boucle.
Sémantique à grands pas: Semantics_simple.v
Petite digression sur les types co-inductifs: Coninduc_simpl.v et plus difficile: Coinduc.v
Systèmes de transition:LTS.v
Types co-inductifs suite Coninduc_simpl.v.
Propriétés inductives: exercices d'analyses proposés par le Coq'Art dyck.v
Complétude de la reconnaissance pour le langage de Dyck dyck_rec.v