{"entities":{"Q2503336":{"pageid":2514079,"ns":120,"title":"Item:Q2503336","lastrevid":49917403,"modified":"2026-01-12T00:52:00Z","type":"item","id":"Q2503336","labels":{"en":{"language":"en","value":"Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5054326"}},"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":"Q2503336$51D471DC-5E80-4364-8759-333ADE7CAF81","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"70e1152268f5fcff891c3d30e6acc615f583549c","datavalue":{"value":{"text":"Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2503336$E48EEB61-3B70-4624-9096-64757D39A474","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c6c9b8b2766afad1946ed1d9dbf0bb37720e19e5","datavalue":{"value":"1099.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$C9AC967F-7797-4240-BEE1-907F77E64065","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6575cff51975739d551f57056395ae004f63ff1a","datavalue":{"value":{"entity-type":"item","numeric-id":2503335,"id":"Q2503335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$9FD90EDB-7071-4DF1-9331-3ABC54D04B95","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$32B457CC-CF2C-4C37-9A08-23F3985B414D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f4ffc608ada8e4a14c4a7ac75bb9921c404be25","datavalue":{"value":{"time":"+2006-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2503336$855B19E8-B04C-48BE-B382-840139748C41","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$378FB69E-301A-4F83-9E66-CFA02A5B0A71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$8FBC8D70-C2C6-4CAB-9F1A-5DF26FE60E43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$ED4F0CC2-1D4E-4073-BA4B-F17C8123A723","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$A5AA5FB7-9C0F-4D93-8BC3-23DB6B6E6378","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"44bfe90f17a7ad0027a9dbba6d9564554d8f86b7","datavalue":{"value":"18D15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$656B59B1-6F49-4661-95E6-0656E952FCE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$0F4BA0BC-CD3E-442A-9A7F-4A467E04BCC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$775A4D90-8F7F-44B2-A0A7-C496F375186D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"76ea10dd88fb4d94b43a64d057c09c8bc65e53ba","datavalue":{"value":"5054326","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$5AC6337E-B7D4-47F9-A43E-7060A4CEB247","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503336$E2C75415-E367-4C2E-8D63-77540E52DFA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50da3e22f353aab60122cf77f58fb715a3c4aa9b","datavalue":{"value":"interactive programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503336$10C78EF8-5F82-4863-B96D-79D7BAF4907A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e1f5cd0980353ef12c3cca1547f9f9bc9bbd8890","datavalue":{"value":"coalgebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q2503336$43BAEBB8-E9B7-49B5-96BB-EDC3A7AEE37B","rank":"normal"}],"P1463":[{"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":"Q2503336$BC974E52-8020-4C56-9512-ABA6F4630B5B","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":"Q2503336$B316717B-1099-4FFE-A041-7DE926915CB1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"45090ad0ad61c77c3da0389b85dd5a011908f6b9","datavalue":{"value":"https://doi.org/10.1016/j.tcs.2006.05.033","type":"string"},"datatype":"url"},"type":"statement","id":"Q2503336$A596119C-2D83-4C44-8155-62614386689B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f85a54ecc990f768714021afbff96d7408324bc1","datavalue":{"value":"W1965763876","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$353F0317-67CF-4104-8B5E-699B83DA7030","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"03fbca56191e433ddad7d589e9817e8f20721a5b","datavalue":{"value":{"entity-type":"item","numeric-id":4417849,"id":"Q4417849"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$9FC03916-03FE-4463-87B7-BF22BEEC9A8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f4edb495601af130d31283333a6e85af411ec6","datavalue":{"value":{"entity-type":"item","numeric-id":4457445,"id":"Q4457445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$7274055D-A158-45CA-ADB4-143A344A80BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6dd3b5cd7b22633fdc01dc1070528c5c96b5c8b3","datavalue":{"value":{"entity-type":"item","numeric-id":4681360,"id":"Q4681360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$860E395F-CC90-4320-BC45-4ECA35AD5594","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79aa05cbdf7e9c30715a43e649084cfac28e9645","datavalue":{"value":{"entity-type":"item","numeric-id":4457833,"id":"Q4457833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$7C118F10-9D87-4F0E-BB55-2DB514CD3719","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":"Q2503336$48C551A6-8549-43F3-8D51-3A80DC6FB2BD","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":"Q2503336$1EEECDED-8094-48A9-A9F4-1158DF842F94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c24d98fe8151a7ee984475d5ecd61101306ad23e","datavalue":{"value":{"entity-type":"item","numeric-id":4461768,"id":"Q4461768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$212A481B-D8A1-431E-B9B7-1B9F6861F053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b4dfbaa0e17e1ebd4172fa6deb841857771ca02","datavalue":{"value":{"entity-type":"item","numeric-id":5712306,"id":"Q5712306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$10607AC6-25EC-45AE-B11E-44C4DD9E294F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bb3a3eb73ddc5bb5845397c93ec55eceb2ef8c6","datavalue":{"value":{"entity-type":"item","numeric-id":2575770,"id":"Q2575770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$31F709CD-E580-4630-9E31-406DC0E5C61A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c43b86216fe1c5702aab5ae75ac68f23c82c002","datavalue":{"value":{"entity-type":"item","numeric-id":2753682,"id":"Q2753682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$9DC7FEF0-2F7D-459A-B945-0B2C3AF825CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9c5d4cff434102bed227e3e021e251aecd1efd2","datavalue":{"value":{"entity-type":"item","numeric-id":4236885,"id":"Q4236885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$16AECDF3-E1F0-4B86-8B83-9C115817FFA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65d374a999f00d07f932ef685e3747f62c43ff1b","datavalue":{"value":{"entity-type":"item","numeric-id":5311250,"id":"Q5311250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$75AF1DA9-687D-4515-B27A-080BFBC9C080","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e33b53c9004b61a90401a2052769d8efa2f34a0","datavalue":{"value":{"entity-type":"item","numeric-id":4120115,"id":"Q4120115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$284E60BC-0D08-47AA-B0E9-F8CA74E375DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b922f86164ec53ebebd54c2fd6306ff8129ffc0e","datavalue":{"value":{"entity-type":"item","numeric-id":3822156,"id":"Q3822156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$7BD2186C-FCE1-4716-A1D8-6B88F4881CCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3bbf5c4acba1e943106282227d496dff22117d6","datavalue":{"value":{"entity-type":"item","numeric-id":4238487,"id":"Q4238487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$5652FE07-38EC-4D82-BF63-65128E83768A","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":"Q2503336$6E86F20E-9A9E-450B-88A3-C5398D5E2E13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c3faaf5806bffb98996997da8da058ecfd89e5","datavalue":{"value":{"entity-type":"item","numeric-id":5752569,"id":"Q5752569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$867F2C83-41D7-4C77-95D7-361E2A23DF44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d91a6fc5a255cbadfa617ce94146193166c4f9ed","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$D5D20CB0-E800-4969-9D1C-F03CAC927177","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"89bef463cb658cddbd9f9784826ecb28ab8be5ea","datavalue":{"value":{"entity-type":"item","numeric-id":2503336,"id":"Q2503336"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$6904E4C8-6161-47CD-A4AC-023F1487DB4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66f882b16138e41fa0c717226b3709126034f01d","datavalue":{"value":{"entity-type":"item","numeric-id":5897609,"id":"Q5897609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$30DABE0F-AAAC-4237-BA25-31BB37DE1B47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b27bc1bc7aed1d424f54d60aa2047fc82fd3285","datavalue":{"value":{"entity-type":"item","numeric-id":2849882,"id":"Q2849882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$F87C8E2F-CD47-45B8-ACCE-BE7DE5967C5B","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":"Q2503336$DFDF8A36-8014-413D-BD24-6351BF05709C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a3f5182c5f84b08fd5162da8260189a7d667355c","datavalue":{"value":{"entity-type":"item","numeric-id":4247308,"id":"Q4247308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$23654163-7A76-4860-B780-F42308E248B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd7a8d1c5be3816c0eac56917cb8b0244a44b6bf","datavalue":{"value":{"entity-type":"item","numeric-id":5438968,"id":"Q5438968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2503336$44D05880-E8EE-4475-BF00-1FAC14C2F64F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f86c47729322ed32dbcb5d2a2606b3335f5a9665","datavalue":{"value":"10.1016/J.TCS.2006.05.033","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2503336$F1BDA370-DAB7-46C7-9268-4B6EF81B4242","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"433a68f0d59c31b22fabad5184270d1ca2e16b6d","datavalue":{"value":{"entity-type":"item","numeric-id":5718566,"id":"Q5718566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0e6aee5f9e8e708e4b237df5dc29641ff14f3a7","datavalue":{"value":{"amount":"+0.854343831539154","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":"Q2503336$6227F1C5-5439-44B2-BB8B-D1C1F712E761","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d314eca77b725a7ecd863408b025bc4d09438404","datavalue":{"value":{"entity-type":"item","numeric-id":2849882,"id":"Q2849882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11ad511297c17a264921f70c56b23351c6e178ec","datavalue":{"value":{"amount":"+0.8143715858459473","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":"Q2503336$B73A034E-5C09-448E-AB6E-6BA8D07F6F12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0041265b30330555ea416b4f65d7526eb233d647","datavalue":{"value":{"entity-type":"item","numeric-id":3638258,"id":"Q3638258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74c14162a2b644f9d388c075d7c885cf637a345e","datavalue":{"value":{"amount":"+0.7733115553855896","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":"Q2503336$D65AF921-1AAC-48C4-990D-590105E3ABFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b5d5a7f7c75195facb34a525a726911d710bb2b4","datavalue":{"value":{"entity-type":"item","numeric-id":5897609,"id":"Q5897609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0c4f138585c23e64bec8727ad622878abae72d2","datavalue":{"value":{"amount":"+0.7513816356658936","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":"Q2503336$1B3B20F1-6DE0-44B0-87F0-E95FEF025188","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67545d5628fd3e254d6d62ebccfc0af8654ad1d0","datavalue":{"value":{"entity-type":"item","numeric-id":5739360,"id":"Q5739360"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db79b2681bb9e8b38925f4192579b9b3b38550de","datavalue":{"value":{"amount":"+0.7461322546005249","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":"Q2503336$F7A182FD-9C2A-495D-8F71-07283FE0590F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2503336","badges":[]}}}}}