{"entities":{"Q6151610":{"pageid":13285917,"ns":120,"title":"Item:Q6151610","lastrevid":57443136,"modified":"2026-03-30T23:13:41Z","type":"item","id":"Q6151610","labels":{"en":{"language":"en","value":"Certifying expressive power and algorithms of reversible primitive permutations with \\textsf{Lean}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7803175"}},"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":"Q6151610$7F94777B-D47C-45C9-BEEC-EC08F3D73F0F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2a3236813f74694c71c16a6d93b390b32a6bbb3a","datavalue":{"value":{"text":"Certifying expressive power and algorithms of reversible primitive permutations with \\textsf{Lean}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6151610$9D71C293-09E2-4A32-890F-4C05F90DE0A1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4329e2ea841404848d2ea4e6ba499ad648cd9ba","datavalue":{"value":{"entity-type":"item","numeric-id":2097419,"id":"Q2097419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$D00456A9-0B77-4EA8-A907-CDC5AA046F75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7fe2e34ceb1a5a0fc819d5b27ac5700ee0e0306","datavalue":{"value":{"entity-type":"item","numeric-id":737108,"id":"Q737108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$CAD6BA17-2D6E-4AAA-B379-04674AC21A89","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2532b82fbfd494721e144e8b872f80867d7316e9","datavalue":{"value":{"entity-type":"item","numeric-id":246441,"id":"Q246441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$9DC4BB9F-5A1A-4B04-8B53-417E17E2EE4C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e2690d5dc291ad0ded12f2eb8597187f840576ab","datavalue":{"value":{"time":"+2024-02-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6151610$271072B8-CFA1-4F02-AE0C-BCF2544D4099","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6151610$B100EA47-CCBD-4648-BD86-C01820A8A845","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ed90be7b24a8b8223bdece7994b0cf590d6cf70b","datavalue":{"value":"7803175","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6151610$F05F35D0-5E1B-4F43-B69E-132D541E29AC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8035d3b6d7d9a37791aa6f0d7914506938dbd83f","datavalue":{"value":"reversible computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q6151610$147F1A14-F115-4E5A-9892-567FC8847BDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac91c497e5a12b747663afac74f58bf2ab28eb97","datavalue":{"value":"primitive recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q6151610$1CBCE626-06E0-467C-85BB-4C42FB036841","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e8fd89fa28c0f6c3672ef10c3a2104586281edb","datavalue":{"value":"Lean","type":"string"},"datatype":"string"},"type":"statement","id":"Q6151610$B33E3E25-10B1-48D7-80E1-8F8123ECFEA3","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":"Q6151610$CDFF2CEF-5FCA-4101-92E4-234F758A8F09","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cbb81131a9746f49f0faa267c7fe88f677f75e31","datavalue":{"value":"https://doi.org/10.1016/j.jlamp.2023.100923","type":"string"},"datatype":"url"},"type":"statement","id":"Q6151610$B0BEDC55-5FB5-4665-ACBC-9BB0B5CECD33","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f5d645307ceac2b53ff7b4d878987359f911594d","datavalue":{"value":"W4387873252","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6151610$0E2FE8B1-3D54-4F75-906D-8F7EA63B448B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bf5d30377b1d88f6fded624586a0306b8b2d38d","datavalue":{"value":{"entity-type":"item","numeric-id":3629225,"id":"Q3629225"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$B16F538B-A285-48B3-9476-602418A2C538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84574726939c563ff0c1d253534b262fc319b9f9","datavalue":{"value":{"entity-type":"item","numeric-id":3076735,"id":"Q3076735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$F472658F-CE82-4580-947F-CE90B11114C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36643d132f53e3cc2affee54b5315e94aed0558a","datavalue":{"value":{"entity-type":"item","numeric-id":1684627,"id":"Q1684627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$5187806F-F8EF-4BB3-971A-5EAE01E2E0CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d64348ad348372cadfbc43f64ea26ea379dcc05b","datavalue":{"value":{"entity-type":"item","numeric-id":1989331,"id":"Q1989331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$ADB16112-240A-42C3-96FA-4C642453AF8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9635365b0780328d7ae22bc69b462e7144999d03","datavalue":{"value":{"entity-type":"item","numeric-id":5573961,"id":"Q5573961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$341E8896-F6E1-44E9-874E-A4CEB7CE03E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b729a52ad4fc74104ed077cfa51390d6480c163","datavalue":{"value":{"entity-type":"item","numeric-id":2039893,"id":"Q2039893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$36165482-C7B7-40D9-8DA7-581AA2E9BF9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9db4cf58426c9ea10d231a6a0aa9dd7c938708b8","datavalue":{"value":{"entity-type":"item","numeric-id":1401215,"id":"Q1401215"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$1D4CBB6A-1B66-4B2C-9529-6EBB820A5471","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a6a9a34084d4e9eef8d1389ed4cb5b4c36757fa","datavalue":{"value":{"entity-type":"item","numeric-id":1989327,"id":"Q1989327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$C90380DE-6649-489C-9D91-A98A8416E3A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8242928870aab67343ad0152eb7ca8357168f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$06E0C3FE-E647-4EA8-A1FD-0BA336F01E92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93654b425fcdd746a5e9e21b3c746b60c6dc1952","datavalue":{"value":{"entity-type":"item","numeric-id":2097420,"id":"Q2097420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$549988E0-C6E2-4386-81F2-989A0B183016","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c8847fc96bd6cc15667c599e80d53cc2bce3050","datavalue":{"value":{"entity-type":"item","numeric-id":2462635,"id":"Q2462635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$5F446ECF-A864-4C74-AC18-8AF1840D4A3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98791e67835c414f0f96760868bb6411dc74eb22","datavalue":{"value":{"entity-type":"item","numeric-id":1123625,"id":"Q1123625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$38F0BB9D-E26A-478D-9FE9-F33C2C95DB45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"abc213f810e809eb3818c9e2bbad1ade805e212e","datavalue":{"value":{"entity-type":"item","numeric-id":5875420,"id":"Q5875420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$FC82602D-1C1F-47CA-894E-F8EF6D6EDA36","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"20271a156060cb9edec9471e4c35ba2c286b2658","datavalue":{"value":"10.1016/J.JLAMP.2023.100923","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6151610$AFF69A91-C8B5-41F1-A890-66D49401A555","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6151610$A999D051-5F03-4898-BBDA-E4FC7F9FE40D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6151610","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6151610"}}}}}