Relative monads and lambda-calculus

James Chapman

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
Last update 15.1.2012