{"entities":{"Q4580232":{"pageid":6609818,"ns":120,"title":"Item:Q4580232","lastrevid":53167328,"modified":"2026-01-24T09:03:51Z","type":"item","id":"Q4580232","labels":{"en":{"language":"en","value":"\\(\\Pi\\)-Ware: hardware description and verification in Agda"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6917249"}},"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":"Q4580232$CD1685FE-4C7A-469F-8C51-AB0B608F9C2D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bb62fadef1ff010ae93ed5a39aeed66156e77eba","datavalue":{"value":"1433.68081","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4580232$0ADFC338-74B0-4A45-BC36-FF9C14F967AD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f66901cb9867e865543261423733486683849453","datavalue":{"value":{"entity-type":"item","numeric-id":4580230,"id":"Q4580230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$B6DBFCFC-82A0-4F99-A537-3AB5A01F623B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb347ea749674b96dcf23d1f480d130c607a21fd","datavalue":{"value":{"entity-type":"item","numeric-id":1791196,"id":"Q1791196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$EDF1B3C4-6251-439B-9E11-06AFC2C2F25D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"871cd77b477f7e305ce874fd9b04d1090e18248a","datavalue":{"value":{"entity-type":"item","numeric-id":4580231,"id":"Q4580231"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$99849B3C-DC9D-410E-94B1-6858A7622D79","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"30feba6170f0dd078cec0568a6ba1b353248bccc","datavalue":{"value":{"time":"+2018-08-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":"Q4580232$9940C5FA-A79D-4D02-9F10-3A690AA57705","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4580232$72513D40-21BE-417E-8D4D-C0CEEED6CE16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4580232$70BE63FE-226F-4715-86D3-3D3F17C9923C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a252ac0e16e7cd1b816dd4d8c55ab05955b53869","datavalue":{"value":"94C11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4580232$5D74591D-2DBE-4751-B6B9-800DAA737533","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1df8c9135a40706c764d0f3bc5a71f4cf6c98b4b","datavalue":{"value":"6917249","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4580232$A1BEA9BD-2683-4ACE-A8F6-F9724BFED834","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a5fde500c1b893101a3b51394b8a804cb1b9660c","datavalue":{"value":"dependently typed programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4580232$8C60411A-009A-4C26-A6D4-123E843D0B7F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cb0249487b7eb1ecf24cddb1d300f9fa92e8fe1d","datavalue":{"value":"Agda","type":"string"},"datatype":"string"},"type":"statement","id":"Q4580232$92E515A6-9AFB-443D-9E2E-C39277737548","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1a73e0fc9f65acc04029f2cd319efc4a6e825d0","datavalue":{"value":"EDSL","type":"string"},"datatype":"string"},"type":"statement","id":"Q4580232$027334C5-FE94-49BF-BA1B-127B7A39B6C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0493a24a84b95da82cc4dce68573310d2137b60d","datavalue":{"value":"hardware description languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q4580232$DEF0793D-2606-44D5-BC16-9EA20F174E7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00b76a2e54f8798fe172effecd557ced03e2f904","datavalue":{"value":"functional programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4580232$0E8E78AD-16ED-4DA4-BE3A-2C6EC5C5948B","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":"Q4580232$FD9925B3-2E96-454F-B7E8-FD41B8118DA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$BE2BDCAD-DE2A-43A3-BE52-3F5398AD4A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ddd31dae9cec559546306beb5fe50048bbc464af","datavalue":{"value":{"entity-type":"item","numeric-id":21898,"id":"Q21898"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$F46721C9-6913-4C5D-B35F-77DC9E6393F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bb6c2d18287764041ae60ee5f8b5af9b2b2245a7","datavalue":{"value":{"entity-type":"item","numeric-id":40357,"id":"Q40357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$5B4C61F7-D164-40D4-9193-A7460C89BCBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bab78c386ed6c81792f96e275843babc4b24bbce","datavalue":{"value":{"entity-type":"item","numeric-id":40359,"id":"Q40359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$FAB83715-B96D-4F7C-B50F-EFCC1FD13A66","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":"Q4580232$29F60E41-2CC7-44C9-A757-B6A00223ED13","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3892482ec4f186976ac2a5d19953cfb636bf760","datavalue":{"value":{"entity-type":"item","numeric-id":5493212,"id":"Q5493212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$C0CBB015-D68B-4228-AE1B-4D3226EF5EA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$45E41D57-689F-4A50-80D6-D1C64C45E83D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"64738746c7f98fb10a5cd52a09a9338c108e599b","datavalue":{"value":{"entity-type":"item","numeric-id":3100217,"id":"Q3100217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$71A2795D-43F2-4DE3-9711-2ECD0BA8FC00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e60952b47723901f82e58c54a04c5f6187f9bf5","datavalue":{"value":{"entity-type":"item","numeric-id":4025341,"id":"Q4025341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$92F306CE-36BB-4CBF-A5F7-53052E996B79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9751d8f12e3f2c7dd6bcb47ce70a0a4e9d0ee68e","datavalue":{"value":{"entity-type":"item","numeric-id":5313086,"id":"Q5313086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$C52C26AB-E1EA-430E-A3B5-0334BD9CFD58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c29368e9733758742d444e7bba01cb75642d55","datavalue":{"value":{"entity-type":"item","numeric-id":1327711,"id":"Q1327711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$5BDA7F03-0AA4-4A0D-9151-FFF47A349716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"77095c41135cb4764d3667c129e4e23c5421ff28","datavalue":{"value":{"entity-type":"item","numeric-id":2941181,"id":"Q2941181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$F2AC001F-F16B-4459-833A-1D182100A470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1bd189fa5aa1e1558cc53627e8e63ce419b9d9c","datavalue":{"value":{"entity-type":"item","numeric-id":5178754,"id":"Q5178754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4580232$E1D112BE-59E6-4B60-8F8C-76CCF7D0E452","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"00e1b07d626a106aad6a6bba761b063e245c7747","datavalue":{"value":"10.4230/LIPICS.TYPES.2015.9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4580232$BAD679DD-FB1F-44D5-B4BA-88DE72229317","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b42b0f154574fe6f9093d1067ca431c00e19f7e6","datavalue":{"value":{"entity-type":"item","numeric-id":1791197,"id":"Q1791197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c4d7e8bb0398533e08d1071ddbce4bfef7d22168","datavalue":{"value":{"amount":"+0.8468188047409058","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":"Q4580232$B696F288-3D44-4E6D-B7C0-9A892310F422","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d70d5ce8b63a6d88c2164ea8975126b43fca81b","datavalue":{"value":{"entity-type":"item","numeric-id":3100217,"id":"Q3100217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22ee8279e3d2a28b11e14477b60e4a8d839a0adb","datavalue":{"value":{"amount":"+0.7548333406448364","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":"Q4580232$FA3A3A24-B277-47F8-A7B7-65A00558ABCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3759b7d7dc516dbd11ddc44d79565c29c01c078","datavalue":{"value":{"entity-type":"item","numeric-id":1764432,"id":"Q1764432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a75c4ed8ca67c4f6a29b011bfce1a2a00a1e758a","datavalue":{"value":{"amount":"+0.7510334849357605","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":"Q4580232$C18A663F-3C2F-4E33-A372-A451DD8887CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f137b9d1cc9897b233b70f3cf7ebee3dd6baa73","datavalue":{"value":{"entity-type":"item","numeric-id":3021415,"id":"Q3021415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11793943fdee43e27a4b2a68f33cbebb94dc95bd","datavalue":{"value":{"amount":"+0.7177005410194397","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":"Q4580232$FCD534FF-05C3-4281-9026-1486D1F8EE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"806602fc7daf24c050d2c203dfd111ae30216068","datavalue":{"value":{"entity-type":"item","numeric-id":4028147,"id":"Q4028147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c047c57fb6fe7452511ea1e452961d79cd6523e7","datavalue":{"value":{"amount":"+0.7114040851593018","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":"Q4580232$1013EA79-4F6F-4EA6-AAAC-852DC7215D02","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4580232","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4580232"}}}}}