Sam Lindley and Ian Stark
In Typed Lambda Calculi and Applications: Proceedings of the 7th International Conference TLCA 2005, Nara, Japan, April 21–23, 2005, Lecture Notes in Computer Science 3461, pages 262–277. Springer-Verlag, 2005.
Fetch the paper and slides from the conference presentation. Go to other papers, talks or home page.
We propose TT-lifting as a technique for extending operational predicates to Moggi's monadic computation types, independent of the choice of monad. We demonstrate the method with an application to Girard-Tait reducibility, using this to prove strong normalisation for the computational metalanguage λml.
The particular challenge with reducibility is to apply this semantic notion at computation types when the exact meaning of "computation" (stateful, side-effecting, nondeterministic, etc.) is left unspecified. Our solution is to define reducibility for continuations and use that to support the jump from value types to computation types. The method appears robust: we apply it to show strong normalisation for the computational metalanguage extended with sums, and with exceptions. Based on these results, as well as previous work with local state, we suggest that this "leap-frog" approach offers a general method for raising concepts defined at value types up to observable properties of computations.
@InProceedings{lindley/stark:reducibility, author = {Sam Lindley and Ian Stark}, title = {Reducibility and $\top\top$-lifting for Computation Types}, booktitle = {Typed Lambda Calculi and Applications: Proceedings of the Seventh International Conference TLCA~2005}, pages = {262--277}, year = 2005, series = {Lecture Notes in Computer Science}, number = 3461, publisher = {Springer-Verlag}, url = {http://www.inf.ed.ac.uk/~stark/reducibility.html}, pdf = {http://www.inf.ed.ac.uk/~stark/reducibility.pdf} }