Evènement pour le groupe GT Génie Logiciel

Date 2012-03-08  16:00-17:30
Titreécole Coq GT-GL 
Résumé4 sessions for learning Coq (2/4): Modelling and verifying algorithms in Coq: an introduction The Coq system provides a functional programming language and a reasoning framework based on higher order logic to perform proofs on programs. The expressive power of the language is such that advanced notions of mathematics (such as the graph theory in the four color theorem) or programs of high complexity (such as a compiler for a significant kernel of the C Programming language) can be described formally. In this school, we address the basic programming techniques and approaches to prove properties of the programs. The covered notions involve structural recursive programming, list and integer handling, proof by induction, in the key definition of data-types, pattern matching constructs and case-based reasoning, and inductive properties.  
Lieusalle 178 
OrateurPierre Casteran 

Aucun document lié à cet événement.

Retour à l'index