×

Observational program calculi and the correctness of translations. (English) Zbl 1309.68052

Summary: For the issue of translations between programming languages with observational semantics, this paper clarifies the notions, the relevant questions, and the methods; it constructs a general framework, and provides several tools for proving various correctness properties of translations like adequacy and full abstractness, with a special emphasis on observational correctness. We will demonstrate that a wide range of programming languages and programming calculi and their translations can make advantageous use of our framework for focusing the analysis of their correctness.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages

Software:

TALx86; Haskell
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., The lazy lambda calculus, (Turner, D., Research Topics in Functional Programming (1990), Addison-Wesley), 65-116
[2] Abramsky, S.; Ong, C.-H. L., Full abstraction in the lazy lambda calculus, Inform. and Comput., 105, 2, 159-267 (Aug. 1993) · Zbl 0779.03003
[3] Ahmed, A., Step-indexed syntactic logical relations for recursive and quantified types, (Sestoft, P., Programming Languages and Systems, 15th European Symposium on Programming. Programming Languages and Systems, 15th European Symposium on Programming, Lecture Notes in Comput. Sci., vol. 3924 (2006), Springer: Springer Berlin, Heidelberg), 69-83 · Zbl 1178.68146
[4] Ahmed, A.; Blume, M., Typed closure conversion preserves observational equivalence, (Hook, J.; Thiemann, P., Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming (2008)), 157-168 · Zbl 1323.68350
[5] Ahmed, A.; Blume, M., An equivalence-preserving cps translation via multi-language semantics, (Chakravarty, M. M.T.; Hu, Z.; Danvy, O., Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming (2011), ACM: ACM New York, NY, USA), 431-444 · Zbl 1323.68088
[6] Ahmed, A.; Dreyer, D.; Rossberg, A., State-dependent representation independence, (Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2009), ACM: ACM New York, NY, USA), 340-353 · Zbl 1315.68080
[7] The Alice project (2007), Saarland University
[8] Appel, A. W.; McAllester, D., An indexed model of recursive types for foundational proof-carrying code, ACM Trans. Program. Lang. Syst., 23, 5, 657-683 (Sept. 2001)
[9] Astesiano, E.; Costa, G., Nondeterminism and fully abstract models, RAIRO Theor. Inform. Appl., 14, 4, 323-347 (1980) · Zbl 0463.03024
[10] Barendregt, H. P., The Lambda Calculus, Its Syntax and Semantics, Stud. Logic Found. Math., vol. 103 (1984), Elsevier Science · Zbl 0551.03007
[11] Benton, N.; Hur, C.-K., Biorthogonality, step-indexing and compiler correctness, (Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (2009), ACM: ACM New York, NY, USA), 97-108 · Zbl 1302.68083
[12] Carayol, A.; Hirschkoff, D.; Sangiorgi, D., On the representation of McCarthy’s amb in the pi-calculus, Theoret. Comput. Sci., 330, 3, 439-473 (2005) · Zbl 1078.68106
[13] Chlipala, A., A verified compiler for an impure functional language, (Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2010), ACM: ACM New York, NY, USA), 93-106 · Zbl 1312.68044
[14] De Nicola, R.; Hennessy, M., Testing equivalences for processes, Theoret. Comput. Sci., 34, 83-133 (1984) · Zbl 0985.68518
[15] de’Liguoro, U.; Piperno, A., Must preorder in non-deterministic untyped lambda-calculus, (Raoult, J.-C., Proceedings of the 17th Colloquium on Trees in Algebra and Programming. Proceedings of the 17th Colloquium on Trees in Algebra and Programming, Lecture Notes in Comput. Sci., vol. 581 (1992), Springer), 203-220
[16] Felleisen, M., On the expressive power of programming languages, Sci. Comput. Program., 17, 1-3, 35-75 (1991) · Zbl 0745.68033
[17] Ford, J.; Mason, I. A., Formal foundations of operational semantics, High.-Order Symb. Comput., 16, 3, 161-202 (2003) · Zbl 1074.68033
[18] Fournet, C.; Swamy, N.; Chen, J.; Dagand, P.-E.; Strub, P.-Y.; Livshits, B., Fully abstract compilation to JavaScript, (Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2013), ACM: ACM New York, NY, USA), 371-384 · Zbl 1301.68100
[19] Gladstein, D. S.; Wand, M., Compiler correctness for concurrent languages, (Ciancarini, P.; Hankin, C., Proceedings of the First International Conference on Coordination Languages and Models. Proceedings of the First International Conference on Coordination Languages and Models, Lecture Notes in Comput. Sci., vol. 1061 (1996), Springer: Springer London, UK), 231-248
[20] Gordon, A. D., Bisimilarity as a theory of functional programming, Theoret. Comput. Sci., 228, 1-2, 5-47 (1999) · Zbl 0968.68028
[21] Howe, D. J., Proving congruence of bisimulation in functional programming languages, Inform. and Comput., 124, 2, 103-112 (1996) · Zbl 0853.68073
[22] Hu, L.; Hutton, G., Compiling concurrency correctly: cutting out the middle man, (Horváth, Z.; Zsók, V., Selected Papers from the Tenth Symposium on Trends in Functional Programming. Selected Papers from the Tenth Symposium on Trends in Functional Programming, Komarno, Slovakia, June 2009. Selected Papers from the Tenth Symposium on Trends in Functional Programming. Selected Papers from the Tenth Symposium on Trends in Functional Programming, Komarno, Slovakia, June 2009, Trends Funct. Program., vol. 10 (Sept. 2010), Intellect), 17-32
[23] Hur, C.-K.; Dreyer, D., A Kripke logical relation between ML and assembly, (Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2011), ACM: ACM New York, NY, USA), 133-146 · Zbl 1284.68148
[24] Hur, C.-K.; Dreyer, D.; Neis, G.; Vafeiadis, V., The marriage of bisimulations and Kripke logical relations, (Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2012), ACM: ACM New York, NY, USA), 59-72 · Zbl 1321.68198
[25] Jim, T.; Meyer, A., Full abstraction and the context lemma, SIAM J. Comput., 25, 3, 663-696 (1997) · Zbl 0856.03013
[26] Kutzner, A.; Schmidt-Schauß, M., A nondeterministic call-by-need lambda calculus, (Felleisen, M.; Hudak, P.; Queinnec, C., Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming (1998), ACM), 324-335 · Zbl 1369.68106
[27] Leroy, X., Formal verification of a realistic compiler, Commun. ACM, 52, 7, 107-115 (2009)
[28] Mason, I.; Smith, S. F.; Talcott, C. L., From operational semantics to domain theory, Inform. and Comput., 128, 26-47 (1996) · Zbl 0856.68094
[29] McCarthy, J., A basis for a mathematical theory of computation, (Braffort, P.; Hirschberg, D., Computer Programming and Formal Systems (1963), North-Holland: North-Holland Amsterdam), 33-70
[30] McCusker, G., Full abstraction by translation, (Advances in Theory and Formal Methods of Computing (1996), IC Press)
[31] Milner, R., Fully abstract models of typed lambda calculi, Theoret. Comput. Sci., 4, 1, 1-22 (1977) · Zbl 0386.03006
[32] Milner, R., Communication and Concurrency (1989), Prentice Hall · Zbl 0683.68008
[33] Milner, R., Functions as processes, (Proceedings of the Seventeenth International Colloquium on Automata, Languages and Programming (1990), Springer: Springer New York, NY, USA), 167-180 · Zbl 0766.68036
[34] Mitchell, J. C., On abstraction and the expressive power of programming languages, Sci. Comput. Program., 21, 2, 141-163 (1993) · Zbl 0809.68049
[35] Morris, J., Lambda-calculus models of programming languages (1968), MIT, PhD thesis
[36] Morrisett, J. G.; Walker, D.; Crary, K.; Glew, N., From system F to typed assembly language, (MacQueen, D. B.; Cardelli, L., Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1998), ACM), 85-97
[37] Nain, S.; Vardi, M. Y., Branching vs. linear time: semantical perspective, (ATVA (2007)), 19-34 · Zbl 1141.68481
[38] Niehren, J.; Sabel, D.; Schmidt-Schauß, M.; Schwinghammer, J., Observational semantics for a concurrent lambda calculus with reference cells and futures, 23rd Conference on Mathematical Foundations of Programming Semantics. 23rd Conference on Mathematical Foundations of Programming Semantics, Electron. Notes Theor. Comput. Sci., 173, 313-337 (Apr. 2007) · Zbl 1316.68034
[39] Niehren, J.; Schwinghammer, J.; Smolka, G., A concurrent lambda calculus with futures, Theoret. Comput. Sci., 364, 3, 338-356 (Nov. 2006) · Zbl 1110.68023
[40] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous pi-calculus, (Lee, P.; Henglein, F.; Jones, N. D., Proceedings of 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1997), ACM Press), 256-265
[41] Peyton Jones, S.; Gordon, A.; Finne, S., Concurrent Haskell, (Boehm, H.-J.; Steele, G. L., Proceedings of the 23rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (1996), ACM), 295-308
[42] Pierce, B. C., Types and Programming Languages (2002), MIT Press
[43] Pitts, A. M., Parametric polymorphism and operational equivalence, Math. Structures Comput. Sci., 10, 321-359 (2000) · Zbl 0955.68024
[44] Pitts, A. M., Howe’s method for higher-order languages, (Sangiorgi, D.; Rutten, J., Advanced Topics in Bisimulation and Coinduction. Advanced Topics in Bisimulation and Coinduction, Cambridge Tracts Theoret. Comput. Sci., vol. 52 (Nov. 2011), Cambridge University Press), 197-232, Chapter 5 · Zbl 1285.68110
[45] Plotkin, G. D., LCF considered as a programming language, Theoret. Comput. Sci., 5, 3, 225-255 (1977) · Zbl 0369.68006
[46] Rau, C.; Sabel, D.; Schmidt-Schauß, M., Correctness of program transformations as a termination problem, (Gramlich, B.; Miller, D.; Sattler, U., Proceedings of the 6th International Joint Conference on Automated Reasoning. Proceedings of the 6th International Joint Conference on Automated Reasoning, Lecture Notes in Comput. Sci., vol. 7364 (2012), Springer: Springer Berlin, Heidelberg), 462-476 · Zbl 1358.68076
[47] Rau, C.; Schmidt-Schauß, M., A unification algorithm to compute overlaps in a call-by-need lambda-calculus with variable-binding chains, (Proceedings of the 25th International Workshop on Unification (2011)), 35-41
[48] Riecke, J. G., Fully abstract translations between functional languages, (Wise, D. S., Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages (1991), ACM), 245-254
[49] Ritter, E.; Pitts, A. M., A fully abstract translation between a lambda-calculus with reference types and Standard ML, (Dezani-Ciancaglini, M.; Plotkin, G. D., Proceedings of the Second International Conference on Typed Lambda Calculi and Applications. Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, Lecture Notes in Comput. Sci., vol. 902 (1995), Springer), 397-413 · Zbl 1063.68551
[50] Sabel, D., Semantics of a call-by-need lambda calculus with McCarthy’s amb for program equivalence (November 2008), Goethe-Universität Frankfurt, Institut für Informatik, Fachbereich Informatik und Mathematik, PhD thesis
[51] Sabel, D., An abstract machine for Concurrent Haskell with futures, (Jähnichen, S.; Rumpe, B.; Schlingloff, H., Software Engineering 2012 Workshopband. Software Engineering 2012 Workshopband, GI Ed. Lect. Notes Inform., vol. 199 (February 2012)), 29-44, (5. Arbeitstagung Programmiersprachen (ATPS’12))
[52] Sabel, D.; Schmidt-Schauß, M., A call-by-need lambda-calculus with locally bottom-avoiding choice: context lemma and correctness of transformations, Math. Structures Comput. Sci., 18, 3, 501-553 (2008) · Zbl 1153.68011
[53] Sabel, D.; Schmidt-Schauß, M., A contextual semantics for Concurrent Haskell with futures, (Schneider-Kamp, P.; Hanus, M., Proceedings of the 13th International ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming (July 2011), ACM: ACM New York, NY, USA), 101-112
[54] Sabel, D.; Schmidt-Schauß, M., Conservative concurrency in Haskell, (Dershowitz, N., Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science (2012), IEEE), 561-570 · Zbl 1361.68049
[55] Sabel, D.; Schmidt-Schauß, M., A two-valued logic for properties of strict functional programs allowing partial functions, J. Automat. Reason., 50, 4, 383-421 (June 2013) · Zbl 1267.68088
[56] Sanjabi, S. B.; Ong, C.-H. L., Fully abstract semantics of additive aspects by translation, (Barry, B. M.; de Moor, O., Proceedings of the 6th International Conference on Aspect-Oriented Software Development (2007), ACM), 135-148
[57] Schmidt-Schauß, M.; Machkasova, E.; Sabel, D., Extending Abramsky’s lazy lambda calculus: (non)-conservativity of embeddings, (van Raamsdonk, F., 24th International Conference on Rewriting Techniques and Applications. 24th International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 21 (2013), Schloss Dagstuhl - Leibniz-Zentrum für Informatik: Schloss Dagstuhl - Leibniz-Zentrum für Informatik Dagstuhl, Germany), 239-254 · Zbl 1356.68037
[58] Schmidt-Schauß, M.; Machkasova, E.; Sabel, D., Extending Abramsky’s lazy lambda calculus: (non)-conservativity of embeddings (April 2013), Institut für Informatik, Fachbereich Informatik und Mathematik, Goethe-Universität Frankfurt am Main, Frank report 51 · Zbl 1356.68037
[59] Schmidt-Schauß, M.; Niehren, J.; Schwinghammer, J.; Sabel, D., Adequacy of compositional translations for observational semantics, (Fifth IFIP International Conference on Theoretical Computer Science. Fifth IFIP International Conference on Theoretical Computer Science, IFIP, vol. 273 (2008), Springer), 521-535
[60] Schmidt-Schauß, M.; Sabel, D., Closures of may-, should- and must-convergences for contextual equivalence, Inform. Process. Lett., 110, 6, 232-235 (2010) · Zbl 1209.68308
[61] Schmidt-Schauß, M.; Sabel, D., On generic context lemmas for higher-order calculi with sharing, Theoret. Comput. Sci., 411, 11-13, 1521-1541 (2010) · Zbl 1191.68165
[62] Schmidt-Schauß, M.; Sabel, D., Correctness of an STM Haskell implementation, (Morrisett, G.; Uustalu, T., Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (September 2013), ACM: ACM New York, NY, USA), 161-172 · Zbl 1323.68154
[63] Schmidt-Schauß, M.; Sabel, D.; Machkasova, E., Simulation in the call-by-need lambda-calculus with letrec, (Lynch, C., Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Proceedings of the 21st International Conference on Rewriting Techniques and Applications, LIPIcs, vol. 6 (2010), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 295-310 · Zbl 1236.68148
[64] Schmidt-Schauß, M.; Sabel, D.; Machkasova, E., Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq (July 2012), Institut für Informatik, Fachbereich Informatik und Mathematik, Goethe-Universität Frankfurt am Main, Frank report 49 · Zbl 1352.68123
[65] Schwinghammer, J.; Sabel, D.; Schmidt-Schauß, M.; Niehren, J., Correctly translating concurrency primitives, (Proceedings of the 2009 ACM SIGPLAN Workshop on ML (August 2009), ACM: ACM New York, NY, USA), 27-38
[66] Shapiro, E., Separating concurrent languages with categories of language embeddings, (Koutsougeras, C.; Vitter, J. S., Proceedings of the 23rd Annual ACM Symposium on Theory of Computing (1991), ACM), 198-208
[67] Sumii, E.; Pierce, B. C., A bisimulation for type abstraction and recursion, (Proceedings of the 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2005), ACM: ACM New York, NY, USA), 63-74 · Zbl 1369.68117
[68] Wand, M., Compiler correctness for parallel languages, (Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture (1995), ACM: ACM New York, NY, USA), 120-134
[69] Wells, J. B.; Plump, D.; Kamareddine, F., Diagrams for meaning preservation, (Nieuwenhuis, R., Proceedings of the 14th International Conference on Rewriting Techniques and Applications. Proceedings of the 14th International Conference on Rewriting Techniques and Applications, Lecture Notes in Comput. Sci., vol. 2706 (2003), Springer), 88-106 · Zbl 1038.68073
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.