{"entities":{"Q2879258":{"pageid":2889978,"ns":120,"title":"Item:Q2879258","lastrevid":58039695,"modified":"2026-04-03T13:48:28Z","type":"item","id":"Q2879258","labels":{"en":{"language":"en","value":"Experience implementing a performant category-theory library in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6341487"}},"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":"Q2879258$ED8F23EB-AC50-471B-B63E-892F27775100","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5d407f818783a8c26291ce20f406879431ec3686","datavalue":{"value":{"text":"Experience Implementing a Performant Category-Theory Library in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2879258$1D941D43-9C76-416F-821A-70430E5A4062","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3df712280596555c3ccbb8b289f89b873d60235d","datavalue":{"value":"1416.68163","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879258$DE71C5E4-3BBC-4372-98CB-21905ADD5DCB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"eb7708c48a1337ef2ef0ca549267621dae52c748","datavalue":{"value":"10.1007/978-3-319-08970-6_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879258$0A162642-AB1A-43EA-BDBA-8EBFCB9718C5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ed360e5a5b6485d0ec642ab4e5a8b7cc72636740","datavalue":{"value":{"entity-type":"item","numeric-id":1791168,"id":"Q1791168"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879258$0792B9D0-5FAE-4F2F-87F9-9759A7FD5734","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d957a3f31f9610e79e212a1ae2ae0004027dee9c","datavalue":{"value":{"entity-type":"item","numeric-id":1702890,"id":"Q1702890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879258$C3E62380-129A-4252-9B70-78E34EBEED2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0fbbf69258f6d48525479abc15deea1d10693da4","datavalue":{"value":{"entity-type":"item","numeric-id":618739,"id":"Q618739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879258$F7F14398-BF44-4324-9D38-EEF436BD25B8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879258$72DBD56D-3588-4311-85D7-F5E699BD2528","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"565bc5987614f46e32dc98add32d630fe2eeb533","datavalue":{"value":{"time":"+2014-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2879258$6F9BD430-697C-43E6-A4F7-4692603FC66A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e2332d4aa2b16447f66af3f94a84f1717c7c8f49","datavalue":{"value":"https://arxiv.org/abs/1401.7694","type":"string"},"datatype":"url"},"type":"statement","id":"Q2879258$510AD7D1-0636-4334-89D5-D75588F240E7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879258$D5083BA3-F736-4A3B-99B5-28AA4F14F3B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7f8ff1bc7135bb1a5f4ce6282771b53dfaffbb01","datavalue":{"value":"18-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879258$2C2D01DF-02EB-4B75-9417-89A1E411FFAC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3d5928d5cf34c58fc47d921c8f4c4f63b04d7ee2","datavalue":{"value":"6341487","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879258$746C7FA2-655E-47BC-A17A-E6EF142CE94E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2879258$417FAF23-285D-4207-AAF7-BA532EAFF93B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5685485f4c27abda29cd481c0486a1adb54b3a91","datavalue":{"value":"category theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2879258$692BF994-2001-477D-ADEA-C68E4FE44B58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4ecd2d433c9f863c39fe5a1fa2de24434b6de0d","datavalue":{"value":"homotopy type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2879258$46941F63-718D-4314-9AFA-C38B44A9DAF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d1ecf978a28e5d1baefdbd10dbc4f102a6158a13","datavalue":{"value":"duality","type":"string"},"datatype":"string"},"type":"statement","id":"Q2879258$E7D66FBC-8CD9-4864-B5E0-8ADB2BA94F6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"afee417564209b61e3e00baf8c5b26c09ce9029b","datavalue":{"value":"performance","type":"string"},"datatype":"string"},"type":"statement","id":"Q2879258$494173EC-F95C-422A-A868-DF0F8969833A","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":"Q2879258$03D3E92B-E840-4333-BFA6-C48CB37D4C4D","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":"Q2879258$A6960600-36E7-4C0E-ADB9-97E0338C8A00","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3a5ff7127119b4e28c1f71c088258127292f7a6c","datavalue":{"value":"W2181522451","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879258$1780E892-82FF-4CB5-9417-0B884143B9EA","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bfa89091fad97dbdb20c47dd603917c3a32a36f9","datavalue":{"value":{"entity-type":"item","numeric-id":5369495,"id":"Q5369495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ce66a55fc124e818ca6b4705e1bc566dcc5f660","datavalue":{"value":{"amount":"+0.8294665813446045","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":"Q2879258$A20F26B3-E93E-4776-9292-14527751DC8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f283ce1b7bb222e202a6acf28a6a844d9018de04","datavalue":{"value":{"entity-type":"item","numeric-id":5747673,"id":"Q5747673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a88d8babda0a9879531efab502550f76cd88cd72","datavalue":{"value":{"amount":"+0.7543133497238159","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":"Q2879258$B73DB70A-D932-45DC-9486-8E9D10C2DAE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae89b6fe2fcc9b6c72128a35539891e81f9d02a8","datavalue":{"value":{"entity-type":"item","numeric-id":6488555,"id":"Q6488555"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5abf8f16dbf29c5b5e951778695bc08e44ddaf43","datavalue":{"value":{"amount":"+0.740667998790741","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":"Q2879258$53859191-D711-4549-945D-F974089AA761","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00741d8653e7ff3ed03255de9dc4a5ba9833efb9","datavalue":{"value":{"entity-type":"item","numeric-id":3094177,"id":"Q3094177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c84e0f96ecfb6994edc992dd879829d7dba1e242","datavalue":{"value":{"amount":"+0.723871111869812","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":"Q2879258$79437313-B032-48DA-96FA-4F9E6B6841B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a7725344fd806c8bb0e8ce86201602686f3ebbe9","datavalue":{"value":{"entity-type":"item","numeric-id":2879252,"id":"Q2879252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d3bacd3637c96060fb47c0023a6b5d84366c78a0","datavalue":{"value":{"amount":"+0.7233871817588806","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":"Q2879258$F00F3B7D-337C-49C4-B44E-0F6FAEA32E4A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2879258","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2879258"}}}}}