Relating computational effects by TT-lifting
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