{"entities":{"Q3183520":{"pageid":3194228,"ns":120,"title":"Item:Q3183520","lastrevid":80028047,"modified":"2026-05-06T15:16:33Z","type":"item","id":"Q3183520","labels":{"en":{"language":"en","value":"A Brief Overview of Agda \u2013 A Functional Language with Dependent Types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5618500"}},"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":"Q3183520$3029A5BB-6EEE-4558-8818-61181C2B6F40","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"361924b6b95e1fb658a5c03a0884e96260ff07b0","datavalue":{"value":{"text":"A Brief Overview of Agda \u2013 A Functional Language with Dependent Types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3183520$E4CB53B3-1B1A-4428-B412-ABCC078AC854","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8ad58ceee07cf56a4d48d2df25ef65c1ca61dfc5","datavalue":{"value":"1252.68062","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183520$179A156B-74E3-4CA7-8F0C-3714F7AEFED5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8e578beaa6619958cff8862323472872c01d6175","datavalue":{"value":"10.1007/978-3-642-03359-9_6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183520$F09F2E8E-6290-4E10-BD2D-85C049E9785E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"43fa8ed1a432c4af2ca647b623e8e3f5c6fe6565","datavalue":{"value":{"entity-type":"item","numeric-id":1744409,"id":"Q1744409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$BA69BA20-B2E6-4468-83C5-DB13D4940CBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d75275853fb84ac426baf809ec86decf612055f","datavalue":{"value":{"entity-type":"item","numeric-id":651314,"id":"Q651314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$6C950695-E2FE-4BF8-8EDA-F5F72E5C2E40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"121420623aa3457d6aa5126f26a1fd007c4c6074","datavalue":{"value":{"entity-type":"item","numeric-id":3183519,"id":"Q3183519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$1A62C09A-BA81-4220-B833-3659790CAF82","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$A10B8167-D235-4850-8CAF-134AB768722A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4b03fe0d32567f363cc3207214473a7371265cf3","datavalue":{"value":{"time":"+2009-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3183520$9C8CCCE4-B5DE-4C2E-863B-FB3EAA049889","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183520$C0B8B3E2-778F-46CC-A15B-F948E198831B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183520$92F49405-D408-4C69-94BB-FB37C5A8B4FA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"707e835e09982a89186b2509718369179b66e8da","datavalue":{"value":"5618500","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183520$0BDE2BED-D305-4CDE-B0FB-D45B50B98C75","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":"Q3183520$D3D64898-EE57-4877-AB47-34256D68B899","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$A7CFE5B8-E6A4-4CC4-93DF-6D3DA23F7E63","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":"Q3183520$80788987-BEB5-41BB-99EA-E037E4575C4C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f0bde8270c7d0c472ab3a840c230c3c4de8fe4df","datavalue":{"value":"https://doi.org/10.1007/978-3-642-03359-9_6","type":"string"},"datatype":"url"},"type":"statement","id":"Q3183520$1EB40788-C2D1-46A5-8C7C-5428F7B795BC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0e8e4ed4e8a62c809fb1dcad54485231005f293d","datavalue":{"value":"W1558175043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3183520$CAD096DA-2A02-470D-88AE-6C6DC660D113","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$5BF7A2C4-A330-4089-A241-8E112B32FF81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"027e4855cde125bdc1bb418924731ec6618aa622","datavalue":{"value":{"entity-type":"item","numeric-id":5191088,"id":"Q5191088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$14BA325F-A3ED-405A-A992-0DDC974623F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$0EC9F6D5-46B1-4C6D-9BEE-4CD24DF92028","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0191c8d55bfb13f05e230de930538ee944fa6808","datavalue":{"value":{"entity-type":"item","numeric-id":1336951,"id":"Q1336951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$6A8B6770-7CEB-4097-926A-87DFB458568C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"364525b70d80e5ad032dd4bcb752b39f36195669","datavalue":{"value":{"entity-type":"item","numeric-id":4508246,"id":"Q4508246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$DC4227B7-0E1D-4B06-943C-3F880D527DF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"220e7bd07cfc86bd56365fb168aa15481d8c02d7","datavalue":{"value":{"entity-type":"item","numeric-id":2577476,"id":"Q2577476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$AB6C126C-0B95-4430-81B3-2CD1E8593C6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"545b70a52fbd739fcbdc5fb79649e5d3315f9433","datavalue":{"value":{"entity-type":"item","numeric-id":3598006,"id":"Q3598006"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$78F5DF5F-843A-4875-9E64-297F0A51FB46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6ee172cf1bbc62eabf7dd1b43feaebcac6a2fa9","datavalue":{"value":{"entity-type":"item","numeric-id":3886868,"id":"Q3886868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$0ED82F00-69FB-453B-89FF-51C39D6EB0B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$2607278C-8C26-4635-B0BA-C493830E99D6","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":"Q3183520$AC113B61-A259-43C0-BCD6-9B16DA8FD269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1cb314be56584c4a3b78c42d4c6a1e8e149e010","datavalue":{"value":{"entity-type":"item","numeric-id":3649136,"id":"Q3649136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3183520$0D363A59-07CC-4568-884D-C84854269C14","rank":"normal"}],"P1643":[{"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":"08450004a875b87d9176f790f4081c30c39e83fb","datavalue":{"value":{"amount":"+0.9049173","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":"Q3183520$2DE6B585-6B69-45DD-84FB-F63EFE1CE048","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27e06515956bdf64098be5a872edb3320002254f","datavalue":{"value":{"entity-type":"item","numeric-id":5016211,"id":"Q5016211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c606e8433746cdaf487e15931ce7b7af251f4f7e","datavalue":{"value":{"amount":"+0.8978542","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":"Q3183520$F27C90BC-EE48-401E-B8E1-5B773A83B055","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d3b7bcd1d68db7d577128e4a5c1fa35ac4c5ac0","datavalue":{"value":{"entity-type":"item","numeric-id":3644935,"id":"Q3644935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3229974d6a37877a6ab668609e26b96a767a8e17","datavalue":{"value":{"amount":"+0.85690576","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":"Q3183520$BD6403E2-087D-4E8C-9720-2DE10E993F95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"32855381b841b2f251643e7696e8b54441703099","datavalue":{"value":{"entity-type":"item","numeric-id":6079228,"id":"Q6079228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f040c6896087e2405a3dcfcd595a533e2654b0de","datavalue":{"value":{"amount":"+0.8445944","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":"Q3183520$CB20C490-3CA4-4236-829A-7DC6CFEADBEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2808296c78d138368e61e821e9f5a75db030f7f3","datavalue":{"value":{"entity-type":"item","numeric-id":3002481,"id":"Q3002481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1671e502aaf316929d2cf83702a74ec37be047e5","datavalue":{"value":{"amount":"+0.833999","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":"Q3183520$A58D5721-14A2-4415-BF59-346ED7E31DC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"358995f440739c95e401811ea48d338eda2492a8","datavalue":{"value":{"entity-type":"item","numeric-id":5741554,"id":"Q5741554"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd957b9956630ff030f17fe990d588df4d0d323b","datavalue":{"value":{"amount":"+0.83214706","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":"Q3183520$F09CD133-9781-4D37-AA3A-B912A8B530D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57dfed40ad76c1909dac7454800a8de7e13eb374","datavalue":{"value":{"entity-type":"item","numeric-id":6068934,"id":"Q6068934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59f492785107d533558799e5fa6a7f77934cdebb","datavalue":{"value":{"amount":"+0.828255","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":"Q3183520$4F8F5BAA-BF17-45F6-B05A-A7687DCFCFEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f78239855dab5d379d904c9afe4d265edfaac228","datavalue":{"value":{"entity-type":"item","numeric-id":5089035,"id":"Q5089035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4140a5afdd1002d1d3619c1e503aa0528a188432","datavalue":{"value":{"amount":"+0.82772017","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":"Q3183520$0F8B1C6B-DAF3-456A-9367-0879F7065DAB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Brief Overview of Agda \u2013 A Functional Language with Dependent Types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Brief_Overview_of_Agda_%E2%80%93_A_Functional_Language_with_Dependent_Types"}}}}}