{"entities":{"Q6923518":{"pageid":21044017,"ns":120,"title":"Item:Q6923518","lastrevid":84135827,"modified":"2026-05-11T00:57:58Z","type":"item","id":"Q6923518","labels":{"en":{"language":"en","value":"Extracting efficient exact real number computation from proofs in constructive type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8099522"}},"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":"Q6923518$54929DF7-68DB-4482-91A5-3CFF10C501E9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1ae4c0bf771f4354e7cc7170a001d91ac553b930","datavalue":{"value":{"text":"Extracting efficient exact real number computation from proofs in constructive type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6923518$B0E3F9E2-C1DD-4744-A10D-DAE6B175463B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8743bee70627b87c86d21862c5071f7b01fd91aa","datavalue":{"value":"10.1093/LOGCOM/EXAE066","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6923518$27C790CE-A9E4-4918-AC6B-564BEBCB28B4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"71f7a423d7ec55ba984d2e14faa1ff96597d329a","datavalue":{"value":{"entity-type":"item","numeric-id":254163,"id":"Q254163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$273EB574-1F67-4C69-B1DB-ACED770BADB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a630879ccaa4c21630472591755ba89df50ec18e","datavalue":{"value":{"entity-type":"item","numeric-id":260175,"id":"Q260175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$CA586339-B131-42F7-AAEE-B66C0B8F5055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9cdee734ffa77906c36b38f540e8794957a5d4e2","datavalue":{"value":{"entity-type":"item","numeric-id":831999,"id":"Q831999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$0F8D2009-A08B-4D97-9F6B-6873CDB228A8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4e284497c1d95ed03031b32369f55bf404c9e002","datavalue":{"value":{"entity-type":"item","numeric-id":6768690,"id":"Q6768690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$BE4D8583-B80D-4B46-B26D-9E50D9F85CAA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"67b571ae3ce5d75bc39c8248f19a512a27075c5d","datavalue":{"value":{"time":"+2025-09-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6923518$5F2F9FD4-662B-41CE-B9A5-D83C1C146FCC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7a1d4d343889492e30dd853837039fd3cd08322a","datavalue":{"value":"03-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6923518$5343FB1E-1180-4EB7-B5D6-58BD6EE219B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6923518$3BDA5244-B612-44BF-BA87-7DC8375CD198","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8e8165be4eeabf0dbebaea65b8fd350680a67bf5","datavalue":{"value":"8099522","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6923518$AACAC432-7861-414F-901F-293243FC3B1E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3d759d48ec4ae609a46c2c3b612bebd8f4939d92","datavalue":{"value":"constructive real numbers","type":"string"},"datatype":"string"},"type":"statement","id":"Q6923518$CC1B02F9-6FA3-451F-BA4F-874679558020","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"55caf05c57404ab910cf1d6d785d791abcc73ea3","datavalue":{"value":"formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q6923518$71DC2394-27AC-4E07-A0A8-CFC70E33257B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b229ed9383ed2232d0f4aa93f4113d23427c959","datavalue":{"value":"exact real number computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6923518$3D46E2F6-49A0-4DCB-9F8F-608E2B58A337","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6923518$9C0A1915-51BC-466E-B545-A5FB74C3E98F","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":"Q6923518$2BEC1F7B-81FC-4BC3-8FE7-FA9087CE296A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"918f2ab1b9ec59829674d3c94f9d64972bb8ff93","datavalue":{"value":{"entity-type":"item","numeric-id":1015372,"id":"Q1015372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$28193CB7-75C7-485E-AEB5-00142C729BBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"63933023c2b92e8f26e17359d374c320ae00c929","datavalue":{"value":{"entity-type":"item","numeric-id":5278412,"id":"Q5278412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$1CA560DF-9103-450B-8EB6-4F52F46EE55D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de8be793d43ccbcec7fd4c624e4436431c592807","datavalue":{"value":{"entity-type":"item","numeric-id":2220485,"id":"Q2220485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$DC739873-CC44-4488-A012-DEE7C3FE9A95","rank":"normal"},{"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":"Q6923518$6C1CFE24-F322-4C0B-A041-3ACAE2902FA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbb7fdabd5a856f8e1d09080b76afc7309a50a3e","datavalue":{"value":{"entity-type":"item","numeric-id":3637269,"id":"Q3637269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$10AA52CE-30B1-42CF-9AD1-31AFB79EE278","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc90f519741959885c97856c7164fc497d5566b1","datavalue":{"value":{"entity-type":"item","numeric-id":2973239,"id":"Q2973239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$8D40375F-5ABA-4761-A80C-B1519266A35F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ab1fb3b741de6ad15a6cf3e725ed00bb86921b6","datavalue":{"value":{"entity-type":"item","numeric-id":5274886,"id":"Q5274886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$2D80C92E-B0E2-4975-892F-48FE84207899","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"277a19545eca3d3587926ef01bfae42aa94c848d","datavalue":{"value":{"entity-type":"item","numeric-id":5140200,"id":"Q5140200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$039A2E39-568D-446E-8359-9C9C294D10E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca4eaaffe954537216921c73f393b9d06098a9c9","datavalue":{"value":{"entity-type":"item","numeric-id":1279912,"id":"Q1279912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$2CEDFFF5-5B5D-4B0B-A9D2-14E83D69E1BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7cd68876abdd58647e84af16093f8bce867abd5","datavalue":{"value":{"entity-type":"item","numeric-id":6487409,"id":"Q6487409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$77C00BFE-5349-4F04-B977-4BBEE8E50CCA","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":"Q6923518$CD7FAE8E-6507-4D35-BADF-F05ADA6E1ECE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b02cebc44c2831878b18e904086383fc947d3037","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$759B189F-75E4-4076-B999-2A13057F38A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6eea79f11eb3478d0537dd5c1cde79192e8dc27","datavalue":{"value":{"entity-type":"item","numeric-id":5441002,"id":"Q5441002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$DDE179AE-4F42-4A4D-9B93-0F2AFFE5DE05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e7df3906eae3c2b887cc910e28b2339b9830fc52","datavalue":{"value":{"entity-type":"item","numeric-id":5313080,"id":"Q5313080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$A0DF1E3D-3237-4CD7-A0B6-0AAB4D2B03BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ea65857c6c049fdc48aed336cd6c70e162f8ae0","datavalue":{"value":{"entity-type":"item","numeric-id":2299211,"id":"Q2299211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$2A5DB000-FE50-499D-AF1F-6E1CB52ADDB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4726a5d4743e198a171b14042c89ae025f0ef064","datavalue":{"value":{"entity-type":"item","numeric-id":4243908,"id":"Q4243908"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$49528B62-F2B0-40C1-9CAD-B7E5B583E4DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb54e6eb505dee5c4fe6f451936f1b75a4e767e1","datavalue":{"value":{"entity-type":"item","numeric-id":4474857,"id":"Q4474857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$3831F67E-6B32-448D-B880-D7260A7C6958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d6acb3eb05828de28f2584c746c0d8ef3e38672","datavalue":{"value":{"entity-type":"item","numeric-id":1279608,"id":"Q1279608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$1662C386-E33F-4BBE-BEA1-0857B45726E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50e55698549203a710dc73f53d8efd7aa10bd9c0","datavalue":{"value":{"entity-type":"item","numeric-id":1799286,"id":"Q1799286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$E82DABBB-594E-4FA9-A907-29CDD7758A79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8e1b21288875b8284999fc64c197e280596881","datavalue":{"value":{"entity-type":"item","numeric-id":6839852,"id":"Q6839852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$1DFF7396-2379-4C98-94B5-3AD43CFF7F7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4846833055bd6cc0b39b0f908c138bb4cef2949d","datavalue":{"value":{"entity-type":"item","numeric-id":2148797,"id":"Q2148797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$5A1614BB-0275-42A9-A2C2-3A5C862269CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4af769b87d49a62b854d9114364a61655ea375b","datavalue":{"value":{"entity-type":"item","numeric-id":2330561,"id":"Q2330561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$337839F3-433A-487C-ABD9-40589BB8D77C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71989260ea67bc4b5ba36054c70da0e87718c8d1","datavalue":{"value":{"entity-type":"item","numeric-id":5200110,"id":"Q5200110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$55E39CDE-A24C-47A2-80BD-CC054AB3A785","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b14dd23e439d8a5676d55733e6e6fc2f64720ea6","datavalue":{"value":{"entity-type":"item","numeric-id":1073022,"id":"Q1073022"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$C17BC361-163A-4713-BFCF-1A6874680FCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1484fc6ae5032c0644f4322db26bf86d8db0d4d","datavalue":{"value":{"entity-type":"item","numeric-id":1245217,"id":"Q1245217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$0F719842-7FAD-460B-8A40-916C79E9D727","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a61099a476f9a57129d822e2de0c2a34fbb0d06","datavalue":{"value":{"entity-type":"item","numeric-id":3541683,"id":"Q3541683"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$E229891D-71D0-430E-BC9D-2CE1F17710D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5edca5f1b7cbe413037278593fddcc0fdab39989","datavalue":{"value":{"entity-type":"item","numeric-id":5740678,"id":"Q5740678"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$7B3A7496-4252-41B6-9850-0AC16902CF3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f30365d42caf6766e6692a155b036d7f93a051e","datavalue":{"value":{"entity-type":"item","numeric-id":4531992,"id":"Q4531992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$26B65168-D76B-41F9-89E2-B5DBB7E69C04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78972e0dfbf7207842dca7100ccec8637ca3e796","datavalue":{"value":{"entity-type":"item","numeric-id":1679677,"id":"Q1679677"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$5ECBF9D2-0153-4AD9-B731-8D050C001B37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"390367f7aaf1bf5f1955bd4bab78a8eb5df8953e","datavalue":{"value":{"entity-type":"item","numeric-id":3431547,"id":"Q3431547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$E7BCC033-F913-42FA-AAFA-67F9AAE02963","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a15f025b82e462b08b6da310a0699c520bda9047","datavalue":{"value":{"entity-type":"item","numeric-id":3543662,"id":"Q3543662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$713B9B17-345D-4607-9E2A-38463FF4E078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60b8958c11cf12e9828f35bf950395907ec01462","datavalue":{"value":{"entity-type":"item","numeric-id":987984,"id":"Q987984"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$9C23434D-15E7-4A28-B625-AE3FA39022E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8ca643b60ebdb93e4f644b5a215affb30f564fa","datavalue":{"value":{"entity-type":"item","numeric-id":6563064,"id":"Q6563064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$3FD77FE1-93A7-420E-8804-176550C02B28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1374495af3930b21180042cfbcf82ed4d49a9f36","datavalue":{"value":{"entity-type":"item","numeric-id":4499143,"id":"Q4499143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$662E760D-906F-499E-89F3-90FC9F6D2C2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da60596735b1de63e9cc7cd04f41b24092deab21","datavalue":{"value":{"entity-type":"item","numeric-id":4787859,"id":"Q4787859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$056E06E5-15DD-4524-901E-4EFA749C84A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e5535cf4be6e9985903d73b8af103848456d31d","datavalue":{"value":{"entity-type":"item","numeric-id":5435637,"id":"Q5435637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$D4C91BBE-D4BF-4213-9DD2-99E6EEED50C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68b9b6e1876a7ef6a8d3ae40b917b0c350a8b4db","datavalue":{"value":{"entity-type":"item","numeric-id":5790901,"id":"Q5790901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$A46962CB-3B84-4209-84C3-C424C6ADD876","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad4168c7403b3e6139601a0e087b810e4ec38e2d","datavalue":{"value":{"entity-type":"item","numeric-id":4989411,"id":"Q4989411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$D65FFF31-6E7D-47BD-AB47-C628A8640988","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45e2187512867fe4f712404ca585a26321bb0036","datavalue":{"value":{"entity-type":"item","numeric-id":5286647,"id":"Q5286647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$13B18E1C-9AA9-4E79-887D-746F7C31B85B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb99eb66c25fe4c4058c32bc65bca0017ab853cf","datavalue":{"value":{"entity-type":"item","numeric-id":1011333,"id":"Q1011333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6923518$94C19238-1B12-4933-A534-6E0BADFB6B63","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":"Q6923518$2F907D87-CC00-4C2A-80CC-80DCA88F96CA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extracting efficient exact real number computation from proofs in constructive type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extracting_efficient_exact_real_number_computation_from_proofs_in_constructive_type_theory"}}}}}