Advertisement

Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance

  • Jieung Kim
  • Sukyoung Ryu
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)

Abstract

In object-oriented languages, overloaded methods with multiple dispatch extend the functionality of existing classes, and multiple inheritance allows a class to reuse code in multiple classes. However, both multiple dispatch and multiple inheritance introduce the possibility of ambiguous method calls that cannot be resolved at run time. To guarantee no ambiguous calls at run time, the overloaded method declarations should be checked statically.

In this paper, we present a core calculus for the Fortress programming language, which provides both multiple dispatch and multiple inheritance. While previous work proposed a set of static rules to guarantee no ambiguous calls at run time, the rules were parametric to the underlying programming language. To implement such rules for a particular language, the rules should be instantiated for the language. Therefore, to concretely realize the overloading rules for Fortress, we formally define a core calculus for Fortress and mechanize the calculus and its type safety proof in Coq.

Keywords

Coq Fortress overloading multiple dispatch multiple inheritance type system proof mechanization 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
  2. 2.
  3. 3.
    Allen, E., Chase, D., Hallett, J.J., Luchangco, V., Maessen, J.-W., Ryu, S., Steele Jr., G.L., Tobin-Hochstadt, S.: The Fortress Language Specification Version 1.0 (March 2008)Google Scholar
  4. 4.
    Allen, E., Hallett, J.J., Luchangco, V., Ryu, S., Steele Jr., G.L.: Modular Multiple Dispatch with Multiple Inheritance. In: Proceedings of the 2007 ACM Symposium on Applied Computing, New York, NY, USA, pp. 1117–1121. ACM (2007)Google Scholar
  5. 5.
    Allen, E., Hilburn, J., Kilpatrick, S., Ryu, S., Chase, D., Luchangco, V., Steele Jr., G.L.: Type-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance. In: Proceedings of the 26th ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications. ACM (2011)Google Scholar
  6. 6.
    Altherr, P., Cremet, V.: Adding Type Constructor Parameterization to Java. In: Formal Techniques for Java-like Programs (2007)Google Scholar
  7. 7.
    Bettini, L., Capecchi, S., Venneri, B.: Featherweight Java with Multi-methods. In: Proceedings of the 5th International Symposium on Principles and Practice of Programming in Java, New York, NY, USA, pp. 83–92. ACM (2007)Google Scholar
  8. 8.
    Bettini, L., Capecchi, S., Venneri, B.: Featherweight Java with Dynamic and Static Overloading. Science of Computer Programming 74, 261–278 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Bobrow, D.G., DiMichiel, L.G., Gabriel, R.P., Keene, S.E., Kiczales, G., Moon, D.A.: Common Lisp Object System Specification. ACM SIGPLAN Notices, 23 (September 1988)Google Scholar
  10. 10.
    Bonniot, D., Keller, B., Barber, F.: The Nice user’s manual (2003), http://nice.sourceforge.net/NiceManual.pdf
  11. 11.
    Bracha, G., Steele, G., Joy, B., Gosling, J.: Java\(^{\mbox{TM}}\) Language Specification, 3rd edn. Java Series. Addison-Wesley Professional (July 2005)Google Scholar
  12. 12.
    Castagna, G., Ghelli, G., Longo, G.: A Calculus for Overloaded Functions with Subtyping. SIGPLAN Lisp Pointers 1, 182–192 (1992)CrossRefzbMATHGoogle Scholar
  13. 13.
    Clifton, C., Leavens, G.T., Chambers, C., Millstein, T.: MultiJava: Modular Open Classes and Symmetric Multiple Dispatch for Java. In: Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, New York, NY, USA, pp. 130–145. ACM (2000)Google Scholar
  14. 14.
    The Coq Development Team. The Coq Proof Assistant, http://coq.inria.fr/
  15. 15.
    Cremet, V., Altherr, P.: FGJ-ω in Coq (2007), http://lamp.epfl.ch/~cremet/FGJ-omega
  16. 16.
    Delaware, B., Cook, W.R., Batory, D.: Fitting the Pieces Together: a Machine-checked Model of Safe Composition. In: Proceedings of the the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, ESEC/FSE 2009, New York, NY, USA, pp. 243–252. ACM (2009)Google Scholar
  17. 17.
    Dubois, C.: Proving ML Type Soundness within Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 126–144. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  18. 18.
    De Fraine, B., Ernst, E., Südholt, M.: Cast-Free Featherweight Java (2008), http://soft.vub.ac.be/~bdefrain/featherj
  19. 19.
    Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A Minimal Core Calculus for Java and GJ. In: Meissner, L. (ed.) Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Applications (OOPSLA 1999), vol. 34(10), pp. 132–146. NY (1999)Google Scholar
  20. 20.
  21. 21.
    Kim, J., Ryu, S.: FFMM: Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. Technical report, KAIST (June 2011)Google Scholar
  22. 22.
    Kim, J., Ryu, S.: Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness. Technical Report ROSAEC-2011-011, KAIST (May 2011)Google Scholar
  23. 23.
    Lievens, D., Harrison, W.: Symmetric Encapsulated Multi-methods to Abstract over Application Structure. In: Proceedings of the 2009 ACM Symposium on Applied Computing, New York, NY, USA, pp. 1873–1880. ACM (2009)Google Scholar
  24. 24.
    Millstein, T., Chambers, C.: Modular Statically Typed Multimethods. In: Information and Computation, pp. 279–303 (2002)Google Scholar
  25. 25.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press (1997)Google Scholar
  26. 26.
    Muschevici, R., Potanin, A., Tempero, E., Noble, J.: Multiple Dispatch in Practice. In: Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications, pp. 563–582. ACM (2008)Google Scholar
  27. 27.
    Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-Step Guide, 2nd edn. Artima Inc. (2011)Google Scholar
  28. 28.
    Schärli, N., Ducasse, S., Nierstrasz, O., Black, A.P.: Traits: Composable Units of Behaviour. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 248–274. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  29. 29.
    Stroustrup, B.: The C++ Programming Language. Addison-Wesley (1985)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Jieung Kim
    • 1
  • Sukyoung Ryu
    • 1
  1. 1.Computer Science DepartmentKAISTKorea

Personalised recommendations