A Semantic Formulation of ⊤ ⊤-Lifting and Logical Predicates for Computational Metalanguage

  • Shin-ya Katsumata
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)


A semantic formulation of Lindley and Stark’s ⊤ ⊤-lifting is given. We first illustrate our semantic formulation of the ⊤ ⊤-lifting in Set with several examples, and apply it to the logical predicates for Moggi’s computational metalanguage. We then abstract the semantic ⊤ ⊤-lifting as the lifting of strong monads across bifibrations with lifted symmetric monoidal closed structures.


Natural Transformation Semantic Formulation Logical Predicate Closure Operation Typing Context 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M.: TT-closed relations and admissibility. MSCS 10(3), 313–320 (2000)zbMATHMathSciNetGoogle Scholar
  2. 2.
    Amadio, R., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, vol. 46. Cambridge University Press, Cambridge (1998)zbMATHGoogle Scholar
  3. 3.
    G.-Larrecq, J., Lasota, S., Nowak, D.: Logical relations for monadic types. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 553–568. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Girard, J.Y.: Linear logic. Theor. Comp. Sci. 50, 1–102 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Hasegawa, M.: Categorical glueing and logical predicates for models of linear logic. Technical Report RIMS-1223, Research Institute for Mathematical Sciences, Kyoto University (1999)Google Scholar
  6. 6.
    Hermida, C.: Fibrations, Logical Predicates and Indeterminants. PhD thesis, University of Edinburgh (1993)Google Scholar
  7. 7.
    Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)zbMATHGoogle Scholar
  8. 8.
    Johann, P.: Short cut fusion is correct. J. Funct. Program. 13(4), 797–814 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Jung, A., Tiuryn, J.: A new characterization of lambda definability. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 245–257. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  10. 10.
    Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik 23, 113–120 (1970)CrossRefMathSciNetGoogle Scholar
  11. 11.
    Lindley, S.: Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh (2004)Google Scholar
  12. 12.
    Lindley, S., Stark, I.: Reducibility and TT-lifting for computation types. In: TLCA, pp. 262–277 (2005)Google Scholar
  13. 13.
    Ma, Q., Reynolds, J.: Types, abstractions, and parametric polymorphism, part 2. In: Schmidt, D., Main, M.G., Melton, A.C., Mislove, M.W., Brookes, S.D. (eds.) MFPS 1991. LNCS, vol. 598, pp. 1–40. Springer, Heidelberg (1992)Google Scholar
  14. 14.
    MacLane, S.: Categories for theWorking Mathematician, 2nd edn. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1998)Google Scholar
  15. 15.
    Melliès, P.-A., Vouillon, J.: Recursive polymorphic types and parametricity in an operational framework. In: Proc. LICS 2005 (2005) (to appear)Google Scholar
  16. 16.
    Mitchell, J.: Representation independence and data abstraction. In: Proc. POPL, pp. 263–276 (1986)Google Scholar
  17. 17.
    Mitchell, J., Scedrov, A.: Notes on sconing and relators. In: Martini, S., Börger, E., Kleine Büning, H., Jäger, G., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 352–378. Springer, Heidelberg (1993)Google Scholar
  18. 18.
    Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Nishimura, S.: Correctness of a higher-order removal transformation through a relational reasoning. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 358–375. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  20. 20.
    Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. Journal of Symbolic Logic 62(4), 1461–1479 (1997)zbMATHCrossRefMathSciNetGoogle Scholar
  21. 21.
    Pitts, A.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10(3), 321–359 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  22. 22.
    Pitts, A., Stark, I.: Operational reasoning for functions with local state. In: Gordon, A.D., Pitts, A.M. (eds.) Higher Order Operational Techniques in Semantics, Publications of the Newton Institute, pp. 227–273. Cambridge University Press, Cambridge (1998)Google Scholar
  23. 23.
    Plotkin, G.: Lambda-definability in the full type hierarchy. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 367–373. Academic Press, San Diego (1980)Google Scholar
  24. 24.
    Tait, W.: Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic 32 (1967)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Shin-ya Katsumata
    • 1
  1. 1.Research Institute for Mathematical SciencesKyoto University 

Personalised recommendations