{"entities":{"Q1799114":{"pageid":1809856,"ns":120,"title":"Item:Q1799114","lastrevid":53239778,"modified":"2026-01-24T12:59:51Z","type":"item","id":"Q1799114","labels":{"en":{"language":"en","value":"Verifying asymptotic time complexity of imperative programs in Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6958121"}},"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":"Q1799114$1E2E1F37-2B04-4780-BEC2-D4B298F65506","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8db895c9f1ebdb54eab2b605ce0529dce91a872c","datavalue":{"value":{"text":"Verifying asymptotic time complexity of imperative programs in Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1799114$A35DBCF8-CBE1-48D5-A353-AB87024DE91D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"98054f44b4e041e1a980317834f96a92d2b61c40","datavalue":{"value":"10.1007/978-3-319-94205-6_35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799114$633B3F0D-B4CE-4593-9DDE-C1B7F7D40B21","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d47a0b532fadc119a2da0b4f59e3906ea7d12d94","datavalue":{"value":{"entity-type":"item","numeric-id":258840,"id":"Q258840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$66974574-B261-4F18-87E3-886F94DE463A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c1d33c2cb482f696fa81fcf6b993c9bc4e7576e8","datavalue":{"value":{"entity-type":"item","numeric-id":1799113,"id":"Q1799113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$850E5240-1739-410E-A116-90F4C99E3997","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1799114$C36B30DF-8B07-44FC-BF90-A83B3A26CCA1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fe3440ea43f95df03b52b7f157f2529257205436","datavalue":{"value":"https://arxiv.org/abs/1802.01336","type":"string"},"datatype":"url"},"type":"statement","id":"Q1799114$7A116F5D-8132-48AF-A659-567FE8B8A3B1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799114$6C123DB7-286E-41EB-A381-49BF070A5907","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799114$A3AB02AA-5724-4D77-B950-1500023AC392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799114$E91280B3-3E7D-481C-AAE4-0A56ED00A782","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1cc49da80ec7fcd9fa832a9c19da8e310ed1ebb3","datavalue":{"value":"6958121","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799114$4FFD81FE-3BDC-43C5-983B-F464B07A91D2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799114$AFF4B9F0-2F2B-49FE-B58D-7A2BBF7C6D95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0677cb0d983c977c2f44635a6a8e9e9cd3414ca1","datavalue":{"value":"time complexity analysis","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799114$60CD373D-C338-41DD-9069-1F99E7EF5CD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799114$C7CED050-607E-476E-88C7-394F3A236048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1799114$A83AB173-92AE-4F86-AE28-A382049ADFCC","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":"Q1799114$8FF70057-0C81-48BB-971C-5E86F9CDD72E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$F0B3085D-7C2B-476A-BB25-E7A7722FEC7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8d339879d056b1662f5af84b9896ce6b40246d9d","datavalue":{"value":{"entity-type":"item","numeric-id":43957,"id":"Q43957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$5004D5F3-8F76-4082-9C20-A6F1BDCC4F12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d082feafa45d8fd2af5638ac3cc0080de90d3ac","datavalue":{"value":{"entity-type":"item","numeric-id":40263,"id":"Q40263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$096FC833-FE9D-4270-AB19-1A055D5DCD7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$5B675971-FCF0-48FA-B63E-7903CF87889A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e7faabf74dc18d0f41bd3f5c99c24fed967b6378","datavalue":{"value":{"entity-type":"item","numeric-id":29452,"id":"Q29452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$BA56465D-8124-490B-A8B9-66B0EE9C3090","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"68e5df8c3dae7752bf7f3ad5b01ba30abc445cad","datavalue":{"value":{"entity-type":"item","numeric-id":39280,"id":"Q39280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$A7FF4C0C-A62B-4C22-9151-EBADD2B721BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2c491ca24cb85bbd6f9c4698ce87ed511fac835c","datavalue":{"value":{"entity-type":"item","numeric-id":40310,"id":"Q40310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$052F8AC3-A7A8-403D-A49A-E053BA8B6E2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"29cdafe150c2f905fae45ec9e0724a076d6dee21","datavalue":{"value":{"entity-type":"item","numeric-id":41251,"id":"Q41251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$0B63ADB6-00A0-4702-B07A-16B097215445","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2f69537ed7c37995dd62cdaaa7c2aa36c1a11909","datavalue":{"value":{"entity-type":"item","numeric-id":41252,"id":"Q41252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799114$7F0FAB0F-FDF7-4CBC-82B7-42BD8F18FA49","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":"Q1799114$F508C4E1-13BB-49E0-9756-2F84D7598362","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3870fea45105d357a92595efa769af3f08e89bf0","datavalue":{"value":"W2964083189","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799114$A1984BB0-2D82-4C8E-AAA2-993D74236DF0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59bfbdc7e86cccf445f54e1e3091c5033971a071","datavalue":{"value":{"entity-type":"item","numeric-id":2323994,"id":"Q2323994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa77972eeff6a3bf948f5e2cbbba4ee146a136d6","datavalue":{"value":{"amount":"+0.8235533237457275","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":"Q1799114$A91B494E-D93C-4544-86F8-4663009AF303","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54dac0ad3a84c5897bebd78827e84bdb3c2abbdb","datavalue":{"value":{"entity-type":"item","numeric-id":2324204,"id":"Q2324204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8242f86f09a373a7a872d8308513a093eecef1d5","datavalue":{"value":{"amount":"+0.7354008555412292","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":"Q1799114$AE7D12D7-5CBF-44C1-AE5D-ADFCBFE09242","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d2be8401770ae0a8798151eb1914f05246d53c1e","datavalue":{"value":{"entity-type":"item","numeric-id":670699,"id":"Q670699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"107b17807345dfac32377190f7c65761eebad4f4","datavalue":{"value":{"amount":"+0.7255369424819946","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":"Q1799114$C96D3046-587F-4DDD-9441-1A3683C9D7C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8f17d04554222e5b1937078aa86886c179cc1a46","datavalue":{"value":{"entity-type":"item","numeric-id":2945628,"id":"Q2945628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5905f5a773f292c25adfa4ae5a0dff8a61e07383","datavalue":{"value":{"amount":"+0.7232534289360046","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":"Q1799114$D5322D89-F135-4B4A-B968-E9B1DD92A276","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"959be19baa4476667a8bf253e7c26f9c31eafdc1","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89cb942274c086aaed1321a12a22b13b4651be5c","datavalue":{"value":{"amount":"+0.7226787805557251","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":"Q1799114$407A7BA2-9489-4E5C-A0F0-4D2C6602B815","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1799114","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1799114"}}}}}