{"entities":{"Q843222":{"pageid":845070,"ns":120,"title":"Item:Q843222","lastrevid":42723157,"modified":"2025-07-09T13:58:12Z","type":"item","id":"Q843222","labels":{"en":{"language":"en","value":"Dependently typed array programs don't go wrong"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5609497"}},"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":"Q843222$A56D76AD-14AE-474C-9E8A-E6B5A8901931","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"256cc8943c0a437f2a0cb5373d4faa19a79e8712","datavalue":{"value":{"text":"Dependently typed array programs don't go wrong","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q843222$B5283AEC-D7CC-4F18-839B-5907D09F6627","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"73f59266d251b4365a7d0e887437e625af1c3563","datavalue":{"value":"1187.68320","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843222$9A6A63B6-468D-4580-A119-5C20B3E4E4DF","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa5bdfc85f29b48fda3891f464fb303def1382b6","datavalue":{"value":{"entity-type":"item","numeric-id":843220,"id":"Q843220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$1BBE9175-091A-4C26-860C-8C8E64D96009","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bdbfadaf80931278c43bd722d7f6dbe08a1469ba","datavalue":{"value":{"entity-type":"item","numeric-id":843221,"id":"Q843221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$4D42991B-B43D-4418-B683-34C3880185D0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"786ecb874cd758b218aa4cf99a475aee0b3588ed","datavalue":{"value":{"entity-type":"item","numeric-id":175862,"id":"Q175862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$5B6E74A8-57AD-4443-B6BB-D600F05E97B9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3a20869fcd975d123d10d62c56ba2fbfe1c71aa3","datavalue":{"value":{"time":"+2009-09-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q843222$16F7A23A-796A-495A-BB9A-678538625A32","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"59e589efa098274ba35af736c06cb0c7744a89a3","datavalue":{"value":"http://dare.uva.nl/personal/pure/en/publications/dependently-typed-array-programs-dont-go-wrong(f5e7edc3-30f6-4fc9-903a-b886513faf9a).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q843222$706A8245-5845-4CFC-8BA4-52769866AF1B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843222$9CCCA1A5-FB28-4930-9C8D-B29AE6F2940C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"517ace4a4f9c45a5475b4a8927a567447dbdb293","datavalue":{"value":"68N99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843222$D5E79542-E53C-4B33-9021-9EA100E06A0F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e0cfde1dbd7177b0cca7cab4b6cb8636439bb8bd","datavalue":{"value":"5609497","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843222$ED8735D3-5A4C-40BF-9B49-7D91C6AF0432","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8b9785f558a843a538a42687878142adbac57f21","datavalue":{"value":"array programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q843222$F969E380-4EC0-4EEC-9C88-F534F9A34C80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q843222$DBC60F18-E7EC-457B-A14D-98EBED2B5C8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q843222$A292EF9E-B0C8-457D-9518-DB8CFAF6B7D8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a709ac7c97c67049e241e0b036253f1d955c589a","datavalue":{"value":{"entity-type":"item","numeric-id":13313,"id":"Q13313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$4E4FCCC6-B550-4197-837D-666A0CC5A4CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"97a4b6d3c8d40b2dcd33f0a7a9a105bc3e94ffed","datavalue":{"value":{"entity-type":"item","numeric-id":13907,"id":"Q13907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$8A170727-069D-48BF-8107-365B4285C636","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e41927344b9397ba2eb05288d661d38c0f0d55a6","datavalue":{"value":{"entity-type":"item","numeric-id":21665,"id":"Q21665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$D27CE20C-F33A-4176-B96E-4ABF38C8F58B","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":"Q843222$9D327521-DFE6-43B1-A7C3-6524AC53CA06","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d1dfe8bfe02c45a82e38ca9427527718024ba21e","datavalue":{"value":"W2569339511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843222$40E0C166-4C4E-4AFB-8217-181CFF5708B4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0dafb1be3c7af3b4b5138021dd75e9003d45ed22","datavalue":{"value":{"entity-type":"item","numeric-id":5706723,"id":"Q5706723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$27CA15D4-C240-4547-AEEC-DF1A9C428CED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"97ea7690139d2a7a00df4e790236d6c8f952035c","datavalue":{"value":{"entity-type":"item","numeric-id":3284160,"id":"Q3284160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$FD7A96AC-9746-4314-A85C-46FCBA04CC99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57b8eee2a5e632767a2d045008a3bbc01ebf76cd","datavalue":{"value":{"entity-type":"item","numeric-id":2431843,"id":"Q2431843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$E4B1D7D6-CD70-42FC-B12E-2612CB48C575","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b349db4d65a7235baeca61c61e087b984a93232e","datavalue":{"value":{"entity-type":"item","numeric-id":3623958,"id":"Q3623958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$E66DA6F0-0476-4A73-B801-D7DDE373A334","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e3c9740dc87f0aba4702af08773fe882498acd2","datavalue":{"value":{"entity-type":"item","numeric-id":1389626,"id":"Q1389626"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$A70B31AF-834D-4FC3-8E67-C79DDBBA4C43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e32e6c895a421389f04c5499d388fc13d53e99f","datavalue":{"value":{"entity-type":"item","numeric-id":2778806,"id":"Q2778806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$E04B062F-6C26-4AE2-9FE6-26259307C7CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ce95859b006696dd3172c086dc9b758f9304237","datavalue":{"value":{"entity-type":"item","numeric-id":843222,"id":"Q843222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$961E4EC7-4B27-4963-AAEF-13EB393F7018","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2b1ebc1ae7ffc3042b5e838a24da8662374478","datavalue":{"value":{"entity-type":"item","numeric-id":5898633,"id":"Q5898633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$2A9C595C-24CD-4CC5-841A-BD9255EA9D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4ba59d723fcb1622cd6bfe4e7c7439e2eeda1ed","datavalue":{"value":{"entity-type":"item","numeric-id":5679686,"id":"Q5679686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$67D127DC-B2CB-4A07-930B-5FE5CE4B1565","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c602c4b793e3df19813f8870b7524627f2ea56d1","datavalue":{"value":{"entity-type":"item","numeric-id":5390282,"id":"Q5390282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$C0758BAF-8E69-4D12-9898-9816BAF709B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$4439CAF8-D52A-4907-8CD2-74B6A4FEB105","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b327cf916e5c8f52b90b371017428a40a2b3f26d","datavalue":{"value":{"entity-type":"item","numeric-id":5348900,"id":"Q5348900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$DBA731B2-75B5-4265-8B36-8762A854C1BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3893e24895c818d766b4ac601e2292c1956a8e2a","datavalue":{"value":{"entity-type":"item","numeric-id":4819653,"id":"Q4819653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$F1E81BA2-052C-410E-85BB-4C7F4B8C6CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b09623b25863ff5c40989a5025b9634ea6113fef","datavalue":{"value":{"entity-type":"item","numeric-id":5501458,"id":"Q5501458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$E42F5F0C-38C7-447B-BDE2-47CD63805F34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a202c15d6f0203e77f6eb394d88152eebfc809d5","datavalue":{"value":{"entity-type":"item","numeric-id":5712319,"id":"Q5712319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$032BF278-5077-4D32-A809-7C405242065D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dc29301745cdf5b8ef90b77fe0818ff9d23948a","datavalue":{"value":{"entity-type":"item","numeric-id":2455898,"id":"Q2455898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q843222$A364C72B-D138-4FE0-82F6-A4EB4CF05B8E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"165e4184c64106bbbb294328aad9c2cccc4e0b47","datavalue":{"value":"10.1016/J.JLAP.2009.03.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q843222$407F35EB-3A27-4C4E-A3CC-425A6CBFA3F3","rank":"normal"}],"P1643":[{"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":"a815781508354bd2bfc4df6daad448c42cf4a0d8","datavalue":{"value":{"amount":"+0.8247237","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$467E4DAF-9682-45D1-83C0-856739491608","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"07564eba529568623cc22a8b64a6cd489fa3ec0c","datavalue":{"value":{"entity-type":"item","numeric-id":3617686,"id":"Q3617686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8372bfc39df7cde2004405a1ed18880b3e66797","datavalue":{"value":{"amount":"+0.8231336","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$71CA5B71-2489-465C-958B-440756F5A0E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"968ef3c413e5fe02e2d496a820a84be2c7737a1a","datavalue":{"value":{"entity-type":"item","numeric-id":5255080,"id":"Q5255080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9b8373e615213c30f3cb7bde096f1f962f2d3ac5","datavalue":{"value":{"amount":"+0.8136327","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$F6EAC24D-6005-4BD2-9B1A-C0C52CE5C634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d4246eaf4aeb7ee18b6fadc7db2ccfc3206320db","datavalue":{"value":{"entity-type":"item","numeric-id":5703756,"id":"Q5703756"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a7cb66347b742ebbfca76b78da1eacb82cb9afb","datavalue":{"value":{"amount":"+0.8107645","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$BCFBC499-62DE-4395-A473-BB7994DA65FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a95bd51c59aba038da623a377f1871ddbae4cf03","datavalue":{"value":{"entity-type":"item","numeric-id":1929345,"id":"Q1929345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b3ca8990b6e541713adc9bd3aef4919132f03f6","datavalue":{"value":{"amount":"+0.80990493","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$1C1E0010-6CED-447E-8544-CB6A705A57EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dfa2ef20d7b2efd6d194ffacf2421bc59f18ff98","datavalue":{"value":{"entity-type":"item","numeric-id":2277831,"id":"Q2277831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"071c3a8cc9554012156b63777a9b84892f442128","datavalue":{"value":{"amount":"+0.8091415","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$2B54F9A0-DE57-474F-AB34-8B5AE3822BF3","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":"46f53cccbeeca290c5577f64ad62c7962bbebd73","datavalue":{"value":{"amount":"+0.80906963","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$829616A7-E665-4982-B0C6-D9AB498C1354","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"60d330218efdb6e0dae35fc2343de58b9a5b8340","datavalue":{"value":{"entity-type":"item","numeric-id":3649136,"id":"Q3649136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61d5915422f58be77c7bb99ee665dd19b83702a0","datavalue":{"value":{"amount":"+0.7993589","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q843222$AFDBF287-7F22-4E94-B390-CCF947979D99","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:843222","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:843222"}}}}}