{"entities":{"Q656862":{"pageid":658711,"ns":120,"title":"Item:Q656862","lastrevid":63374067,"modified":"2026-04-11T12:25:56Z","type":"item","id":"Q656862","labels":{"en":{"language":"en","value":"A lean specification for gadts: System F with first-class equality proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5997563"}},"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":"Q656862$10F65755-3CC8-4EA6-BB07-A42D2B2483CD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"eb32484295cbe65f306f96e995d3206c23d785e6","datavalue":{"value":{"text":"A lean specification for gadts: System F with first-class equality proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q656862$6463E670-3FF7-4E1B-8036-0B187C188485","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9e240bf6c762b5dd74b1e7894f1852ddea596dc5","datavalue":{"value":"1232.68029","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q656862$CB4AAABD-8694-40E8-B497-BF072A0D21C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"db5aa7cc4b8fd2839e737fdcc792cc64666fb7f7","datavalue":{"value":{"entity-type":"item","numeric-id":656859,"id":"Q656859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$79C603D0-B40C-42C6-A18A-C59D5D28A3B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"69fbb24d628e902b0e408ad25e241e06fc8d6a4c","datavalue":{"value":{"entity-type":"item","numeric-id":656860,"id":"Q656860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$AC40DDA8-FDB1-4634-8520-6B2D8F71F046","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"76ed1cc0004eb02824a2ad25329a43a7aa0ffded","datavalue":{"value":{"entity-type":"item","numeric-id":656861,"id":"Q656861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$F19FB7CC-BD6B-4C6F-AB22-797DE5FC5BFD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"64a3a07e604cd8e480c16efc452d3568f025ae86","datavalue":{"value":{"entity-type":"item","numeric-id":162338,"id":"Q162338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$3CC2DA65-A81E-4E03-86D9-206063EB194C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"838e4cd92c3bfbf203f9466fab8ca1f8d1cd6888","datavalue":{"value":{"time":"+2012-01-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":"Q656862$EED21E26-C16A-4562-A134-3CE336D3BC77","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q656862$A23080EE-DB6C-4DD1-B9BC-292A29AB0154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q656862$1DFA719C-F799-4D9C-A5C9-16DFF783FF47","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a497a2d08217f36ac0867d12069846dbab9ded4f","datavalue":{"value":"5997563","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q656862$2E563F92-E68A-4402-852A-02A5ACFDD654","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92b4edef10612b66f6eed634fbf58b8a7ba51304","datavalue":{"value":"type system","type":"string"},"datatype":"string"},"type":"statement","id":"Q656862$6D8C6EBC-6246-4E11-9883-C710BAAAF219","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"601cfe43b9c2cb795a7d4f7ea9013bfb423f6057","datavalue":{"value":"GADT","type":"string"},"datatype":"string"},"type":"statement","id":"Q656862$4571C69B-1896-4AB8-9BFC-314EE8AE28D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"826cb17a61389397478ca005848e294acb35a0eb","datavalue":{"value":"system F","type":"string"},"datatype":"string"},"type":"statement","id":"Q656862$20003A15-B2A8-4959-8366-C364F6521C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"43cf81de9bccbd7e9d1df0d754d812c2513e7f57","datavalue":{"value":"equality proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q656862$C867570C-DCEA-44A7-8BEB-D30F670BFC35","rank":"normal"}],"P1463":[{"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":"Q656862$57EAA226-4B48-43DA-BE52-A6A76C844379","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":"Q656862$65DFD5BC-7F25-40E5-A7C5-2285107979A5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"63a31a8a720a0abcb0706f1fa8854a7403b79f80","datavalue":{"value":"https://doi.org/10.1007/s10990-011-9065-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q656862$88BE2F91-1B72-4B7E-90C8-BA5A88FC60C8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"cf3042fe21167811b1468b352fe3b48cb5ce59a2","datavalue":{"value":"W2082517951","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q656862$6597EB2F-637E-4ADB-B909-87D932FF7B73","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c1a6758d7f61b1629da4e25cec4c71e0709c1d3","datavalue":{"value":{"entity-type":"item","numeric-id":2949202,"id":"Q2949202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$E178CBA9-2852-4C22-BE5E-CAE06983C1EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c99a3dba522b2b909702ef9674cf3e56e922599","datavalue":{"value":{"entity-type":"item","numeric-id":3649135,"id":"Q3649135"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$EF8CC5C4-1C16-4614-9DA3-2518787660A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"667244bbb64cbeae656c8710018670875f6b25da","datavalue":{"value":{"entity-type":"item","numeric-id":4764616,"id":"Q4764616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$CE3F25D8-76D3-47AA-8124-ECE5AFBB8D92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7910c3c1fcb2b0e85336cf11117807f90b06f21f","datavalue":{"value":{"entity-type":"item","numeric-id":5348926,"id":"Q5348926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$3FCEC1C1-B0D4-4036-A66D-9B166F12FC8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56e8f349b9d040399464f58e77fd5e3e98ad4608","datavalue":{"value":{"entity-type":"item","numeric-id":2936831,"id":"Q2936831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$8F561200-FFBB-44B6-9DE7-6D28022ADB79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60a441da9409ddffedf9bbe35244797e4a0e62ff","datavalue":{"value":{"entity-type":"item","numeric-id":5385585,"id":"Q5385585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$5CE3BE37-7EBA-4940-A255-B86A1A9F507B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e9fbdcfeca765d18f7d3b2cc70ef3d3dbbb4e8aa","datavalue":{"value":{"entity-type":"item","numeric-id":3434624,"id":"Q3434624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$1195DD39-864E-4733-A0A0-4FBD7CE6BD90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"419ff1969ffd0e11ef3eb49d0dfd1b9abfbe2482","datavalue":{"value":{"entity-type":"item","numeric-id":4332424,"id":"Q4332424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$95776BF7-CBE6-43E4-9128-1AEC2D91FA65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d081a3183fffc4fc614babec26bb3a44f947b76","datavalue":{"value":{"entity-type":"item","numeric-id":5501473,"id":"Q5501473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$ED96CAD3-B463-4583-8EB7-CC0607EA5741","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"da87916c671807ba24519483c706753f7aa2c914","datavalue":{"value":"10.1007/S10990-011-9065-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q656862$4A73A80B-3149-49AA-AD5A-0C97322734D2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7143b5e8110138b76ec32962aa3cfc3673612d9a","datavalue":{"value":{"entity-type":"item","numeric-id":3189848,"id":"Q3189848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4260769c87919a023f046330a49c05a41565315","datavalue":{"value":{"amount":"+0.7433602809906006","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":"Q656862$9ACF5751-232F-4877-93AD-8DCD7A3DA51F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f60eb72bfbd77468baad6ea1f60803db6da171","datavalue":{"value":{"entity-type":"item","numeric-id":2937793,"id":"Q2937793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3b170517314247435ce5549f501712de96021c4","datavalue":{"value":{"amount":"+0.7324967980384827","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":"Q656862$A1643263-6C25-4AAE-A37A-81174A903796","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"980807ce7a8f4a0fa49fa180b5c0c08d532a8d1c","datavalue":{"value":{"entity-type":"item","numeric-id":2936831,"id":"Q2936831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"23928646999e92e9bbe5c72d6c6f959a26380631","datavalue":{"value":{"amount":"+0.7259816527366638","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":"Q656862$24CBDFF2-1E37-4B2E-9230-7383427A96A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d654042debfe05ad206d8c9d05e83e0dead0622b","datavalue":{"value":{"entity-type":"item","numeric-id":2828286,"id":"Q2828286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a9d53330fbf8e72c8c862c1a67ed70de8845007","datavalue":{"value":{"amount":"+0.7199389934539795","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":"Q656862$5F36522B-C8A5-4BA5-925C-DCA57CBF00C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"61e398ef6d2636c88d65241e4ee8a5e94d56b9ff","datavalue":{"value":{"entity-type":"item","numeric-id":5326307,"id":"Q5326307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"453c06483b320be0f080ec19fd96745786fd2036","datavalue":{"value":{"amount":"+0.7158883810043335","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":"Q656862$7E0E1143-E226-46CE-981C-D4BCA999D1C6","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"bee1ddd2bb542a0e64ca96574e4fab1bba361385","datavalue":{"value":{"entity-type":"item","numeric-id":57074,"id":"Q57074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q656862$9C4D0DF1-7EC2-4D0D-A939-8C9B7E6482E9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A lean specification for gadts: System F with first-class equality proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_lean_specification_for_gadts:_System_F_with_first-class_equality_proofs"}}}}}