Abstract
It is well known that big-step operational semantics are not suitable for proving soundness of type systems, because of their inability to distinguish stuck from non-terminating computations. We show how this problem can be solved by interpreting coinductively the rules for the standard big-step operational semantics of a Java-like language, thus making the claim of soundness more intuitive: whenever a program is well-typed, its coinductive operational semantics returns a value.
Indeed, coinduction allows non-terminating computations to return values; this is proved by showing that the set of proof trees defining the semantic judgment forms a complete metric space when equipped with a proper distance function.
In this way, we are able to prove soundness of a nominal type system w.r.t. the coinductive semantics. Since the coinductive semantics is sound w.r.t. the usual small-step operational semantics, the standard claim of soundness can be easily deduced.
This work has been partially supported by MIUR DISCO - Distribution, Interaction, Specification, Composition for Object Systems. I would like to thank Erik Ernst for his useful comments and suggestions; many thanks also to Sophia Drossopoulou, Atsushi Igarashi, Alan Mycroft and Elena Zucca for all their useful suggestions and questions.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ager, M.S.: From Natural Semantics to Abstract Machines. In: Etalle, S. (ed.) LOPSTR 2004. LNCS, vol. 3573, pp. 245–261. Springer, Heidelberg (2005)
Amadio, R., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Ancona, D.: Coinductive big-step operational semantics for type soundness of Java-like languages. In: Formal Techniques for Java-like Programs (FTfJP 2011), pp. 5:1–5:6. ACM (2011)
Ancona, D., Corradi, A., Lagorio, G., Damiani, F.: Abstract Compilation of Object-Oriented Languages into Coinductive CLP(X): Can Type Inference Meet Verification? In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 31–45. Springer, Heidelberg (2011)
Ancona, D., Lagorio, G.: Coinductive Type Systems for Object-Oriented Languages. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 2–26. Springer, Heidelberg (2009)
Ancona, D., Lagorio, G.: Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas. In: Montanari, A., Napoli, M., Parente, M. (eds.) Proceedings of GandALF 2010. Electronic Proceedings in Theoretical Computer Science, vol. 25, pp. 214–223 (2010)
Ancona, D., Lagorio, G.: Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theoretical Informatics and Applications 45(1), 3–33 (2011)
Arnold, A., Nivat, M.: The metric space of infinite trees. Algebraic and topological properties. Fundamenta Informaticae 3, 445–476 (1980)
Courcelle, B.: Fundamental properties of infinite trees. Theoretical Computer Science 25, 95–169 (1983)
Ernst, E., Ostermann, K., Cook, W.R.: A virtual class calculus. In: POPL, pp. 270–282 (2006)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Transactions on Programming Languages and Systems 23(3), 396–450 (2001)
Kusmierek, J.D.M., Bono, V.: Big-step operational semantics revisited. Fundam. Inform. 103(1-4), 137–172 (2010)
Leroy, X., Grall, H.: Coinductive big-step operational semantics. Information and Computation 207, 284–304 (2009)
Tofte, M., Milner, R.: Co-induction in relational semantics. Theoretical Computer Science 87(1), 209–220 (1990)
Nakata, K., Uustalu, T.: Trace-Based Coinductive Operational Semantics for While. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 375–390. Springer, Heidelberg (2009)
Nakata, K., Uustalu, T.: A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 488–506. Springer, Heidelberg (2010)
Simon, L., Mallya, A., Bansal, A., Gupta, G.: Coinductive Logic Programming. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 330–345. Springer, Heidelberg (2006)
Stoughton, A.: An operational semantics framework supporting the incremental construction of derivation trees. Electr. Notes Theor. Comput. Sci. 10 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ancona, D. (2012). Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics. In: Noble, J. (eds) ECOOP 2012 – Object-Oriented Programming. ECOOP 2012. Lecture Notes in Computer Science, vol 7313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31057-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-31057-7_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31056-0
Online ISBN: 978-3-642-31057-7
eBook Packages: Computer ScienceComputer Science (R0)