Colloquium di matematica: "On the mathematical interpretation of programs and proofs"

Thomas Ehrhard CNRS, directeur du laboratoire Preuves, Programmes et Syste'mes (PPS) Universite' Paris Diderot - Paris 7
evento esterno
14/10/2015 - 16:00
Dipartimento di Matematica e Fisica Universita' degli Studi Roma Tre Aula F, primo piano, edificio Aule - Largo San Leonardo Murialdo,1

We shall see how the notions of monoidal categories, adjunctions and monads/comonads are deeply connected to the mathematical interpretation of functional computer programs and of mathematical proofs. We shall illustrate how this interpretation can suggest improvements of the syntax of programs. For instance, it allows to accommodate the call-by-name and the call-by-value evaluation strategies in a common functional setting, or provides a simple algebraic understanding of the "call with current continuation" primitive of the language scheme, both using the category of coalgebras of a comonad.