Les sessions du second semestre ont pour prérequis les cours du premier semestre.
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.