Big-step Operational Semantics Revisited

• Autorzy: Dominik J. , Kuśmierek M. , Bono V.
• Języki publikacji: EN

Abstrakty

EN

In this paper we present a novel approach to big-step operational semantics. This approach stems from the observation that the typical type soundness property formulated via a big-step operational semantics is weak, while the option of using a small-step operational semantics is not always an option, because it is less intuitive to build and understand. We support our claim by using a simple language called LM, for which we present a big-step semantics expressed with the new approach, allowing one to formulate a stronger type soundness property. We prove this property for LM and we present an example of an error in the typing rules which does not violate the typical type soundness property, but does violate ours.

Słowa kluczowe

EN

big-step operational semantics; LM language; operational semantics; typing rules

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 103, nr 1-4
• Strony: 137--172
• Opis fizyczny: Bibliogr. 13 poz.

Twórcy

autor

Dominik J.

autor

Kuśmierek M.

autor

Bono V.

• Institute of Informatics, Warsaw University, Banacha 2, 02-097 Warszawa, Poland,

Bibliografia

• [1] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag New York, Inc., NJ, USA, 1996.
• [2] M. S. Ager. From natural semantics to abstract machines. In Logic Based Program Synthesis and Transformation, volume 3573 of LNCS, pages 245-261. Springer-Verlag, 2005.
• [3] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini, and P. Giannini. More dynamic object reclassification: FickleII . ACM Transactions on Programming Languages and Systems (TOPLAS), 24(2):153-191, 2002.
• [4] K. Fisher, F. Honsell, and J. C. Mitchell. A lambda-calculus of objects and method specialization. Nordic J. of Computing, 1(1):3-37, 1994. Preliminary version appeared in Proc. LICS '93, pp. 26-38.
• [5] M. Flatt, S. Krishnamurthi, and M. Felleisen. Classes and Mixins. In Proc. POPL '98, pages 171-183. ACM, 1998.
• [6] C. A. Gunter and D. Rémy. A Proof-Theoretic Assesment of Runtime Type Errors. AT&T Bell Laboratories Technical Memo 11261-921230-43TM, 1993.
• [7] H. Ibraheem and D. A. Schmidt. Adapting big-step semantics to small-step style: Coinductive interpretations and "higher-order" derivations. In Second Workshop on Higher-Order Techniques in Operational Semantics (HOOTS2). Elsevier, 1997.
• [8] G. Kahn. Natural semantics. In STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings, volume 247 of LNCS, pages 22-39. Springer-Verlag, 1987.
• [9] J. Kuśmierek. A Mixin Based Object-Oriented Calculus: True Modularity in Object-Oriented Programming. PhD thesis, Warsaw University, Departmanet of Informatics, 2010.
• [10] X. Leroy and H. Grall. Coinductive big-step operational semantics. CoRR, abs/0808.0586, 2008.
• [11] R. Milner, M. Tofte, and D. Macqueen. The Definition of Standard ML. MIT Press, Cambridge, MA, USA, 1997.
• [12] G. D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, University of Aarhus, University of Aarhus, 1981.
• [13] A. Stoughton. An operational semantics framework supporting the incremental construction of derivation trees. Electr. Notes Theor. Comput. Sci., 10, 1997.