Cours
Master Recherche Informatique
Filière Modélisation et
Vérification
Cours
Master Professionnel Informatique (2ième année)
__________________________________________________________________________________________
Module Méthodes formelles
Programme
- Lambda-Calcul,
termes, beta-réduction, normalisation.
Lambda-Calcul typé,
systèmes de types, synthèse et vérification de
types
- Déduction
naturelle: le système
minimal, dérivations,
interprétation
fonctionnelle
(Curry-Howard), le système intuitionniste.
- Initiation au
système Coq par l'exemple (Notes de cours pdf)
- Développement interactif, tactiques
élémentaires,
mécanisme
de sections, preuves propositionnelles.
- Polymorphisme et ordre supérieur : identité
polymorphique et
imprédicativité.Types dépendants, logique des
prédicats. Abstration
types/types
- Induction, récursion. Définitions, preuves par
induction. L'égalité de Leibniz
et les tactiques associées. Les connecteurs inductifs.
L'inversion.
- Développement d'un bibliothèque sur les vecteurs de
bits.
Application à
la spécification et vérification d'un additionneur.
- Le
principe de coinduction, la coinduction en Coq. Application
à la
modélisation
d'automates et de circuits séquentiels synchrones.
- Logique
Temporelle Linéaire, exemples. Axiomatisation en
Coq.
- Application à la spécification formelle d'un
récupérateur de mémoire et à
l'expression des propriétés à prouver.
Architecture de la preuve.
- Introduction
à CCS. Exemples. Simulations, bisimulations.
Axiomatisation en Coq.
__________________________________________________________________________________________
Bibliographie
Logique,
réduction,
résolution. René Lalement. Masson.
Le Coq'Art. Y. Bertot et
P.
Castéran.
Springer-Verlag.
Circuit
Certification in Type Theory, S.
Coupet-Grimal et L. Jakubiec.
Copyright :
Springer-Verlag. Formal
Aspects of Computing .
Vol 16 No 4, pp 352 - 373, Nov 2004.
An
Axiomatization
of Linear Temporal Logic in The Calculus of Inductive Constructions,
S.
Coupet-Grimal. The Journal of Logic and
Computation,
Vol 13 No 6, pp 801-813, 2003
Formal
Verification
of an Incremental Garbage Collector.
S. Coupet-Grimal, C. Nouvet, The
Journal of Logic and
Computation,
Vol 13 No 6, pp 815-833, 2003.
_____________________________________________________________________________________________
TD1 Apprentissage du Lambda-Calcul pur
comme langage de programmation. ps, pdf
TD2 Introduction au Lambda-Calcul
simplement typé. ps, pdf
TD3 Autres principes de récurrence
et arithmétique. ps,
pdf
TD4 Définitons inductives et
récursives, prédicats odd et even, listes. ps,
pdf
TD5
Certification
en Coq d'un additionneur n-bits. ps,
pdf.