Laboratoire d'informatique de l'École polytechnique

Séminaire par Marie Kerjean: «Towards a type theory for differential equations»

Speaker: Marie Kerjean
Location: Salle Grace Hopper
Date: Wed, 28 Nov 2018, 10:30-12:00

Pour le prochain séminaire de l'équipe Cosynus, nous aurons le plaisir d'accueillir Marie Kerjean qui nous parlera de liens entre logique et équations différentielles.

Résumé: Linear Logic (LL) is a resource-aware refinement of intuitionnistic and classical logic, introduced after a study of denotational models of lambda-calculus. Differential Linear Logic (DiLL) spawned from denotational models LL based on vector spaces. While LL enriches logic with tools from algebra, DiLL transports those of differential calculus.

In this talk I will explain how we can refine DiLL into a system which solves linear partial differential equations with constant coefficients. This is done via a semantics study of DiLL, with a focus on smooth and classical models, in which the exponential is interpreted as a space of distributions. From this model, we can then understand exponentials as spaces of solutions to differential equations.