Accueil Publimath  Aide à la recherche   Recherche Avancée   Aidez-nous à améliorer cette fiche 
Certification IDDN Valid HTML 4.01 Transitional
Auteur(s) : Regnier Laurent

Titre : Quadrature. Num. 49. p. 13-22. Les limites de la correspondance preuve/programme.

Editeur : EDP sciences Les Ulis, 2003
Format : A4, p. 13-22 Bibliogr. p. 22-22
  ISSN : 1142-2785

Type : article de périodique ou revue Langue : Français Support : papier

Public visé : élève ou étudiant, enseignant, tout public Niveau : licence Age : 18, 19, 20

Classification : A35Revues, article de revue A38Revues, article de revue E35Logique. Acquisition des capacités de raisonnement logique. E38Logique. Acquisition des capacités de raisonnement logique. E55Méthodes de démonstration. Raisonnement et démonstrations en classe de mathématiques. E58Méthodes de démonstration. Raisonnement et démonstrations en classe de mathématiques. 

Résumé :

Ce long article décrit le champ scientifique de la logique de programmation. Après quelques rappels historiques et philosophiques, l'auteur présente le système axiomatique formel des séquents de Gentzen et son théorème d'élimination des coupures (le Hauptsatz). Ensuite, il explique l'isomorphisme de Curry-Howard entre preuve logique et programme informatique.

Notes :
Quadrature est un magazine de mathématiques pures et appliquées. Il s’adresse aux enseignants, étudiants, ingénieurs et amateurs de mathématiques.
Tout internaute peut acheter le numéro en cours et les anciens numéros sur la site de la revue quadrature.info (ISSN de l'édition électronique : 1760-4826).

Une version texte intégral est en téléchargement sur le site http://www.i2m.univ-amu.fr/perso/laurent.regnier/articles/

Mots clés :


© ADIREM-APMEP -2003- ISSN 1292-8054 Mise à jour 12/06/2018
Accueil Publimath  Aide à la recherche   Recherche Avancée   Aidez-nous à améliorer cette fiche 
Certification IDDN