A Generalisation of Pre-logical Predicates to Simply Typed Formal Systems

1. Barendregt, H.: The Lambda Calculus-Its Sytax and Semantics. North-Holland, Amsterdam (1984)

   Google Scholar 

2. Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proc. PPDP 2002, pp. 26–37. ACM Press, New York (2002)

   Chapter  Google Scholar 

3. Fiore, M., Plotkin, G.: An axiomatization of computationally adequate domain theoretic models of FPC. In: Proc. LICS 1994, pp. 92–102. IEEE, Los Alamitos (1994)

   Google Scholar 

4. Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. LICS 1999, pp. 193–202. IEEE Computer Society Press, Los Alamitos (1999)

   Google Scholar 

5. Hermida, C.: Fibrations, Logical Predicates and Indeterminantes. PhD thesis, The University of Edinburgh (1993)

   Google Scholar 

6. Honsell, F., Longley, J., Sannella, D., Tarlecki, A.: Constructive data refinement in typed lambda calculus. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 161–176. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

7. Hoffman, M.: Semantical analysis of higher-order abstract syntax. In: Proc. LICS 1999, pp. 204–213. IEEE Computer Society, Los Alamitos (1999)

   Google Scholar 

8. Honsell, F., Sannella, D.: Prelogical relations. INFCTRL: Information and Computation (formerly Information and Control) 178(1), 23–43 (2002)

   MATH  MathSciNet  Google Scholar 

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

   MATH  Google Scholar 

10. Katsumata, S.: Behavioural equivalence and indistinguishability in higher-order typed languages. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) WADT 2003. LNCS, vol. 2755, pp. 284–298. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

11. Kinoshita, Y., O’Hearn, P.W., Power, A.J., Takeyama, M.: An axiomatic approach to binary logical relations with applications to data refinement. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 191–212. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

12. Kinoshita, Y., Power, J.: Data-refinement for call-by-value programming languages. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 562–576. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

13. Lafont, Y.: Logiques, Categories et Machines. PhD thesis, Université de Paris VII (1988)

    Google Scholar 

14. Leiß, H.: Second-order pre-logical relations and representation independence. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 298–314. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

15. Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)

    Google Scholar 

16. Ma, Q., Reynolds, J.C.: 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 

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. Miculan, M., Scagnetto, I.: A framework for typed HOAS and semantics. In: Proc. PPDP 2003, pp. 184–194. ACM Press, New York (2003)

    Chapter  Google Scholar 

19. Plotkin, G., Power, J., Sannella, D., Tennent, R.: Lax logical relations. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 85–102. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references