{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T23:38:45Z","timestamp":1743032325705,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642253782"},{"type":"electronic","value":"9783642253799"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-25379-9_20","type":"book-chapter","created":{"date-parts":[[2011,11,13]],"date-time":"2011-11-13T20:33:47Z","timestamp":1321216427000},"page":"264-279","source":"Crossref","is-referenced-by-count":4,"title":["Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance"],"prefix":"10.1007","author":[{"given":"Jieung","family":"Kim","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sukyoung","family":"Ryu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Dylan, http:\/\/www.opendylan.org\/"},{"key":"20_CR2","unstructured":"Metatheory Library: Atom, http:\/\/www.cis.upenn.edu\/~plclub\/popl08-tutorial\/code\/coqdoc\/Atom.html"},{"key":"20_CR3","unstructured":"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)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"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\u20131121. ACM (2007)","DOI":"10.1145\/1244002.1244245"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/2048066.2048140"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Altherr, P., Cremet, V.: Adding Type Constructor Parameterization to Java. In: Formal Techniques for Java-like Programs (2007)","DOI":"10.5381\/jot.2008.7.5.a2"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"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\u201392. ACM (2007)","DOI":"10.1145\/1294325.1294337"},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/j.scico.2009.01.007","volume":"74","author":"L. Bettini","year":"2009","unstructured":"Bettini, L., Capecchi, S., Venneri, B.: Featherweight Java with Dynamic and Static Overloading. Science of Computer Programming\u00a074, 261\u2013278 (2009)","journal-title":"Science of Computer Programming"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.1145\/885631.885632"},{"key":"20_CR10","unstructured":"Bonniot, D., Keller, B., Barber, F.: The Nice user\u2019s manual (2003), http:\/\/nice.sourceforge.net\/NiceManual.pdf"},{"key":"20_CR11","unstructured":"Bracha, G., Steele, G., Joy, B., Gosling, J.: Java $^{\\mbox{TM}}$ Language Specification, 3rd edn. Java Series. Addison-Wesley Professional (July 2005)"},{"key":"20_CR12","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1145\/141478.141537","volume":"1","author":"G. Castagna","year":"1992","unstructured":"Castagna, G., Ghelli, G., Longo, G.: A Calculus for Overloaded Functions with Subtyping. SIGPLAN Lisp Pointers\u00a01, 182\u2013192 (1992)","journal-title":"SIGPLAN Lisp Pointers"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013145. ACM (2000)","DOI":"10.1145\/353171.353181"},{"key":"20_CR14","unstructured":"The Coq Development\u00a0Team. The Coq Proof Assistant, http:\/\/coq.inria.fr\/"},{"key":"20_CR15","unstructured":"Cremet, V., Altherr, P.: FGJ-\u03c9 in Coq (2007), http:\/\/lamp.epfl.ch\/~cremet\/FGJ-omega"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"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\u2013252. ACM (2009)","DOI":"10.1145\/1595696.1595733"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-44659-1_9","volume-title":"Theorem Proving in Higher Order Logics","author":"C. Dubois","year":"2000","unstructured":"Dubois, C.: Proving ML Type Soundness within Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 126\u2013144. Springer, Heidelberg (2000)"},{"key":"20_CR18","unstructured":"De Fraine, B., Ernst, E., S\u00fcdholt, M.: Cast-Free Featherweight Java (2008), http:\/\/soft.vub.ac.be\/~bdefrain\/featherj"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"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.\u00a034(10), pp. 132\u2013146. NY (1999)","DOI":"10.1145\/320385.320395"},{"key":"20_CR20","unstructured":"Kim, J.: FFMM in Coq (2011), http:\/\/plrg.kaist.ac.kr\/_media\/research\/software\/ffmm_in_coq.tar.gz"},{"key":"20_CR21","doi-asserted-by":"crossref","unstructured":"Kim, J., Ryu, S.: FFMM: Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. Technical report, KAIST (June 2011)","DOI":"10.1007\/978-3-642-25379-9_20"},{"key":"20_CR22","unstructured":"Kim, J., Ryu, S.: Coq Mechanization of Featherweight Basic Core Fortress for Type Soundness. Technical Report ROSAEC-2011-011, KAIST (May 2011)"},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"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\u20131880. ACM (2009)","DOI":"10.1145\/1529282.1529702"},{"key":"20_CR24","doi-asserted-by":"crossref","unstructured":"Millstein, T., Chambers, C.: Modular Statically Typed Multimethods. In: Information and Computation, pp. 279\u2013303 (2002)","DOI":"10.1006\/inco.2002.3103"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press (1997)","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"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\u2013582. ACM (2008)","DOI":"10.1145\/1449764.1449808"},{"key":"20_CR27","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-Step Guide, 2nd edn. Artima Inc. (2011)"},{"key":"20_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-540-45070-2_12","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"N. Sch\u00e4rli","year":"2003","unstructured":"Sch\u00e4rli, N., Ducasse, S., Nierstrasz, O., Black, A.P.: Traits: Composable Units of Behaviour. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, pp. 248\u2013274. Springer, Heidelberg (2003)"},{"key":"20_CR29","unstructured":"Stroustrup, B.: The C++ Programming Language. Addison-Wesley (1985)"}],"container-title":["Lecture Notes in Computer Science","Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-25379-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,19]],"date-time":"2019-06-19T09:39:23Z","timestamp":1560937163000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-25379-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642253782","9783642253799"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-25379-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}