Actualités
  Période
semaine
ou mois
aucune période


  Thèmes:
Thèses
Colloques
Autres
Groupes
Tous les thèmes

   
  Liens:
Voir les thèses

Voir les colloques

Voir les autres événements

Voir la page des groupes

Accéder à l'intranet

Intitulé:   
école Coq GT-GL
du 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 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index