Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages
We extend the study of the relationship between behavioural equivalence and the indistinguishability relation [4,7] to the simply typed lambda calculus, where higher-order types are available. The relationship between these two notions is established in terms of factorisability . The main technical tool of this study is pre-logical relations , which give a precise characterisation of behavioural equivalence. We then consider a higher-order logic to reason about models of the simply typed lambda calculus, and relate the resulting standard satisfaction relation to behavioural satisfaction.
KeywordsLogical Relation Indistinguishability Relation Lambda Calculus Observable Type Lambda Abstraction
Unable to display preview. Download preview PDF.
- 9.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. 149–164. Springer, Heidelberg (2000)Google Scholar
- 11.Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)Google Scholar