Enseignants et ressources officielles

Objectifs d’apprentissage du cours INF9340

Ce cours présente les concepts fondamentaux de la théorie de la démonstration et leurs applications à l’informatique. Il cherche à préparer les étudiants pour entamer un projet de recherche dans ce domaine.

À la fin de ce cours, les étudiants devraient pouvoir:

  1. raisonner au sujet de divers systèmes logiques (par exemple, les logiques propositionnelles, les logiques linéaires, les logiques modales, et leurs variantes intuitionnistes ou classiques) ainsi que faire le lien entre leurs différentes présentations (par exemple, la déduction naturelle, le calcul des séquents, et l’axiomatique hilbertienne);
  2. utiliser divers critères (tels que la correction et la complétude locale, l’élimination de coupures, et la propriété de la sous-formule) comme critères pour évaluer et concevoir des systèmes logiques;
  3. raisonner au sujet de démonstrations en tant qu’objets mathématiques
  4. raisonner au sujet de diverses interprétations computationnelles de systèmes logiques, et comprendre leurs applications à l’informatique, telles que la programmation logique, les systèmes de typage, et la sûreté du typage.

Aperçu du cours INF9340 (pour informaticiennes et informaticiens)

Le cours INF9340 explore les concepts logiques qui sous-tendent les systèmes informatiques de pointe, tels que les langages de programmation quantique, concurrente ou distribuée; l’intelligence artificielle; la vérification de systèmes informatiques; et les langages de requête. Selon les intérêts des personnes inscrites, il traitera des concepts de programmation avancés, tels que la programmation par continuation; la métaprogrammation; et la programmation quantique, concurrente ou distribuée.

Dans ce cours, nous répondrons à des questions telles que:

  • Quels sont les principes à la base de langages de programmation de pointe, tels que Rust, les langages de programmation concurrente et les langages de programmation quantique? Comment permettent-ils de raisonner au sujet de l’utilisation de ressources?
  • Comment peut-on concevoir et implémenter un système d’inférence et de vérification de types qui est à la fois simple et robuste?
  • Quelles sont les différences et les similarités entre divers langages de requête et comment peut-on intégrer leurs différentes fonctionnalités dans un seul système?
  • Quels sont les liens pratiques entre la démonstration et la programmation? Comment peuvent-ils nous guider lors de la conception de langages de programmation? Comment peut-on utiliser des concepts de programmation pour faciliter le raisonnement mathématique et informatique?
  • Quel est le lien entre des techniques de programmation avancées, comme la programmation par continuation, et des paradoxes mathématiques, tels que le paradoxe de Banach-Tarski qui permet de découper une boule et de réassembler ses morceaux pour former deux boules identiques à la première?
  • Comment peut-on concevoir des systèmes logiques adaptés qui permettent de raisonner au sujet d’applications particulières?

Aperçu du cours INF9340 (pour mathématiciennes et mathématiciens)

Le cours INF9340 explore les concepts logiques qui sous-tendent le calcul. Bien que nous sommes habitués en tant que mathématiciennes et mathématiciens de lire et de faire des démonstrations, nous les considérons rarement en tant qu’objets mathématiques. C’est la perspective que nous donne la théorie de la démonstration. Étonnement, il y a un lien profond entre les démonstrations et les programmes. C’est la correspondance de Curry-Howard, qui nous permet d’interpréter les démonstrations comme des programmes, et la simplification de démonstrations comme l’exécution. Différents systèmes logiques induisent différentes notions de calcul. Par exemple, la déduction naturelle correspond à une notion de programmation fonctionnelle; la logique linéaire correspond aux systèmes de réécriture, ou à diverses formes de calcul parallèle ou concurrent; la logique modale correspond à la métaprogrammation ou aux systèmes distribués; et les logiques adjointes captent l’interaction entre le calcul classique et quantique. De plus, la démonstration automatique (la recherche de démonstrations) est elle-même une forme de calcul et, en variant le système logique utilisé, on peut induire différentes sortes de calcul, telles que celles offertes par Prolog et Datalog.

Dans ce cours, nous répondrons à des questions telles que:

  • Quelles sont les propriétés désirables d’un système de logique formelle? En quoi sont-elles reliées à des propriétés de correction des langages de programmation et à la terminaison? Comment peuvent-elles nous guider lors de la conception de systèmes logiques ou de langages de programmation?
  • De quoi a l’air notre univers mathématique si l’on se limite aux fondements mathématiques qui ont un contenu computationnel, c’est à dire, aux mathématiques constructives ou intuitionnistes?
  • Comment peut-on utiliser la correspondance de Curry-Howard-Lambek comme pierre de Rosette pour faire le transfert de résultats entre l’informatique et les mathématiques?