Reducibility and TT-lifting for computation types

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 lambda(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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications
EditorsP Urzyczyn
Place of PublicationBerlin
PublisherSpringer-Verlag GmbH
Number of pages16
ISBN (Electronic)978-3-540-25593-2
ISBN (Print)978-3-540-25593-2
Publication statusPublished - 2005
Event7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005) - Nara, Japan
Duration: 21 Apr 200523 Apr 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005)


  • strong normalization
  • monads
  • natural deduction


Dive into the research topics of 'Reducibility and TT-lifting for computation types'. Together they form a unique fingerprint.

Cite this