{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:49Z","timestamp":1771888189785,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642357855","type":"print"},{"value":"9783642357862","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35786-2_11","type":"book-chapter","created":{"date-parts":[[2013,1,5]],"date-time":"2013-01-05T13:04:45Z","timestamp":1357391085000},"page":"135-152","source":"Crossref","is-referenced-by-count":7,"title":["Modeling Ontological Structures with Type Classes in Coq"],"prefix":"10.1007","author":[{"given":"Richard","family":"Dapoigny","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Patrick","family":"Barlatier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"11_CR1","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1016\/j.jvlc.2004.11.001","volume":"16","author":"I. Alia","year":"2005","unstructured":"Alia, I., Abdelmoty, A.I., Smart, P.D., Jones, C.B., Fu, G., Finch, D.: A critical evaluation of ontology languages for geographic information retrieval on the Internet. Journal of Visual Languages & Computing\u00a016(4), 331\u2013358 (2005)","journal-title":"Journal of Visual Languages & Computing"},{"key":"11_CR2","doi-asserted-by":"crossref","first-page":"311","DOI":"10.3233\/AO-2012-0113","volume":"73","author":"P. Barlatier","year":"2012","unstructured":"Barlatier, P., Dapoigny, R.: A Type-Theoretical Approach for Ontologies: the Case of Roles. Applied Ontology\u00a073, 311\u2013356 (in press, 2012)","journal-title":"Applied Ontology"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS series. Springer (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/j.artmed.2006.12.003","volume":"39","author":"O. Bodenreider","year":"2007","unstructured":"Bodenreider, O., Smith, B., Kumar, A., Burgun, A.: Investigating subsumption in SNOMED CT: An exploration into large description logic-based biomedical terminologies. Artificial Intelligence in Medicine\u00a039, 183\u2013195 (2007)","journal-title":"Artificial Intelligence in Medicine"},{"key":"11_CR5","volume-title":"Object-Oriented Design with Applications","author":"G. Booch","year":"1991","unstructured":"Booch, G.: Object-Oriented Design with Applications. Benjamin Cummings, Redwood City (1991)"},{"key":"11_CR6","unstructured":"Bourbaki, N.: Univers, S\u00e9minaire de G\u00e9om\u00e9trie Alg\u00e9brique du Bois Marie Th\u00e9orie des topos et cohomologie \u00e9tale des sch\u00e9mas (SGA 4), 1. Lecture notes in mathematics, vol. 269, pp. 185\u2013217. Springer (1972)"},{"key":"11_CR7","unstructured":"Chein, M., Mugnier, M.L., Simonet, G.: Nested graphs: a graph-based knowledge representation model with FOL semantics. In: Procs. of KR 1998, pp. 524\u2013534. Morgan Kaufmann (1998)"},{"key":"11_CR8","unstructured":"Cirstea, H., Coquery, E., Drabent, W., Fages, F., Kirchner, C., Maluszynski, J., Wack, B.: Types for Web Rule Languages: a preliminary study. Technical report A04-R-560, PROTHEO - INRIA Lorraine - LORIA (2004)"},{"issue":"2-3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Information and Computation\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"11_CR10","unstructured":"Coq Development Team, The Coq Reference Manual, Version 8.3., INRIA, France (2010)"},{"key":"11_CR11","unstructured":"Dapoigny, R., Barlatier, P.: Towards Ontological Correctness of Part-whole Relations with Dependent Types. In: Procs. of the Sixth Int. Conference (FOIS 2010), pp. 45\u201358 (2010a)"},{"issue":"4","key":"11_CR12","doi-asserted-by":"crossref","first-page":"293","DOI":"10.3233\/FI-2010-351","volume":"104","author":"R. Dapoigny","year":"2010","unstructured":"Dapoigny, R., Barlatier, P.: Modeling Contexts with Dependent Types. Fundamenta Informaticae\u00a0104(4), 293\u2013327 (2010b)","journal-title":"Fundamenta Informaticae"},{"key":"11_CR13","unstructured":"Eiter, T., Lukasiewicz, T., Schindlauer, R., Tompits, H.: Combining answer set programming with description logics for the semantic web. In: Proc. of Ninth Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR 2004), pp. 141\u2013151. AAAI Press (2004)"},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31175-8_1","volume-title":"Controlled Natural Language","author":"K. Angelov","year":"2012","unstructured":"Angelov, K., Enache, R.: Typeful Ontologies with Direct Multilingual Verbalization. In: Rosner, M., Fuchs, N.E. (eds.) CNL 2010. LNCS, vol.\u00a07175, pp. 1\u201320. Springer, Heidelberg (2012)"},{"key":"11_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45810-7_18","volume-title":"Knowledge Engineering and Knowledge Management. Ontologies and the Semantic Web","author":"A. Gangemi","year":"2002","unstructured":"Gangemi, A., Guarino, N., Masolo, C., Oltramari, A., Schneider, L.: Sweetening Ontologies with DOLCE. In: G\u00f3mez-P\u00e9rez, A., Benjamins, V.R. (eds.) EKAW 2002. LNCS (LNAI), vol.\u00a02473, pp. 166\u2013181. Springer, Heidelberg (2002)"},{"key":"11_CR16","unstructured":"Guarino, N.: The Ontological Level. In: Casati, R., Smith, B., White, G. (eds.) Philosophy and the Cognitive Science, pp. 443\u2013456. Holder-Pivhler-Tempsky (1994)"},{"key":"11_CR17","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-540-24750-0_8","volume-title":"Handbook on Ontologies","author":"Nicola Guarino","year":"2004","unstructured":"Guarino, N., Welty, C.: An Overview of OntoClean. In: Handbook on Ontologies, pp. 151\u2013172 (2004)"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-642-02463-4_4","volume-title":"Conceptual Modeling: Foundations and Applications","author":"N. Guarino","year":"2009","unstructured":"Guarino, N.: The Ontological Level: Revisiting 30 Years of Knowledge Representation. In: Borgida, A.T., Chaudhri, V.K., Giorgini, P., Yu, E.S. (eds.) Conceptual Modeling: Foundations and Applications. LNCS, vol.\u00a05600, pp. 52\u201367. Springer, Heidelberg (2009)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/3-540-45816-6_15","volume-title":"Conceptual Modeling - ER 2002","author":"G. Guizzardi","year":"2002","unstructured":"Guizzardi, G., Herre, H., Wagner, G.: On the General Ontological Foundations of Conceptual Modeling. In: Spaccapietra, S., March, S.T., Kambayashi, Y. (eds.) ER 2002. LNCS, vol.\u00a02503, pp. 65\u201378. Springer, Heidelberg (2002)"},{"key":"11_CR20","unstructured":"Guizzardi, G.: Ontological Foundations for Structural Conceptual Models. University of Twente (Centre for Telematics and Information Technology) (2005)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/11901181_10","volume-title":"Conceptual Modeling - ER 2006","author":"G. Guizzardi","year":"2006","unstructured":"Guizzardi, G., Masolo, C., Borgo, S.: In Defense of a Trope-Based Ontology for Conceptual Modeling: An Example with the Foundations of Attributes, Weak Entities and Datatypes. In: Embley, D.W., Oliv\u00e9, A., Ram, S. (eds.) ER 2006. LNCS, vol.\u00a04215, pp. 112\u2013125. Springer, Heidelberg (2006)"},{"key":"11_CR22","unstructured":"Howard, W.A.: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. The formulae-as-types notion of construction, pp. 479\u2013490. Academic Press (1980)"},{"key":"11_CR23","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/10722280_37","volume-title":"Conceptual Structures: Logical, Linguistic, and Computational Issues","author":"A. Kabbaj","year":"2000","unstructured":"Kabbaj, A., Janta-Polczynski, M.: From PROLOG+\u2009+ to PROLOG+CG: A CG Object-Oriented Logic Programming Language, B. In: Ganter, B., Mineau, G.W. (eds.) ICCS 2000. LNCS (LNAI), vol.\u00a01867, pp. 540\u2013554. Springer, Heidelberg (2000)"},{"key":"11_CR24","unstructured":"Kaneiwa, K., Mizoguchi, R.: Ontological Knowledge Base Reasoning with Sort-Hierarchy and Rigidity. In: Procs. of KR 2004, pp. 278\u2013288. AAAI Press (2004)"},{"issue":"1-2","key":"11_CR25","doi-asserted-by":"crossref","first-page":"91","DOI":"10.3233\/AO-2008-0044","volume":"3","author":"C.M. Keet","year":"2008","unstructured":"Keet, C.M., Artale, A.: Representing and reasoning over a taxonomy of part-whole relations. Applied Ontology\u00a03(1-2), 91\u2013110 (2008)","journal-title":"Applied Ontology"},{"key":"11_CR26","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1145\/210332.210335","volume":"42","author":"M. Kifer","year":"1995","unstructured":"Kifer, M., Lausen, G., Wu, J.: Logical foundations of object-oriented and frame-based languages. Journal of the ACM\u00a042, 741\u2013843 (1995)","journal-title":"Journal of the ACM"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Kr\u00f6tzsch, M., et al.: How to reason with OWL in a logic programming system. In: Procs. of RuleML 2006 (2006)","DOI":"10.1109\/RULEML.2006.14"},{"issue":"1","key":"11_CR28","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. Journal of Logic and Computation\u00a09(1), 105\u2013130 (1999)","journal-title":"Journal of Logic and Computation"},{"key":"11_CR29","unstructured":"Masolo, C., Borgo, S., Gangemi, A., Guarino, N., Oltramari, A.: Ontology Library (D18). Laboratory for Applied Ontology-ISTC-CNR (2003)"},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"McKinna, J.: Why dependent types matter. In: Procs. of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, vol.\u00a041(1), p. 1 (2006)","DOI":"10.1145\/1111320.1111038"},{"issue":"3","key":"11_CR31","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1016\/j.datak.2006.03.008","volume":"60","author":"M.L. Mugnier","year":"2007","unstructured":"Mugnier, M.L., Lecl\u00e8re, M.: On querying simple conceptual graphs with negation. Data & Knowledge engineering\u00a060(3), 468\u2013493 (2007)","journal-title":"Data & Knowledge engineering"},{"issue":"4","key":"11_CR32","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/102675.102676","volume":"8","author":"J. Mylopoulos","year":"1990","unstructured":"Mylopoulos, J., Borgida, A., Jarke, M., Koubarakis, M.: Telos: Representing Knowledge About Information Systems. ACM Trans. on Information Systems\u00a08(4), 325\u2013362 (1990)","journal-title":"ACM Trans. on Information Systems"},{"key":"11_CR33","unstructured":"Napoli, A.: Subsumption and classification-based reasoning in object-based representations. In: Procs. of the 10th European Conference on Artificial Intelligence (ECAI 1992), pp. 425\u2013429. John Wiley & Sons Ltd. (1992)"},{"key":"11_CR34","unstructured":"Noonan, H.: Identity. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy (2011), http:\/\/plato.stanford.edu\/archives\/win2011\/entries\/identity\/"},{"key":"11_CR35","unstructured":"Pires, L.F., van Sinderen, M., Munthe-Kaas, E., Prokaev, S.M.H., Plas, D.J.: Techniques for describing and manipulating context information, Freeband\/A MUSE D3.5v2.0, Lucent Technologies (2005)"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive Definitions in the System Coq - Rules and Properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664, pp. 328\u2013345. Springer, Heidelberg (1993)"},{"key":"11_CR37","unstructured":"Rosati, R.: DL+log: Tight integration of description logics and disjunctive datalog. In: Proc. of Tenth Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006), pp. 68\u201378. AAAI Press (2006)"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Saibi, A.: Typing algorithm in type theory with inheritance. In: Procs. of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997), pp. 292\u2013301. ACM Press (1997)","DOI":"10.1145\/263699.263742"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Setzer, A.: Object-Oriented Programming in Dependent Type Theory. In: Trends in Functional Programming, Intellect, vol.\u00a07, pp. 91\u2013108 (2007)","DOI":"10.2307\/j.ctv36xvknz.9"},{"key":"11_CR40","volume-title":"MEDINFO 2004","author":"B. Smith","year":"2004","unstructured":"Smith, B., Rosse, C.: The Role of Foundational Relations in the Alignment of Biomedical Ontologies. In: Fieschi, M., et al. (eds.) MEDINFO 2004. IOS Press, Amsterdam (2004)"},{"key":"11_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-Class Type Classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"11_CR42","unstructured":"Sowa, J.F.: Using a lexicon of canonical graphs in a semantic interpreter. Relational models of the lexicon, pp. 113\u2013137. Cambridge University Press (1988)"},{"key":"11_CR43","volume-title":"Knowledge Representation: Logical, Philosophical, and Computational Foundations","author":"J.F. Sowa","year":"2000","unstructured":"Sowa, J.F.: Knowledge Representation: Logical, Philosophical, and Computational Foundations. Brooks Cole Publishing Co., Pacific Grove (2000)"},{"key":"11_CR44","doi-asserted-by":"crossref","unstructured":"Sowa, J.F.: Conceptual Graphs. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation,\u00a0ch. 5, pp. 213\u2013237. Elsevier (2008)","DOI":"10.1016\/S1574-6526(07)03005-2"},{"issue":"4","key":"11_CR45","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science\u00a021(4), 795\u2013825 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"key":"11_CR46","doi-asserted-by":"crossref","unstructured":"Werner, B.: On the strength of proof-irrelevant type theories. Logical Methods in Computer Science 4(3) (2008)","DOI":"10.2168\/LMCS-4(3:13)2008"},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"Woods, W.A.: Understanding Subsumption and Taxonomy: a Framework for progress. In: Sowa, J. (ed.) Principles of Semantic Networks, pp. 45\u201394. Morgan Kaufmann (1991)","DOI":"10.1016\/B978-1-4832-0771-1.50007-2"}],"container-title":["Lecture Notes in Computer Science","Conceptual Structures for STEM Research and Education"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35786-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,28]],"date-time":"2023-06-28T12:59:53Z","timestamp":1687957193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35786-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642357855","9783642357862"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35786-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}