{"entities":{"Q2968412":{"pageid":2979137,"ns":120,"title":"Item:Q2968412","lastrevid":85436600,"modified":"2026-06-03T08:16:17Z","type":"item","id":"Q2968412","labels":{"en":{"language":"en","value":"Extracting imperative programs from proofs: In-place Quicksort"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6694180"}},"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":"Q2968412$0BF751D9-9106-4401-9415-CCF543018BD6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"231f3e66ffaf6d32dba84acb8a3b306b86b40cc9","datavalue":{"value":"1359.68042","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$14117CFC-B79D-43CF-AFFC-E00CA1CA12A1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"56802c23e662b5a0028381459762dce10bc420a6","datavalue":{"value":{"entity-type":"item","numeric-id":234584,"id":"Q234584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2968412$2CAF8DC4-3D3A-4339-93C0-96A2D3CC44B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d06c1321f49508cea4a158e2ae71d33c1ecda72d","datavalue":{"value":{"entity-type":"item","numeric-id":693062,"id":"Q693062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2968412$08567515-23A3-44C3-BC9A-257DCC687A42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bda18ce68a5c1bc7c5502b4c57b511b57870205d","datavalue":{"value":{"entity-type":"item","numeric-id":2968411,"id":"Q2968411"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2968412$3978BFD9-4193-42B8-8F62-543B94C35365","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"856edffdf82e86092e797d3b8ee58dc208c2c6a3","datavalue":{"value":{"time":"+2017-03-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2968412$E3281D08-1D38-4437-9648-47D6E4723867","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$55BE4705-603C-4ACD-907C-3D5F5B5FFC1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$CD3EF6B8-D943-45F6-B541-595C2DB71668","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$504AD645-8D4C-4A85-B959-3DFA22FEF799","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0df8fc04cc71716773fd156f4d095007dc503453","datavalue":{"value":"6694180","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$6CCC9EBF-380F-4248-968F-243DDEF075D7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$E3D672B8-675B-48F5-A0D8-AF8DB13E667C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$A40BBEEA-F14A-481F-B367-38B0DF1CB343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"53d61092cbbff856a3b199e03225e42bcac6db78","datavalue":{"value":"realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$9E896F25-8C1B-47D9-86C7-ED798AC13806","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8469432c7e2e4cd59d964f83e69cb11b07596610","datavalue":{"value":"imperative programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$FC49A0EF-D868-44FE-AC4E-70FE0C1B983C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7ed35b802fc03831f9de08660d92ded9beb8ddd9","datavalue":{"value":"In-place Quicksort","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$448E5024-DFE7-4903-9694-FF59BCC0822B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1cd5153255d72a16ec6e318a93f0b26ea57939b","datavalue":{"value":"computational monads","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$387988FD-0F84-415E-8517-5376D53BE7B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02b7f01fa066541cf231442e5716591d6f993081","datavalue":{"value":"Minlog","type":"string"},"datatype":"string"},"type":"statement","id":"Q2968412$D1F65411-E613-4CFB-9D8A-8666D58C2DA1","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6e1a240c321e56a4c4972fd8e23ea8cd8e21bff0","datavalue":{"value":{"entity-type":"item","numeric-id":21744,"id":"Q21744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2968412$FAE08672-0B8F-420F-BFE6-9C418D3E6C01","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":"Q2968412$DC2CF4F7-0BE6-419D-9CDE-31F5FC838040","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fd48d1f1d19bddb451d8a186f7becee83f01587e","datavalue":{"value":"https://drops.dagstuhl.de/opus/volltexte/2014/4627/pdf/p084-05-berger.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2968412$9F022BE3-3940-49E9-B0C9-21A6797C1F04","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d9bad220fb0487242b5b8e9166997c6c3996e455","datavalue":{"value":"W1522541548","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$44823E8A-FD19-442B-80CD-AAC774619CD6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1c9807b13154d1e76e94a881752efee35d118ad1","datavalue":{"value":{"text":"Extracting Imperative Programs from Proofs: In-place Quicksort","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2968412$A86172D1-32F6-4978-A8EE-7407D447480C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"91eaf5b23c52983a2196faba1c9c81f0dae3080b","datavalue":{"value":"10.4230/LIPICS.TYPES.2013.84","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2968412$B1DD1D6A-5ED9-4034-8CF7-31219FA73263","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"31e06b4fe6c983bb3ab4de626b40fdcb19de88e0","datavalue":{"value":{"entity-type":"item","numeric-id":1823656,"id":"Q1823656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1bd03fa7f9cbfa1f8e3d9921258091dc9a604932","datavalue":{"value":{"amount":"+0.7807831764221191","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":"Q2968412$C97314CC-B93E-42D8-AFB0-10A9A27B1BC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81235c4d3f4c66b6911717e8cbf43cd34a5bdfea","datavalue":{"value":{"entity-type":"item","numeric-id":912594,"id":"Q912594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b5fb602c704accdd495045cf4420ded47c119159","datavalue":{"value":{"amount":"+0.7748847603797913","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":"Q2968412$A0C56174-437C-4C6C-8FED-77C8BD8BBC03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46cbfbc17791325b36a30a473853d313c8e6f88f","datavalue":{"value":{"entity-type":"item","numeric-id":1648867,"id":"Q1648867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f09c2d4ac86e5365e09a48410ebe4d03bd2ddc2a","datavalue":{"value":{"amount":"+0.7611974477767944","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":"Q2968412$3E78053C-06E5-4823-AC59-B3D1CAA39015","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cc18ee63967d27b68bef5b3a1749be5e3c0935e","datavalue":{"value":{"entity-type":"item","numeric-id":4435458,"id":"Q4435458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e388c712ceaafa5209eccd086e2c7890af501af","datavalue":{"value":{"amount":"+0.755851686000824","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":"Q2968412$E5427A60-3137-4D6B-AA7B-DEECA38676C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"126be7296d6b7110e1000144e41a4b9d8fcc6ece","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03a2ad5dcfabb46b3460b67eb91a015a3f87b850","datavalue":{"value":{"amount":"+0.7432755827903748","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":"Q2968412$C9057D81-00B8-481B-8D81-417D5F25111D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extracting imperative programs from proofs: In-place Quicksort","badges":[]}}}}}