Gruppo di Logica e Geometria della Cognizione

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.