11 ressources en auto-formation : preuve de programme

FILTRES

11 résultats
page 1 sur 2
Résultats de 1 à 10
Présentation de la ressource en auto-formation Approches fonctionnelles de la programmation cours / présentation
23/02/2009
Approches fonctionnelles de la programmation
Auteur(s) : Verna Didier
Description : Fournir un panorama complet du paradigme de programmation fonctionnelle et de son positionnement par rapport aux autres paradigmes de programmation (en particulier de la programmation impérative). Illustrer l'ensemble des concepts abordés au moyen de deux langages fonctionnels: Lisp et Haskell.
Présentation de la ressource en auto-formation Demandez le programme cours / présentation, démonstration
17/02/2009
Demandez le programme
Auteur(s) : Boldo Sylvie
Description : La programmation consiste à décomposer un algorithme en ordres simples et à les écrire en un langage compréhensible par l’ordinateur.
Présentation de la ressource en auto-formation Du rêve à la réalité des preuves cours / présentation, démonstration
08/06/2012
Du rêve à la réalité des preuves
Auteur(s) : Delahaye Jean-Paul
Description : Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens.
Présentation de la ressource en auto-formation La vérité et la machine cours / présentation, démonstration
30/09/2009
La vérité et la machine
Auteur(s) : Werner Benjamin
Description : Peut-on être sûr de la vérité d’une preuve ? Cette preuve de la preuve, comment l’obtenir en pratique ? La vérification formelle de démonstration est de plus en plus utilisée par les mathématiciens.
Présentation de la ressource en auto-formation Les ingrédients des algorithmes cours / présentation, démonstration
21/04/2010
Les ingrédients des algorithmes
Auteur(s) : Dowek Gilles, Viéville Thierry, Archambault Jean-Pierre, Baccelli Emmanuel, Wack Benjamin
Description : Pour programmer un ordinateur, le plus important ce sont les méthodes mises en œuvre. Découvrez les ingrédients à combiner pour créer ces algorithmes !
Présentation de la ressource en auto-formation Preuves de programmes en coq cours / présentation, outil, exercice, liste de références
21/09/2012
Preuves de programmes en coq
Auteur(s) : Bertot Yves
Description : Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique ...
Présentation de la ressource en auto-formation Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie cours / présentation
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 2ème partie
Auteur(s) : GIRAULT Alain, JEANNET Bertrand
Description : Nous présentons les systèmes embarqués critiques et les exigences qui leur sont liées : dans certains cas (nucléaire, avionique, santé) aucun bug n'est accepté. Puis nous présentons l'analyse statique, que nous illustrons sur un exemple de programme. Nous montrons que pour analyser des variables ...
Présentation de la ressource en auto-formation Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 1ère partie cours / présentation
Analyse de programmes : A quoi ça sert ? Comment ça marche ? : 1ère partie
Auteur(s) : GIRAULT Alain, JEANNET Bertrand
Description : Nous présentons les systèmes embarqués critiques et les exigences qui leur sont liées : dans certains cas (nucléaire, avionique, santé) aucun bug n'est accepté. Puis nous présentons l'analyse statique, que nous illustrons sur un exemple de programme. Nous montrons que pour analyser des variables ...
Présentation de la ressource en auto-formation From symbolic logic to real mathematics cours / présentation
From symbolic logic to real mathematics
Auteur(s) : Paulson Lawrence
Description : Mathematicians have always been prone to error. As proofs get longer and more complicated, the question of correctness looms ever larger. Andrew Wiles’ proof of Fermat’s last theorem contained a flaw that was only fixed a year later. Meanwhile, proof assistants — formal tools originally developed ...
Présentation de la ressource en auto-formation Les nombres et l'ordinateur cours / présentation
Les nombres et l'ordinateur
Auteur(s) : BOLDO Sylvie
Description : Nous confions à nos ordinateurs de nombreux calculs (météo, simulations aéronautiques, jeux vidéos, feuilles Excel...) et nous considérons naturellement que l'ordinateur fournira une réponse juste. Malheureusement, la machine a ses limites que l'esprit humain n'a pas. Elle utilise une ar ...