Most of us learned in kindergarten that intuitionistic logic can be obtained from classical logic by giving up double negation elimination.
A few months later, we learned that Linear logic is a pleasant system to work in as it makes the features of intuitionistic and classical logic apparent.

Widely used logics are arguably composed of three groups ; the identity , the structural and the logical groups.
A large class of logics can then be defined by variation of those rules present in the structural and logical groups.

Proving interesting facts (cut elimination, normalization, invertibility,…) of those logics becomes redundant on an intuitive level and tedious to carry out formally.

Wouldn’t it be great to construct a general framework such that all variations can be explained ? Proving interesting facts about them would only have to be done once and for all. An attempt at deriving such a framework has been published by D. Licata, M.Shulman, and M. Riley in 2017 in , what the speaker consider, a landmark paper.

In this talk, we will go over the main idea of the framework which relies on formalizing a concept of resource usage. Knowledge of category theory is helpful but not required. Knowledge of gentzen style sequent calculus is desired.

The only reference used in this talk is : “A Fibrational Framework for substructural and modal logics”, by the authors mentioned above.