{"entities":{"Q7361439":{"pageid":31519856,"ns":120,"title":"Item:Q7361439","lastrevid":105423599,"modified":"2026-10-08T13:45:26Z","type":"item","id":"Q7361439","labels":{"en":{"language":"en","value":"Efficient Mergesort"}},"descriptions":{"en":{"language":"en","value":"AFP entry Efficient-Mergesort"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"68082576424f0628832c77adc2ead458845d00fd","datavalue":{"value":"https://isa-afp.org/entries/Efficient-Mergesort.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361439$81D380A3-4AA9-4241-803B-ABC7F3E28646","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361439$066754BB-225B-4AB4-932B-A3D1DFD4CC04","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"9b2bb9e346479df2436b5cd23ba391a7c3211900","datavalue":{"value":"We provide a formalization of the mergesort algorithm as used in GHC's Data.List module, proving correctness and stability. Furthermore, experimental data suggests that generated (Haskell-)code for this algorithm is much faster than for previous algorithms available in the Isabelle distribution.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361439$87587443-443D-4663-A8B3-288310EB42A8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2634de497e429ca644a44809d012b4bf029e7a02","datavalue":{"value":{"time":"+2011-11-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361439$C3017EA2-9DC4-4CB7-B7AA-46650A5D3F98","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cd759f4557fcda242c4f4e16af572d53d94b1aa9","datavalue":{"value":{"text":"Efficient Mergesort","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361439$3F70109B-EB03-43AD-A60E-6D4E4D537E16","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$772BCE78-B040-4C1A-B885-9EDC3D9D3FAC","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$38CBDBFC-530E-4353-877D-47D46C446669","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$12E60E92-B66E-48E9-8C38-339C07C9B408","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"4bc716578de43d8fe587cecc1d20a068fa8e94b2","datavalue":{"value":"28579","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361439$A2587645-014C-4107-BA13-2EEBE68D1FF4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361439$856D8351-8A72-43BF-89BC-D2AD848D954C","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$87C77CAA-F2F2-4CB4-B442-9C0D9C2B2C3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$62DCCD06-68A4-41DD-9D23-3FB783044534","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"61d0c0612cc30c9c51b93ddaf1f78ee1ae75f9fe","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$B71B25E3-DD15-40BF-9868-A62308212F20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$CAEAB8AA-231C-4D03-BB95-F5AC51A1DEAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361439$8B601578-E6A2-43D4-8DD5-13900DC57E7F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient Mergesort (AFP entry Efficient-Mergesort)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Efficient_Mergesort_(AFP_entry_Efficient-Mergesort)"}}}}}