Abstract
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 [4]. The main technical tool of this study is pre-logical relations [8], 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andrews, P.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, London (1986)
Barendregt, H.: The Lambda Calculus-Its Syntax and Semantics. North Holland, Amsterdam (1984)
Bidoit, M., Hennicker, R.: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science 165(1), 3–55 (1996)
Bidoit, M., Hennicker, R., Wirsing, M.: Behavioural and abstractor specifications. Science of Computer Programming 25(2-3), 149–186 (1995)
Bidoit, M., Tarlecki, A.: Behavioural satisfaction and equivalence in concrete model categories. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol. 1059, pp. 241–256. Springer, Heidelberg (1996)
Henkin, L.: Completeness in the theory of types. Journal of Symbolic Logic 15, 81–91 (1950)
Hofmann, M., Sannella, D.: On behavioural satisfaction and behavioural abstraction in higher-order logic. Theoretical Computer Science 167(1-2), 3–45 (1996)
Honsell, F., Sannella, D.: Pre-logical relations. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 546–561. Springer, Heidelberg (1999); An extended version is in Information and Computation 178, 23–43 (2002)
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)
Mitchell, J.: On the equivalence of data representations. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 305–330. Academic Press, San Diego (1991)
Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)
Schoett, O.: Behavioural correctness of data representations. Science of Computer Programming 14, 43–57 (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Katsumata, Sy. (2003). Behavioural Equivalence and Indistinguishability in Higher-Order Typed Languages. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds) Recent Trends in Algebraic Development Techniques. WADT 2002. Lecture Notes in Computer Science, vol 2755. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-40020-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-40020-2_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20537-1
Online ISBN: 978-3-540-40020-2
eBook Packages: Springer Book Archive