Bonjour,
Et bonne rentrée à toutes et tous. Le gdt d'équipe reprend avec un
exposé (ou une série d'exposés, cela dépend de l'intérêt du public)
autour des "algèbres implicatives", une notion que Luc a appris cet été
à l'école de réalisabilité à Montevideo :
________________________________________________________________________
Les algèbres implicatives, d'après A. Miquel
Les structures implicatives sont des structures algèbriques extrèmement
simples généralisant à la fois les modèles dénotationnels du λ-calcul et
les algèbres de Heyting. Elles permettent donc d'interpréter à la fois
les termes et les types, qui se retrouvent ainsi identifiés.
Les structures implicatives sont donc une fondation naturelle pour le
forcing (où l'on interprète les formules dans des algèbres de Boole –
dans le cas classique – ou de Heyting – dans le cas intuitionniste) et
la réalisabilité (où l'on interprète les formules par des ensembles de
λ-termes). On verra qu'en effet, une structure implicative munie d'un
quotient adéquat engendre un tripos, c'est-à-dire un modèle de la
logique intitutionniste d'ordre supérieure (imprédicative).
________________________________________________________________________
Si (comme probable) Luc n'arrivera pas à tout exposer en 1h30 et s'il y
a suffisamment de gens intéressées, on fera la suite vendredi 23
(vendredi 16 la B107 est occupée par autre chose).
Amicalement,
Damiano
