{"entities":{"Q817858":{"pageid":819706,"ns":120,"title":"Item:Q817858","lastrevid":64566678,"modified":"2026-04-11T20:45:15Z","type":"item","id":"Q817858","labels":{"en":{"language":"en","value":"A certified, corecursive implementation of exact real numbers"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5013348"}},"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":"Q817858$963FAD38-F87E-4F21-B68B-4462B47EF475","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b5757126a30fedb622aa2eb98abd1e5314bea728","datavalue":{"value":{"text":"A certified, corecursive implementation of exact real numbers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q817858$5F57A03A-CA5A-41F0-B799-44DF5C235C9F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dc22c95bbdf3f95206b6219eca63e479ec5f7032","datavalue":{"value":"1086.68117","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$27D05F8F-FDA9-444E-BBA6-494329E83F1F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d71615fb71a3a07e792b53a1795eab8ac6d26f1d","datavalue":{"value":{"entity-type":"item","numeric-id":817856,"id":"Q817856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$42B9EA66-62FB-47C5-A1D4-0386AD7C5EE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f97058f80ad0e559576a478b1123296489a1948","datavalue":{"value":{"entity-type":"item","numeric-id":817857,"id":"Q817857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$0E56E955-26C1-4737-A1BE-0D6C378294ED","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$9F13CF91-2C95-4EE8-B747-86A57CEB5490","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"87871fabe918b62ae0b497aecc54a3998d2fdfae","datavalue":{"value":{"time":"+2006-03-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q817858$7F3ECAFA-9A36-4FBF-B0EF-CE57DC3898F9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$FC63EC8E-7D3F-4F55-AECC-7ACC9A3763D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7dde57cbaf704d564d8f981ca98d6340e3d4aaf","datavalue":{"value":"68Q05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$FE6E8EF0-4FB9-41A4-8FDF-D74D3CCF8E50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0282342b24b585fa878a09dabeb8eb52c72be5a3","datavalue":{"value":"03F60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$CFC4AAE4-580F-4D58-AA32-C08850B7EAAE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"43a0de39badb18158b047afca379a7699b909eec","datavalue":{"value":"5013348","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$B7A10ADB-5F6C-4319-B50B-79770E1F170F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36de0ebf26a8efe51a41fd3675f8b65e177bfccd","datavalue":{"value":"exact computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$F817A081-7C3E-4EAF-89A8-E7E6C188228F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"70af58bfd2c1c27af1f77a80cebfef6e81de3e90","datavalue":{"value":"streams of digits","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$01EA1955-4852-4223-B6FC-06D3C916A009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b2d8512ce04716b57b367877299ffeb1a612e40","datavalue":{"value":"lazy functional algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$EF9308C8-A1EA-4410-B7F3-A9A1397A08AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0d889d55356161dadec8bafa4cc877ba03f24fd","datavalue":{"value":"coinductive type theories","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$4CAB6EEA-4ADB-4755-B47E-0333E6811980","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$76DD83FE-8B44-4534-868D-BA5B44E45978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f0ba1fdba7b454f488f3b788f02b8ab766af5b01","datavalue":{"value":"program and system verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$F0575A37-BF1B-409B-A469-91A538936397","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66040eec798fa7d182443c16b59531175d83cf5e","datavalue":{"value":"logical frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$00A4C864-AA71-4A4F-92A3-D57B2650D7CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q817858$9A45CF2B-91B8-422C-9840-50B6168AA02B","rank":"normal"}],"P1463":[{"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":"Q817858$29D8A9BA-F66F-4A00-B6AF-87BAD7EAC95A","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":"Q817858$365043BB-B880-44B4-8004-637D21B86105","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5bc9c71d0bf0e8e5852ff68473e0630b3cb38fc3","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2005.09.061","type":"string"},"datatype":"url"},"type":"statement","id":"Q817858$16D9D191-6C25-43D0-B87A-ED8F9AC5B1DB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2e77a6bdcd567604957dec3dd4827d794b14c927","datavalue":{"value":"W2132370466","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$C1E3A66A-97F8-42B7-9E29-F290DC17249E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4122519b918206897f0af20a4d6bc87fe7850995","datavalue":{"value":{"entity-type":"item","numeric-id":5573965,"id":"Q5573965"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$408B534F-D5A3-46C6-9EA7-E285D3C067B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f00fbc1e561c6327fb187f9c2abb111a98a00842","datavalue":{"value":{"entity-type":"item","numeric-id":1292399,"id":"Q1292399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$854477BA-5724-4671-BF7B-62AE239DA6AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d20bcfebac6a448ef8340db0231c73f600de2f9","datavalue":{"value":{"entity-type":"item","numeric-id":4594262,"id":"Q4594262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$15DF0280-77D7-4C8D-BD51-414C12D89B97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c7b765168c0167c7b6d6154d04245f069af66e6","datavalue":{"value":{"entity-type":"item","numeric-id":2766803,"id":"Q2766803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$B28E1316-0B85-4D91-B652-9E8D5C2D0158","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cc30551d025f035ee8521b0fda860bbe93085c4b","datavalue":{"value":{"entity-type":"item","numeric-id":4736388,"id":"Q4736388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$68FA155C-0C53-4B83-8910-2A8819566161","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$A9F8CC2D-21DB-4509-97F0-CF1C45A43D01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bceb4b852e855ddfca8f6ff6c992758c8fcf1113","datavalue":{"value":{"entity-type":"item","numeric-id":4736391,"id":"Q4736391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$44DC95AA-DF52-44C5-A0EA-24534811F30C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c9a8987a7d8efa9b320ab9f4c18049ee75db52c","datavalue":{"value":{"entity-type":"item","numeric-id":4457464,"id":"Q4457464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$FB0DA24C-C5E2-44F6-B6F0-28BACC5965A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c91066f858fa64a799af591825e0694228fffb","datavalue":{"value":{"entity-type":"item","numeric-id":4122841,"id":"Q4122841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$F2A30B6C-C633-4A04-856B-C0F7BF940E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2002e9228b023d08f49489031907fa50fb1b3491","datavalue":{"value":{"entity-type":"item","numeric-id":1188500,"id":"Q1188500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$4F0BA2F9-85DE-4049-8965-238F247A5FDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66e8a62cd46463c62f9ff883109d60c4695ebc92","datavalue":{"value":{"entity-type":"item","numeric-id":4485693,"id":"Q4485693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817858$4F8EF77B-FA70-4D8F-AC11-95BD799DE70E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2ab76c09411745bd0b29ea74fee9219fcf89d211","datavalue":{"value":"10.1016/J.TCS.2005.09.061","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817858$F0694154-73AA-4972-B094-55D3B2B4646B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ad4c053fd4fe39c501b9b259118832ad25383ee","datavalue":{"value":{"entity-type":"item","numeric-id":2766803,"id":"Q2766803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d755189f8ffc25683b2137d4ca8a3b533ef973b9","datavalue":{"value":{"amount":"+0.8543084859848022","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":"Q817858$F2F84691-4428-4D23-9D06-26F6207771F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d85afd2b3561ea2818747e1775ff78ee754df219","datavalue":{"value":{"entity-type":"item","numeric-id":2863898,"id":"Q2863898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f0e6a9cbf83976a8d688bdb7b5817009324f57df","datavalue":{"value":{"amount":"+0.8533872961997986","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":"Q817858$E06D1E1C-EF37-4C9C-9482-E80C57136A59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a15a471f7738a1b9392baf200b6dd58995712b84","datavalue":{"value":{"entity-type":"item","numeric-id":1015372,"id":"Q1015372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2b74b70527d276e107ae70e4177af9f5236fb038","datavalue":{"value":{"amount":"+0.8483259081840515","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":"Q817858$6E11C662-29C3-4096-8F5B-F466A17B511B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d97cb94e392302237f2f3a394c50c071b2af711c","datavalue":{"value":{"entity-type":"item","numeric-id":3644745,"id":"Q3644745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b58f564d575c46ae2aca53f3516f7ce0397b2ebe","datavalue":{"value":{"amount":"+0.8441452980041504","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":"Q817858$B8A8BD54-3720-4646-85F6-D27FE25EAF73","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":"8c9ae311edf71270a3dd2d7615be032490da4428","datavalue":{"value":{"amount":"+0.8335118889808655","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":"Q817858$42F3EE4A-4C74-4F46-90CF-0EA7FE6D9120","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A certified, corecursive implementation of exact real numbers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_certified,_corecursive_implementation_of_exact_real_numbers"}}}}}