Preuves et programmes (LMFI)

Cours 1: Algèbre initiale

Algèbre intiale (pour un foncteur)

Imprédicativité:

Comment pallier le problème de définition circulaire des candidats de réductibilité $Red(∀X. A)$ ?

Expression, dans Peano, du fait que $Red_ρ(A)$ est un candidat de réductibilité:

Introduction

Dans une Catégorie Cartésienne Close (CCC)

Espaces cohérents

Catégories $Coh$ et $Stab$

Rappel: Le bang $!: Stab ⟶ Coh$ est l’adjoint à gauche du foncteur d’oubli $𝒰: Coh ⟶ Stab$:

Traduction de Girard

Réseaux de preuves pour MLL

Rappels

Nouveau professeur pour cette seconde partie : Michele Pagani

Friedman:

Expressivité

Rappels

Th: Let $M$ be a PCF program, then \[⟦M⟧ = n \text{ iff } M ⟶^\ast \underline{n}\]

cf. Linear Logic, Girard (1987)

Caractérisation des espaces cohérents

In Probabilistic Coherence Spaces, $𝒫(𝒜)$ is closed under $\sup$

1. Le produit monoïdal $\otimes$ de $PCoh$