Y. Bertot, DR INRIA

Preuve et programmation fiable

L'objectif de ce cours est de décrire comment produire des programmes entièrement corrects vis-à-vis de spécifications logiques en utilisant le système de preuve Coq.