{"entities":{"Q2176683":{"pageid":2187426,"ns":120,"title":"Item:Q2176683","lastrevid":73554051,"modified":"2026-04-14T16:26:29Z","type":"item","id":"Q2176683","labels":{"en":{"language":"en","value":"System F in Agda, for fun and profit"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7196587"}},"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":"Q2176683$6D2D8150-7F5D-47AB-83C8-37FF963FD3E1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2c768ae5184d8434055f1c41d82d007ad812e90c","datavalue":{"value":{"text":"System F in Agda, for fun and profit","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2176683$D826295D-7259-49B7-8A8A-AA7BDEC482B1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ebce54c6d57a233983ecc5e77b794aadae756eb6","datavalue":{"value":"1434.68079","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2176683$E6AA05B0-6F1E-4C9D-9634-7E20E46C2A6D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e1ddc30add24692bc75dced2e6ad77ebf25cead6","datavalue":{"value":"10.1007/978-3-030-33636-3_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2176683$147CB1CD-77F7-4CC7-8EF7-DFFCC3438B98","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8b90cf39e1945178350ae0461777360f2997cb3","datavalue":{"value":{"entity-type":"item","numeric-id":2176681,"id":"Q2176681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2176683$69F49928-09B9-4AD2-BE77-75FE8F7EEB2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"166b1ca88463a72cc711678e1da421e9c1c5270b","datavalue":{"value":{"entity-type":"item","numeric-id":2176682,"id":"Q2176682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2176683$6F2EAD3F-987F-42B4-A443-8FAD207AEC6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d8fea356f84d37a924ceb58cfe03d1b4469ed36c","datavalue":{"value":{"entity-type":"item","numeric-id":879365,"id":"Q879365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2176683$CB5B5CF4-1119-42AC-94B1-E8AA57A824E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00aa7e93fa7f222310ed2c02639443a3d00d9426","datavalue":{"value":{"entity-type":"item","numeric-id":635961,"id":"Q635961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2176683$6331184E-0E3F-40A7-8BDC-3100F7445952","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ffa913ad058323c97cdd62b11ad32d016ae0804","datavalue":{"value":{"time":"+2020-05-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2176683$6D21147F-2C4F-44C7-AF25-73CB73C6C59D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3cd3af00c492c7dd24f62a0409512655c9081c34","datavalue":{"value":"https://www.pure.ed.ac.uk/ws/files/129967822/System_F_in_Agda_CHAPMAN_DOA14062019_AFV.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2176683$93FB4B87-F7A8-4021-98A8-8F4F9C562608","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2176683$115BD439-60D7-4D0B-821B-6D7C82270B9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2176683$11B0A8DC-8A22-4A1B-BFC4-81B15755E358","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c5e85568640e0e830640b6b7230cc9e592c5eee4","datavalue":{"value":"7196587","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2176683$58E553C2-9C53-4F3D-9958-7821CBD4397F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2176683$CB8EB883-3B2B-492A-B2A0-B41A436CF98E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2176683$562598AA-46DB-4090-90ED-4B7CE6746104","rank":"normal"},{"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":"Q2176683$4FD35176-15CB-4C4D-966D-8AD7F4842404","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":"Q2176683$E894C40C-23C8-4885-B8E0-33596DC6B187","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":"Q2176683$EB678D59-AAB5-4600-959F-39353916B647","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"63d59bd6ad3b2b55008efcb824b0b4d1cea7b5b0","datavalue":{"value":"W2980703959","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2176683$C88A1F16-D8F0-4D6E-9A77-D62D611DF540","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"242cf683288af100827015f68ac43b1efdb86b09","datavalue":{"value":{"entity-type":"item","numeric-id":5096247,"id":"Q5096247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f9b78eab308cb8335b7ef2cdf55a9c9213738c3","datavalue":{"value":{"amount":"+0.7725265026092529","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":"Q2176683$147F94F1-1A20-47EC-8BB6-A37256C5C1B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b335a567ef190b5b842d362f8ad5bab2ea8f33f","datavalue":{"value":{"entity-type":"item","numeric-id":5300891,"id":"Q5300891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f5d4c8cee21f3168f9053da92d9f21ee986b87a","datavalue":{"value":{"amount":"+0.7594008445739746","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":"Q2176683$FE49A62E-0BFE-4AD6-A122-50A2FD5B056C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"572711cdf34838976e710fb939031862ffef574e","datavalue":{"value":{"entity-type":"item","numeric-id":2892742,"id":"Q2892742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"17edf2b9a87d0f4f8c90a730061e1f6cc2ec6333","datavalue":{"value":{"amount":"+0.743830680847168","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":"Q2176683$5F80BE04-26EC-4FB8-BDC1-F4CB5E22F548","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1bc84c98ecb8d20117ac3288cc27c98c898b554d","datavalue":{"value":{"entity-type":"item","numeric-id":1322473,"id":"Q1322473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa75d4607d888e507e95ea49a8e08bc84b68ac8f","datavalue":{"value":{"amount":"+0.7347354888916016","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":"Q2176683$75C74185-8014-4A21-9290-A378878F0116","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e71f7a6493a8dbc04e7dbf14f2f531038e9beeb7","datavalue":{"value":{"entity-type":"item","numeric-id":5111317,"id":"Q5111317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22c2ac4b2cecfa7b7f9104ea0fa7ed118da34783","datavalue":{"value":{"amount":"+0.7331342697143555","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":"Q2176683$A3F57A77-7CD7-4F11-BFEC-6496C263532E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"System F in Agda, for fun and profit","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/System_F_in_Agda,_for_fun_and_profit"}}}}}