Mercredi 30 mars 3016

Enriched-adjunction models and polarisation for modelling effects and resources

Guillaume Munch-Maccagnoni

University of Cambridge

Résumé: I will present “linear call-by-push-value” enriched-adjunction models refining call-by-push-value models of effects and linear/non-linear models of linear logic, with higher-order functions, sums, and resource modalities, together with a theorem lifting linear models into cartesian ones. I will also present computational interpretations of these models as intuitionistic (linear) logics (LJ/ILL) where the order of evaluation matters, in the form of polarised calculi that satisfy usual properties of Barendregt-style lambda-calculus, and that have sound and coherent interpretations in the previous models. This suggests an approach to modelling proofs and programs with direct models and calculi.

This is a joint work with Marcelo Fiore and Pierre-Louis Curien based on a paper published at POPL 2016.