## Relating computational effects by TT-lifting

**Shin-ya Katsumata**

Kyoto University

Slides from the talk [pdf]

Abstract: When we have two implementations of a programming
language, we are naturally interested in knowing a relationship
between these implementations. Suppose that we obtain two
relationships on 1) data representations in two implementations and 2)
behaviours of side-effects in two implementations. Then the question
is whether the obtained relationships are respected by every program,
that is, for every program *P*, when related data are supplied as
input, the execution of *P* in two implementations raises related
side-effects.

We consider this question in the following theoretical setting:

- For programming languages, we employ λ
_{c}-calculi extended with algebraic operations. We view them as idealised call-by-value functional programming languages. - For implementations, we employ Moggi's monadic semantics of
λ
_{c}-calculi.

We present a sufficient condition for a given set of relationships for values and computations to be respected by every program. This condition is natural, and applicable to any lambda_c-calculus with algebraic operations, monadic semantics and relationships under consideration.

The proof of the condition being sufficient hinges on the technique called categorical TT-lifting. It is a semantic formulation of Lindley and Stark's leapfrog method [3, 4], and constructs logical relations for monads. This construction takes a parameter, and by varying it we can derive various logical relations. In the proof of the sufficiency, we supply the relationship on computations as the parameter - this is the key to achieve the generality of the condition.

If time permits, I will talk about other applications of the categorical TT-lifting. This talk is based on [1, 2].

- S. Katsumata. A semantic formulation of TT-lifting and logical
predicates for computational metalanguage. In L. Ong, ed.,
*Proc. CSL 2005*,*Lect. Notes Comput. Sci.*, v. 3634, pp. 87-102. Springer, 2005. - S. Katsumata. Relating computational effects by
TT-lifting.
*Inf. Comput.*, v. 222, pp. 228--246, 2013. - S. Lindley. Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh, 2004.
- S. Lindley, I. Stark. Reducibility and TT-lifting for computation
types. In P. Urzyczyn, ed.,
*Proc. TLCA*,*Lect. Notes Comput. Sci.*, v. 3461, pp. 262-277. Springer, 2005.

Last changed **
November 23, 2013 0:41 EET**
by
local organizers, nwpt13 (at) ioc.ee