The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Nous prevoyons d'organiser une formation à l'assistant Coq. 
Cette formation aura lieu du lundi 25 au mercredi 27 février à
l'université Paris Sud (Orsay).

N'hésitez pas à transmettre cette annonce aux personnes autour de vous
qui pourraient être intéressées.

Des informations provisoires sur l'organisation de la formation sont
disponibles : http://www.lri.fr/~paulin/FORMATION

Ce stage s'adresse à des personnes travaillant dans le domaine de la
programmation ou de la modélisation qui souhaitent utiliser un langage
et des outils permettant de formellement spécifier et valider des
systèmes critiques.

Objectifs : Être capable de réaliser des modélisations de systèmes
informatiques à l'aide de l'assistant Coq. S'initier aux
fonctionnalités avancées de cet outil : paramétrisation de théories,
 création de tactiques de preuve, génération automatique de code.

Programme :
La formation comprend des cours de présentation et inclut pour la
moitié une formation pratique sur machine.

Jour 1 : Présentation générale de l'outil Coq, langage de
description de modèles, tactiques de preuves élémentaires.
Jour 2 : Aspects avancés du langage de spécification (définition
inductives, coinductives, modélisation de sémantique)
Jour 3 : Outils de certification de programmes, langage de tactiques, 
développer une tactique certifiée.

Les personnes intéressées par cette formation sont invitées à m'envoyer
un courrier électronique : 
mailto:Christine.Paulin AT lri.fr

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84