{"entities":{"Q4913763":{"pageid":6943342,"ns":120,"title":"Item:Q4913763","lastrevid":58369908,"modified":"2026-04-04T22:23:53Z","type":"item","id":"Q4913763","labels":{"en":{"language":"en","value":"Type classes for efficient exact real arithmetic in \\textsc{Coq}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6152231"}},"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":"Q4913763$C7BAB98E-2CD3-46A2-B67F-B99E575E39ED","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cf14a58a45fc5724912a3d0e487312738fd2aaf0","datavalue":{"value":"1260.68378","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4913763$92B15BD5-A2CC-458C-9D82-87F28DF12838","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d784fe6cc5179886bfe36c86ddc8bdd92ade5a26","datavalue":{"value":{"entity-type":"item","numeric-id":549190,"id":"Q549190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4913763$48C00DC1-9EB6-482C-B883-49A3A230D436","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"603d1427f1b21e289d7f29d1759e5e0b15783239","datavalue":{"value":{"entity-type":"item","numeric-id":185814,"id":"Q185814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4913763$C9AAD47C-ECB2-4293-A700-EFB1B07D9988","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e8d05c5960e17df88a20f497dd893bcc369c3eaa","datavalue":{"value":{"time":"+2013-04-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4913763$347347AA-7F3B-4000-B145-133326CE9DD2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1961773cda1240f4d27c44e8ba7faa09c2f91866","datavalue":{"value":"https://arxiv.org/abs/1106.3448","type":"string"},"datatype":"url"},"type":"statement","id":"Q4913763$0CC1B174-D1AF-493A-A91B-C1EA296ABE5E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4913763$64ED51F4-A7F3-4A59-9E1C-D91BD8391AC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"235c6ea5e302e28be6b7d95307dac1a9f1d2b5b4","datavalue":{"value":"65G99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4913763$CC625278-63FD-41EF-B918-5E1F0C254FF9","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c4f1d06056adbc4a029f98c311a7afee2d866f0e","datavalue":{"value":"6152231","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4913763$77BE6CCA-B463-45B1-878E-FF4DADBE9476","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff33796796e98480bd831c12f8abdaa6ed1568ba","datavalue":{"value":"type classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q4913763$56B3DEFE-1E4B-4509-8699-5A0FADD1EA11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c68e78acfd8da85726644b8041d98f4d34edab34","datavalue":{"value":"exact real arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4913763$B8127B19-2209-443F-9E9F-54C8B7760B05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4913763$607515B9-5C87-40F3-BB3D-51199F78BD28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"905c185b35495bc6c5c2ada6dd808940c7264ec2","datavalue":{"value":"\\texttt{Coq}","type":"string"},"datatype":"string"},"type":"statement","id":"Q4913763$A3140A47-E5AD-437E-92B3-80A531983B89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6aeba89ca924fcec3a5675b10e3dcf02d05673b1","datavalue":{"value":"verified computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4913763$0971AA2A-9246-4725-9CE4-5E51B7E87D8D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7bb1c7eafdbb853d5fe04051d89b8463fa8b943a","datavalue":{"value":{"entity-type":"item","numeric-id":18827,"id":"Q18827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4913763$A45A5415-0408-495C-A254-CB95A2D5B0D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0d21fe96e365ecf6c3640683e7818e20408c5a90","datavalue":{"value":{"entity-type":"item","numeric-id":41908,"id":"Q41908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4913763$630A0F75-E301-45CC-9228-86DFA13DB38E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4913763$3318C3B4-5E85-4F08-A60D-F5DD9C8B9EF4","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":"Q4913763$4A426B06-162F-4639-881B-08A8B7502834","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aa786b5c8269f6cf517ad0f032932817c0bb268f","datavalue":{"value":{"entity-type":"item","numeric-id":18875,"id":"Q18875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4913763$3B3E2B26-3023-4EBE-9F92-8E03D82080EF","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":"Q4913763$431D894D-3644-4005-BAD1-70386771A2E1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dd8570b53c061bb8e760410299465c633b887606","datavalue":{"value":{"entity-type":"item","numeric-id":5200110,"id":"Q5200110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a253732261bd96a1d7f3fc82070cb1592da186e7","datavalue":{"value":{"amount":"+0.9421969652175904","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":"Q4913763$DB79A5A2-0B83-4B25-BDAB-2224710D3DC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac0ce1a15a6f8a98914f6aa448f055825b864ff2","datavalue":{"value":{"entity-type":"item","numeric-id":714617,"id":"Q714617"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a576c0eddd82fba538bceccfb5276e66b2b4a7fe","datavalue":{"value":{"amount":"+0.8074982762336731","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":"Q4913763$7733BE9F-6CB6-4209-9DC2-4510AD4D0048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d93184323b25f8cf549364d04d765260ce21bec4","datavalue":{"value":{"entity-type":"item","numeric-id":817858,"id":"Q817858"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef85ce4d5c71667cafb773bae9f48584dbda1eb4","datavalue":{"value":{"amount":"+0.8016306161880493","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":"Q4913763$2B4E62C2-3341-435E-B7DA-CFC53F747046","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0141b06b756e6120b1cab3d217636fe8b682d289","datavalue":{"value":{"entity-type":"item","numeric-id":5458427,"id":"Q5458427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b72abe339f658e742b0df889cfb126a4e979a5e","datavalue":{"value":{"amount":"+0.7919477820396423","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":"Q4913763$980827BC-3576-4B5C-8A84-8F051587FC46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f35972ae61dc081a3614608bd04d82ea882ee1fb","datavalue":{"value":{"entity-type":"item","numeric-id":3543662,"id":"Q3543662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b717be85765bb25fb86205587e0f0dd33cc7290b","datavalue":{"value":{"amount":"+0.7905769944190979","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":"Q4913763$03B791AE-B833-4948-949A-2032643B785B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4913763","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4913763"}}}}}