Linear Implicative Algebras, towards a BHK interpretation of linear logic

Luc Pellissier
LIP, ENS Lyon
https://lacl.fr/~lpellissier/

Date(s) : 29/11/2018   iCal
11 h 00 min - 12 h 30 min

Implicative Algebras were recently introduced as a unified framework for forcing and realisability, whose particularity is to interpret terms and formulæ uniformly.

In this ongoing work with Alexandre Miquel, we show how linear logic fits in this picture.

http://lipn.univ-paris13.fr/~pellissier/

Catégories



Retour en haut