Cours de programmation 2 de Licence de l'ENS de Lyon

Ce cours est assuré par Pierre Lescanne assisté de Philippe Audebaud et Damien Pous .

J'utilise la vidéoprojection

Ce cours parlera de théorie de la démonstration, de calcul symbolique et de sémantique.

• Il présente la déduction naturelle et le lambda-calcul pour introduire la correspondance de Curry-Howard. Il contient cependant une petite incursion vers la théorie des modèles non classiques en introduisant les modèles de Kripke.
• En calcul symbolique nous parlerons de systèmes de récriture (unification, complétion, terminaison).
• En sémantique, nous parlerons de machines abstraites, de sémantique «petite étapes« et «grandes étapes«, de sémantique axiomatique et de sémantique dénotationnelle.

Cours 2007

• Un peu de logique
  • Introduction à la logique
  • à la Hilbert
  • Déduction naturelle
  • Deduction naturelle classique
• Récriture
  • Introduction à la récriture
  • Réductions abstraites
  • Unification
  • Terminaison
  • Complétion
  • Correction de la complétion.
• Lambda calcul
  • Introduction
  • Confluence
  • Lambda calcul typé
  • Logique combinatoire
• Sémantique
  • Sémantique d'un petit langage

Contrôles 2007

• partiel avec son corrigé
• examen final avec son corrigé

Quelques lectures

Quelques biographies: Hilbert, Church 1 2, Curry, Turing, Russel, Heyting, Brouwer, Kolmogorov, Gentzen

Un interview de Church.

Un interview de Kleene et Rosser.

Un article de Jean-Yves Girard.

Deux articles de Wadler sur la correspondance de Curry-Howard.

Un article de Douglas Bridges, paru dans le bulletin de l'EATCS sur ce qu'est la réalité en mathématique. This article introduces three of the twentieth century's main philosophies of mathematics and argues that of those three, one describes mathematical reality, the reality of the other two being virtual.

Divers

Les transparents de 05-06 et le poly 2004 non remis à jour.

L'examen final 2006 et son corrigé (il s'agit d'une nouvelle version du 26 janvier, la précédente comportait des petites fautes...)

• J'utilise un fichier LaTeX pour définir les couleurs.
• Voici l'examen final 2003 et son corrigé.
• Voici l'examen final 2004.
• Voici l'examen final 2005.
• Un tar de tout mes fichiers sources (2006);