{"entities":{"Q2981954":{"pageid":2992679,"ns":120,"title":"Item:Q2981954","lastrevid":52799318,"modified":"2026-01-23T13:01:22Z","type":"item","id":"Q2981954","labels":{"en":{"language":"en","value":"A unification algorithm for Coq featuring universe polymorphism and overloading"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6713866"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$3C0BCBA2-DB40-4908-A562-C3E22F3FE770","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5669cdfdda0a813555a2e468008ed870c36163ff","datavalue":{"value":{"text":"A unification algorithm for Coq featuring universe polymorphism and overloading","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2981954$AB914EEC-A62E-41F8-8F29-23F03F49AC11","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4a11017294dd9971f5085bdacd6e2d2285b21576","datavalue":{"value":"1360.68774","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$54BC8EB5-5991-4189-AB36-9F78D90DB611","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"df93a0c4cfdaaef340fe0bdbd091c5d66cfeb438","datavalue":{"value":"10.1145/2784731.2784751","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$52D51950-D72B-494E-A33B-E005EB655D5B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"03755d4aabc7831f3051426847269a4a588f5547","datavalue":{"value":{"entity-type":"item","numeric-id":777872,"id":"Q777872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$84FB4981-2962-4034-AC47-58EDFAC8A9AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9414558f268ee594724569b856f23c96f190f01","datavalue":{"value":{"entity-type":"item","numeric-id":1791139,"id":"Q1791139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$CC4E0832-9C23-45E6-8665-452DB25D76D9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"958b9d2649c5f166ed12d91711a9f2d3feb923ea","datavalue":{"value":{"entity-type":"item","numeric-id":2945523,"id":"Q2945523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$91EC0C90-C29B-45B0-9453-3663DD222F41","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"81927d6a17a89da4e5bba03bf491f09d50a9b6e5","datavalue":{"value":{"time":"+2017-05-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2981954$3D385DC4-55DE-47A3-90FC-1068D8FA199D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$C92392E3-5683-447C-A462-BC83B5854F8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$B5732DCB-C8D5-4A66-AACB-FBF2D4D4CFAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a0dc380a7a6964f00e6560e4112710836960e832","datavalue":{"value":"68T20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$51635801-F60A-46FB-BAC6-E0515A6BFFD3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e1b9257f757b6f0f6d09dfe4c68e96948bd37dd1","datavalue":{"value":"6713866","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$F427F444-A4EE-4A2B-95DC-A4497E184345","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2981954$99E0BC8D-02A9-46B8-A1C7-D8FA08C62C71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2981954$818A6FC8-0E1D-4F0E-85C3-39482E6C027E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec44778685040bd9bd5cbc0ffb12f352e97e79b2","datavalue":{"value":"overloading","type":"string"},"datatype":"string"},"type":"statement","id":"Q2981954$12FA389B-014E-43AC-BAF8-DBB28F8CE82E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3922eb0b8235fb2b824bcb3eaa0c8d395dbd512","datavalue":{"value":"unification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2981954$6F38A338-6AE9-48EE-B329-588C6758AF7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1159aa73cd8daf4c43043be733617a1e49169dd","datavalue":{"value":"universe polymorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q2981954$79E1A37F-A08D-49ED-95FF-F2303273EB0F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$E1112F67-8068-49DA-9AC7-B9774C0EC978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$27A84AC9-4FC9-463C-B438-191E5C25D87E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4f20857e79be9881c5d7a06583454f1cf2611e9","datavalue":{"value":{"entity-type":"item","numeric-id":24994,"id":"Q24994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$5BEB87AA-BE5E-4DCC-A530-CB274A1B18C9","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2981954$5E9E4E40-0F64-41EA-998B-9D4E7324A9C9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6c792282d89fab575a5ace0f76af827c32865eaf","datavalue":{"value":"https://doi.org/10.1145/2784731.2784751","type":"string"},"datatype":"url"},"type":"statement","id":"Q2981954$65D88AA4-939C-46D5-95AA-11F082B3FA77","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b2ed7144ee82dea225c9dc1080096a10bb712ae6","datavalue":{"value":"W2013202135","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2981954$9AA95881-1B65-4935-9F50-C4020758F6A3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ba3c3d8d6173d7eb904fc0277f9be0c8d3d4b76","datavalue":{"value":{"entity-type":"item","numeric-id":5372007,"id":"Q5372007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"794e7293c40b15bb10c163d0d070664823ee6c36","datavalue":{"value":{"amount":"+0.9514416456222534","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2981954$C29416A0-82EF-482E-AA43-2E3D22898A10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad75dd62ec10db61a132203b18a115cc71365c0f","datavalue":{"value":{"entity-type":"item","numeric-id":2798047,"id":"Q2798047"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c2e7a42933f4f9537fecacfea3c63a12897905f","datavalue":{"value":{"amount":"+0.7909574508666992","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2981954$F97D679E-A7E6-4CDA-8249-E50B8A207251","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec2f0bb38b56f759cbb69a7dc3cbce032e16f8c6","datavalue":{"value":{"entity-type":"item","numeric-id":5055716,"id":"Q5055716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d78c65f6c4e688dba1f16346c9f2232db2349156","datavalue":{"value":{"amount":"+0.7621739506721497","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2981954$F47153F9-786C-4243-AD32-09D831D80F43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb365a5be43980699e4ccd2c54c58af74a822692","datavalue":{"value":{"entity-type":"item","numeric-id":1362142,"id":"Q1362142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc066bce78fd6f4186f36a7b952d55fe9cb1ef23","datavalue":{"value":{"amount":"+0.7540383338928223","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2981954$4238F21A-959B-4E5B-8DDC-97C62C9C5A2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7617193e8711127a2d10b89cea10e226298a4bd4","datavalue":{"value":{"entity-type":"item","numeric-id":2985776,"id":"Q2985776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3773c544d423c5c02d0031da3bafc4ec65305487","datavalue":{"value":{"amount":"+0.745576798915863","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2981954$BC5B873D-2862-4490-8D78-1B95C92BFF5F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2981954","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2981954"}}}}}