{"entities":{"Q5458429":{"pageid":7487988,"ns":120,"title":"Item:Q5458429","lastrevid":50334086,"modified":"2026-01-13T20:28:35Z","type":"item","id":"Q5458429","labels":{"en":{"language":"en","value":"On-Demand Refinement of Dependent Types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5262482"}},"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":"Q5458429$F1F856B5-FC2C-4DA8-86E3-69E5251937E1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9bc826a6fe747467a64deba0fee1ffd8b1b25367","datavalue":{"value":{"text":"On-Demand Refinement of Dependent Types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5458429$53C25B3C-80CE-4E03-9FD8-8509B4B6D0F6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"531469c872b2f2939bfdd5826cfaa5f875ea71ee","datavalue":{"value":"1137.68358","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458429$F6994404-3323-4514-B2E9-098FCFD95A26","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7045f6e026fe66ba5299d75d6d0cbd8ce9e376fb","datavalue":{"value":"10.1007/978-3-540-78969-7_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458429$C82E41A2-9352-4810-AD29-1B322EF5F2AE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad89601800dc23413dc7ca174df857b300e44e3e","datavalue":{"value":{"entity-type":"item","numeric-id":832226,"id":"Q832226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458429$7EE17C9D-60AB-4FFF-B81C-E18934430B34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e3ed03c0e908613601fdd733dba97c4f4513b0a5","datavalue":{"value":{"entity-type":"item","numeric-id":238500,"id":"Q238500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458429$6B516D2A-EAAB-4F9D-BCF7-A08CF285313F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a2a09b5cba4f9e4657809ce2fd194ee37ff6e885","datavalue":{"value":{"entity-type":"item","numeric-id":2798252,"id":"Q2798252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5458429$236F6FF6-590A-4E8A-8CF9-44B3164A77FB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de5306c1211a7dcd78b6214088eb3e5b7092fd16","datavalue":{"value":{"time":"+2008-04-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5458429$9D36AF8A-9345-4B11-81D4-7608DA6AF19A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"db249a588ab157a08053d1017009fc82df2e6658","datavalue":{"value":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.722.8731","type":"string"},"datatype":"url"},"type":"statement","id":"Q5458429$569F5829-FDF7-40F2-948D-5A4428AA3581","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458429$388251AC-CB96-48BA-B817-49A9FF751150","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2cf98c8be1317ec135dc394b78814da781176214","datavalue":{"value":"5262482","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458429$361A99F9-A769-440F-961F-8EC10CF536FD","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":"Q5458429$6D642AE2-23C1-414A-89B1-49B05C4D2986","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c5f7828863b6427a1fb838bbc83ad09c70ba73d1","datavalue":{"value":"W4206095045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5458429$60CF8F7C-B9D7-4EBC-9DD4-EA32F1457213","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf742c5a4fbd9ddaf673b1e54c58866fd6463e56","datavalue":{"value":{"entity-type":"item","numeric-id":5255067,"id":"Q5255067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"36b889c28b457091d506c7de3ce77d789b68d76e","datavalue":{"value":{"amount":"+0.8152652382850647","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":"Q5458429$CD75C12A-641E-4371-88C5-847AB6623853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cbedd6ab3dfe1136ec5ec551c70488fa195c1012","datavalue":{"value":{"entity-type":"item","numeric-id":4673424,"id":"Q4673424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"976e88231de175b393ebba36ee3a2ce87a81aa43","datavalue":{"value":{"amount":"+0.7689988613128662","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":"Q5458429$B051740B-BD0C-4FEE-A0D1-0414D8C90767","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"23680f141fd2144ad476fea8a6ad3dcd9befc86b","datavalue":{"value":{"entity-type":"item","numeric-id":5756515,"id":"Q5756515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9fe3c9990f3c983d60dc20400c2deb88c4c5e5e4","datavalue":{"value":{"amount":"+0.7519329190254211","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":"Q5458429$8C584FCD-A452-43EA-B9AC-520257AE66E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb749952a68c5b82e606596cc60d6f39df18bd79","datavalue":{"value":{"entity-type":"item","numeric-id":5030192,"id":"Q5030192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d71d52a5ca58291841f29f4a02e0c03963ca5a8","datavalue":{"value":{"amount":"+0.7470144629478455","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":"Q5458429$72FFDED9-9CF6-474B-98B4-261209E3F0D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac2f3df0ee4da1afbd28d0537e0f2f5f54498b5c","datavalue":{"value":{"entity-type":"item","numeric-id":5172655,"id":"Q5172655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"582780f8c91a914f52d9dce3b8c164bfc85fce29","datavalue":{"value":{"amount":"+0.7410991191864014","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":"Q5458429$60D4F912-32FB-4B4D-9539-0E126EBF2360","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5458429","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5458429"}}}}}