Copenhagen Programming Language Seminar

Semantic TT-lifting and its application

Shin-ya Katsumata
RIMS, Kyoto University, Japan.

Tuesday, September 9, 2008, 13:00-14:00
ITU, Rued Langgaards Vej 7, 2300 Copenhagen S. Room: Auditorium 4


I will introduce semantic TT-lifting, a method to give predicate liftings of strong monads. I first illustrate the definition of the TT-lifting in Sets with several examples, and show that it is suitable for extending logical predicates to Moggi's computational metalanguage.
I then move on to a special case of the TT-lifting: the semantic TT-closure operator. I apply it to give a new characterisation of morphisms that are definable by the interpretation of the simply typed lambda calculus with sums in any bi-Cartesian closed category. The TT-closure operator will be used to construct the category in which the collection of definable morphisms at sum types can be characterised as the coproducts of such collections at lower types.

Scientific host:Rasmus Møgelberg Administrative host: Annette Enggaard. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org