Institute of Cybernetics at TUT
Thursday, 12 January 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: I will describe the relative monad structure of the untyped/typed lambda-terms which captures the notion of parallel substitution. Interestingly, the algebras for these monads are models (evaluators/interpreters/semantics) of the lambda-terms. I will explain the machinery of relative monads and their algebras, and go through the implementations of the lambda-term examples in the programming language Agda.
(Joint work Thorsten Altenkirch and Tarmo Uustalu.)
Tarmo Uustalu