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

1. Abadi, M.: TT-closed relations and admissibility. MSCS 10(3), 313–320 (2000)

   MATH  MathSciNet  Google Scholar 

2. Amadio, R., Curien, P.-L.: Domains and Lambda-Calculi. Cambridge Tracts in Theoretical Computer Science, vol. 46. Cambridge University Press, Cambridge (1998)

   MATH  Google Scholar 

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)

   Chapter  Google Scholar 

4. Girard, J.Y.: Linear logic. Theor. Comp. Sci. 50, 1–102 (1987)

   Article  MATH  MathSciNet  Google Scholar 

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. Hermida, C.: Fibrations, Logical Predicates and Indeterminants. PhD thesis, University of Edinburgh (1993)

   Google Scholar 

7. Jacobs, B.: Categorical Logic and Type Theory. Elsevier, Amsterdam (1999)

   MATH  Google Scholar 

8. Johann, P.: Short cut fusion is correct. J. Funct. Program. 13(4), 797–814 (2003)

   Article  MATH  MathSciNet  Google Scholar 

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)

   Chapter  Google Scholar 

10. Kock, A.: Strong functors and monoidal monads. Archiv der Mathematik 23, 113–120 (1970)

    Article  MathSciNet  Google Scholar 

11. Lindley, S.: Normalisation by Evaluation in the Compilation of Typed Functional Programming Languages. PhD thesis, University of Edinburgh (2004)

    Google Scholar 

12. Lindley, S., Stark, I.: Reducibility and TT-lifting for computation types. In: TLCA, pp. 262–277 (2005)

    Google Scholar 

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. MacLane, S.: Categories for theWorking Mathematician, 2nd edn. Graduate Texts in Mathematics, vol. 5. Springer, Heidelberg (1998)

    Google Scholar 

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. Mitchell, J.: Representation independence and data abstraction. In: Proc. POPL, pp. 263–276 (1986)

    Google Scholar 

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. Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)

    Article  MATH  MathSciNet  Google Scholar 

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)

    Chapter  Google Scholar 

20. Parigot, M.: Proofs of strong normalisation for second order classical natural deduction. Journal of Symbolic Logic 62(4), 1461–1479 (1997)

    Article  MATH  MathSciNet  Google Scholar 

21. Pitts, A.: Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10(3), 321–359 (2000)

    Article  MATH  MathSciNet  Google Scholar 

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. 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. Tait, W.: Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic 32 (1967)

    Google Scholar 

Download references