{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,13]],"date-time":"2026-10-13T17:05:42Z","timestamp":1791911142743,"version":"4.3.4"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,5,10]],"date-time":"2024-05-10T00:00:00Z","timestamp":1715299200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Manag. Data"],"published-print":{"date-parts":[[2024,5,10]]},"abstract":"<jats:p>Relational data modeling can often be restrictive as it provides no direct facility for modeling polymorphic types, reified relations, multi-valued attributes, and other common high-level structures in data. This creates many challenges in data modeling and engineering tasks, and has led to the rise of more flexible NoSQL databases, such as graph and document databases. In the absence of structured schemas, however, we can neither express nor validate the intention of data models, making long-term maintenance of databases substantially more difficult. To resolve this dilemma, we argue that, parallel to the role of classical predicate logic for relational algebra, contemporary foundations of mathematics rooted in type theory can guide us in the development of powerful new high-level data models and query languages. To this end, we introduce a new polymorphic entity-relation-attribute (PERA) data model, grounded in type-theoretic principles and accessible through classical conceptual modeling, with a near-natural query language: TypeQL. We illustrate the syntax of TypeQL as well as its denotation in the PERA model, formalize our model as an algebraic theory with dependent types, and describe its stratified semantics.<\/jats:p>","DOI":"10.1145\/3651611","type":"journal-article","created":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T08:32:13Z","timestamp":1715675533000},"page":"1-27","source":"Crossref","is-referenced-by-count":2,"title":["TypeQL: A Type-Theoretic &amp; Polymorphic Query Language"],"prefix":"10.1145","volume":"2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1313-7386","authenticated-orcid":false,"given":"Christoph","family":"Dorn","sequence":"first","affiliation":[{"name":"TypeDB &amp; University of Oxford, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8502-9051","authenticated-orcid":false,"given":"Haikal","family":"Pribadi","sequence":"additional","affiliation":[{"name":"TypeDB, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"https:\/\/www.typedb.com","author":"DB.","year":"2023","unstructured":"2023. TypeDB. (2023). https:\/\/www.typedb.com"},{"key":"e_1_2_2_2_1","volume-title":"Foundations of databases","author":"Abiteboul S.","unstructured":"S. Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of databases. Addison-Wesley, Reading, Mass. http:\/\/webdam.inria.fr\/Alice\/"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0--934613--40--8.50006--3"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of the 1990 ACM SIGMOD International Conference on Management of Data","author":"Atkinson Malcolm P.","year":"1990","unstructured":"Malcolm P. Atkinson, Fran\u00e7ois Bancilhon, David J. DeWitt, Klaus R. Dittrich, David Maier, and Stanley B. Zdonik. 1990. The Object-Oriented Database System Manifesto. In Proceedings of the 1990 ACM SIGMOD International Conference on Management of Data, Atlantic City, NJ, USA, May 23--25, 1990, Hector Garcia-Molina and H. V. Jagadish (Eds.). ACM Press, 395."},{"key":"e_1_2_2_5_1","volume-title":"A Formal Presentation of MongoDB (Extended Version). CoRR abs\/1603.09291","author":"Botoeva Elena","year":"2016","unstructured":"Elena Botoeva, Diego Calvanese, Benjamin Cogrel, Martin Rezk, and Guohui Xiao. 2016. A Formal Presentation of MongoDB (Extended Version). CoRR abs\/1603.09291 (2016). arXiv:1603.09291 http:\/\/arxiv.org\/abs\/1603.09291"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053--9"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/320434.320440"},{"key":"e_1_2_2_8_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. http:\/\/mitpress.mit.edu\/books\/certified-programming-dependent-types"},{"key":"e_1_2_2_9_1","volume-title":"Cosette: An Automated Prover for SQL.","author":"Chu Shumo","year":"2017","unstructured":"Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017. Cosette: An Automated Prover for SQL. (2017). http:\/\/cidrdb.org\/cidr2017\/papers\/p51-chu-cidr17.pdf"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062348"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--1--4684--3384--5_11"},{"key":"e_1_2_2_12_1","volume-title":"Mellish","author":"Clocksin William F.","year":"1994","unstructured":"William F. Clocksin and Christopher S. Mellish. 1994. Programming in Prolog (4. ed.). Springer."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/362384.362685"},{"key":"e_1_2_2_14_1","volume-title":"Prakash Panangaden, James T. Sasaki, and Scott F. Smith.","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing mathematics with the Nuprl proof development system. Prentice Hall. http:\/\/dl.acm.org\/citation.cfm?id=10510"},{"key":"e_1_2_2_15_1","volume-title":"Automated Deduction - CADE-25, Amy P","author":"de Moura Leonardo","unstructured":"Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham, 378--388."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3583780.3615999"},{"key":"e_1_2_2_17_1","volume-title":"Formal Semantics of the Type-Theoretic Language TypeQL. In preparation","author":"Dorn Christoph","year":"2024","unstructured":"Christoph Dorn and Haikal Pribadi. 2024. Formal Semantics of the Type-Theoretic Language TypeQL. In preparation (2024)."},{"key":"e_1_2_2_18_1","volume-title":"Fundamentals of Database Systems","author":"Elmasri R","unstructured":"R Elmasri and SB Navathe. 2016. Fundamentals of Database Systems. Pearson, Boston."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0--387--39940--9"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exaa009"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3183713.3190657"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(93)90024-Q"},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the 6th National Conference on Artificial Intelligence","author":"Gelfond Michael","year":"1987","unstructured":"Michael Gelfond. 1987. On Stratified Autoepistemic Theories. In Proceedings of the 6th National Conference on Artificial Intelligence. Seattle, WA, USA, July 1987, Kenneth D. Forbus and Howard E. Shrobe (Eds.). Morgan Kaufmann, 207--211. http:\/\/www.aaai.org\/Library\/AAAI\/1987\/aaai87-037.php"},{"key":"e_1_2_2_24_1","volume-title":"Logic Programming, Proceedings of the Fifth International Conference and Symposium","author":"Gelfond Michael","year":"1988","unstructured":"Michael Gelfond and Vladimir Lifschitz. 1988. The Stable Model Semantics for Logic Programming. In Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, August 15--19, 1988 (2 Volumes), Robert A. Kowalski and Kenneth A. Bowen (Eds.). MIT Press, 1070--1080."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037169"},{"key":"e_1_2_2_26_1","volume-title":"Proofs and types","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. Vol. 7. Cambridge university press Cambridge."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/111197.111200"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.14778\/3151113.3151116"},{"key":"e_1_2_2_29_1","volume-title":"Practical Foundations for Programming Languages (2nd. Ed.)","author":"Harper Robert","unstructured":"Robert Harper. 2016. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press. https:\/\/www.cs.cmu.edu\/%7Erwh\/pfpl\/index.html"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1989323.1989456"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/DBKDA.2009.11"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/BigData.2014.7004486"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--76530--8_11"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/69.60796"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2000.10067"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/311531.311533"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--96826--6"},{"key":"e_1_2_2_38_1","unstructured":"Mary E. S. Loomis and Akmal B. Chaudhri (Eds.). 1997. Object Databases in Practice. Prentice-Hall."},{"key":"e_1_2_2_39_1","volume-title":"Intuitionistic type theory. Studies in proof theory","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Studies in proof theory, Vol. 1. Bibliopolis, Naples."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","unstructured":"Atsushi Ohori Peter Buneman and Val Tannen. 1989. Database Programming in Machiavelli - a Polymorphic Language with Static Type Inference. (1989) 46--57. https:\/\/doi.org\/10.1145\/67544.66931","DOI":"10.1145\/67544.66931"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.2481\/DSJ.GRDI-004"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/1131.003.0016"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/62061.62062"},{"key":"e_1_2_2_44_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce. 2002. Types and programming languages. MIT Press."},{"key":"e_1_2_2_45_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. (2013). https:\/\/homotopytypetheory.org\/book\/"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","unstructured":"Teodor C. Przymusinski. 1988. On the Declarative Semantics of Deductive Databases and Logic Programs. In Foundations of Deductive Databases and Logic Programming Jack Minker (Ed.). Morgan Kaufmann 193--216. https: \/\/doi.org\/10.1016\/B978-0--934613--40--8.50009--9","DOI":"10.1016\/B978-0--934613--40--8.50009--9"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1567274.1567278"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743--1066(94)00039--9"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815072.2815073"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796817000168"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10515-022-00336-Y"},{"key":"e_1_2_2_53_1","volume-title":"Practical Foundations of Mathematics","author":"Taylor Paul","unstructured":"Paul Taylor. 1999. Practical Foundations of Mathematics. Cambridge studies in advanced mathematics, Vol. 59. Cambridge University Press."},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","unstructured":"Bernhard Thalheim. 2018. Extended Entity-Relationship Model. (2018). https:\/\/doi.org\/10.1007\/978--1--4614--8265--9_157","DOI":"10.1007\/978--1--4614--8265--9_157"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699407"}],"container-title":["Proceedings of the ACM on Management of Data"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651611","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651611","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T21:39:59Z","timestamp":1755898799000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651611"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,10]]},"references-count":55,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,5,10]]}},"alternative-id":["10.1145\/3651611"],"URL":"https:\/\/doi.org\/10.1145\/3651611","relation":{},"ISSN":["2836-6573"],"issn-type":[{"value":"2836-6573","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,10]]}}}