{"entities":{"Q2333326":{"pageid":2344069,"ns":120,"title":"Item:Q2333326","lastrevid":71869029,"modified":"2026-04-14T01:04:44Z","type":"item","id":"Q2333326","labels":{"en":{"language":"en","value":"Mechanizing focused linear logic in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7128702"}},"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":"Q2333326$47429934-B2FF-4C8C-8EA7-478A2542281D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dc72ef53c2948063bb66e56b9947bdac17ba7949","datavalue":{"value":{"text":"Mechanizing focused linear logic in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2333326$5CA54ABA-3653-4F09-8C90-CE4786EACA62","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"142ef1548176804d6b3a89c61100e3bd9b65c3b7","datavalue":{"value":"1433.68586","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$46D41960-FB57-424D-8D1A-C0925C59AFC5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f7e4a266b8cc1845b54ce458d5c595f5e6be7904","datavalue":{"value":{"entity-type":"item","numeric-id":2229155,"id":"Q2229155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$C6E97B8A-773F-49E5-83CE-18B3CC93153C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a291a40249c385e5a5b67f84938ffed092fc031","datavalue":{"value":{"entity-type":"item","numeric-id":281157,"id":"Q281157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$B84772B8-0D26-4960-925B-4B76F51089E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"17cdb0f2ca16c9cd1883b12b5d361fd27847e033","datavalue":{"value":{"entity-type":"item","numeric-id":402113,"id":"Q402113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$74558EBD-959D-4901-B80A-E63E63466D29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4ef528bc8876184f9d4707e8d3f50dda4f6f700b","datavalue":{"value":{"entity-type":"item","numeric-id":281158,"id":"Q281158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$492897D8-C115-4572-84F6-55AB9629CBF6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"38a671beb2eece257f68ae67ea5951ace27cbec7","datavalue":{"value":{"time":"+2019-11-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2333326$617D5832-A524-4C39-BD4F-50229E5E4BEC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$C6357F3F-2332-4DEC-98E5-8522F0EF212E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$E3ED9FA6-8DD5-4926-8E6E-98AB614EA91B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$4642A95B-5BA3-424F-9926-8E0484425610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f73d157ce9374047ebf746e6996382fc4dfda34d","datavalue":{"value":"03F52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$D8F80C53-DBD1-41DF-A9D2-177157D846A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$FE04D109-BF67-454B-AD46-590F84F7289B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4f33740444c8daddabbb32e8526ffefe2c308736","datavalue":{"value":"7128702","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$BC371B76-AB87-4910-8DBD-F8B8ACC7ABF6","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7f688d80cd10dc9c0b004843c0674655ad59b2fb","datavalue":{"value":"linear logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333326$DEB370A4-06F9-4578-9095-80F8198F7C39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98f41781e04ce8b5a53d7eeddf045b92e5e84bfa","datavalue":{"value":"focusing","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333326$001C9EAF-2FB1-43D6-9BC2-52E60810A54F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333326$39C0521B-B9C4-493A-9673-DEDABBBA9FC8","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0ca68d9e60f39b64375620b23802b5755dae3004","datavalue":{"value":{"entity-type":"item","numeric-id":13181,"id":"Q13181"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$6B089420-8ABF-4B21-8BBA-48C7303BBFBE","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":"Q2333326$2A2E28E6-563E-4918-A0D5-8F85EEE05190","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":"Q2333326$841F6317-8C87-4259-A2FA-81EE575F2CC0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bc574518236a2cef49b8fb29f6e37c2636911079","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2018.10.014","type":"string"},"datatype":"url"},"type":"statement","id":"Q2333326$10C79150-E148-485B-A890-A7734505B4F8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3599a536b0056aeb50c4cad6126ec6154f803cb7","datavalue":{"value":"W2898966813","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$1706BC95-CFD0-45B7-B3A7-5868D2F4DC95","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"8ff44544bf75e8e9e80e74a441140213a9bfb919","datavalue":{"value":"Q113317501","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$6DD5AAD5-25C4-4024-B833-FF73C96C1CAF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"42bdbea0160e788f4fb95a24a8a29ffb0eadc069","datavalue":{"value":{"entity-type":"item","numeric-id":4018167,"id":"Q4018167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$9EBDB7A9-247F-4372-BD49-E041FEFAD228","rank":"normal"},{"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":"Q2333326$235ACCD4-F9B3-4A2E-9035-B21BE9E25E99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9aa68a56f1e6d920b4253e172f355c0c21d40c1a","datavalue":{"value":{"entity-type":"item","numeric-id":1744443,"id":"Q1744443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$7A6F2F71-3D60-44B5-8353-AAD41B9ADD6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"367ef177c9ab91da57ee385240218ffe15eeadc2","datavalue":{"value":{"entity-type":"item","numeric-id":5178760,"id":"Q5178760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$A46290B4-F649-4EB6-AB40-A9258C8B6347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66f272d7287f994bc6a285690f7059c71fa20c01","datavalue":{"value":{"entity-type":"item","numeric-id":4933310,"id":"Q4933310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$D913EE6F-6FEA-484D-A67B-465DCF778CEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e723c31e56f2487bba3b93f0d7637a4943535187","datavalue":{"value":{"entity-type":"item","numeric-id":3024831,"id":"Q3024831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$8A0A806E-A56F-4A26-B5C3-7038E2A7075F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc08fb401a97c65d0aa2e5b35738ed07413a3aa1","datavalue":{"value":{"entity-type":"item","numeric-id":1744445,"id":"Q1744445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$5F8A2AD8-3752-45B1-982F-A91977F03217","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ac95a97664ee433af6430c2c176331df8f4ba1b","datavalue":{"value":{"entity-type":"item","numeric-id":4649549,"id":"Q4649549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$26D3EF6E-EC23-4F31-9C97-CD7292D13E58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ea3d89d9caeecb4ce96d5251e582d3bc04e60e3","datavalue":{"value":{"entity-type":"item","numeric-id":438569,"id":"Q438569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$4BB940CF-C0EF-425D-8A14-12FFE283C6F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf284620825356e4026f7163726a6eaa28789317","datavalue":{"value":{"entity-type":"item","numeric-id":287277,"id":"Q287277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$FE605745-0E06-4353-BC1D-A5DD2993FFC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54351e142ba78301c80d7c3516f9734aa8ddee58","datavalue":{"value":{"entity-type":"item","numeric-id":3791120,"id":"Q3791120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$080DCE9C-383E-4823-8B50-B9FA27BDE413","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de22e68338ce91d5f7b421aaf2ecefb70507cdce","datavalue":{"value":{"entity-type":"item","numeric-id":1944778,"id":"Q1944778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$86B53925-C482-445E-8821-82077809617B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f16cf29a6be511b5490d0e9bb1ee22c0133e4fb4","datavalue":{"value":{"entity-type":"item","numeric-id":707742,"id":"Q707742"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$D0A90FCD-9085-4868-BC53-66D1C59F1428","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af86435b42405e3baf6ad114d46e4c9403be99f2","datavalue":{"value":{"entity-type":"item","numeric-id":2842123,"id":"Q2842123"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$0202F4C5-675E-434B-9264-38EC5C9C8F80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c5489b5a21e6a1d194eff456c59674a50c3ae17","datavalue":{"value":{"entity-type":"item","numeric-id":897936,"id":"Q897936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$517A5952-30DA-495D-8AFE-CF233347F9D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9dd741c8f779448cca2e557d9c65f69f1eb3195f","datavalue":{"value":{"entity-type":"item","numeric-id":1854335,"id":"Q1854335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$04321CF7-C357-414E-A270-8C5CB9CC2C85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2221baf7e4bab4cc38963939c795119dc4b2829","datavalue":{"value":{"entity-type":"item","numeric-id":2946730,"id":"Q2946730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$C22015D1-76EA-45EB-A95F-49BABA386C6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56327724d8101cacc3d4e5b36700dc86a7feb472","datavalue":{"value":{"entity-type":"item","numeric-id":4499084,"id":"Q4499084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333326$2C5FADB6-296F-445D-8363-7BAE5B9F8360","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3a18cace713ef122db56f787e9c037bb7791eb17","datavalue":{"value":"10.1016/J.ENTCS.2018.10.014","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333326$D7DFB156-1D6C-4AD3-B42D-5B97869935DD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b1a1b8742ad4b4fd8b08700fc7fa5c02d34775c","datavalue":{"value":{"entity-type":"item","numeric-id":4018167,"id":"Q4018167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2fa4827d46cfc05d9180eeb0d532bedf4177669e","datavalue":{"value":{"amount":"+0.8124310374259949","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":"Q2333326$5F5C76EE-5510-4F50-8E83-C9C70CF3D3D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a7ebe750efa17eec7129d8dc648916fa37660af","datavalue":{"value":{"entity-type":"item","numeric-id":5179015,"id":"Q5179015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2fa4827d46cfc05d9180eeb0d532bedf4177669e","datavalue":{"value":{"amount":"+0.8124310374259949","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":"Q2333326$813FE202-D24E-482A-84B9-1A4A3C7B5982","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e85076c70b4e18204bcee063ef0e4420ac7c9849","datavalue":{"value":{"entity-type":"item","numeric-id":3608427,"id":"Q3608427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a10a0e3cccee065c6bb1c1d88b082d1924ea7c4d","datavalue":{"value":{"amount":"+0.7915326952934265","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":"Q2333326$7AF512D9-0EA1-4719-BEFF-824BA0E53A7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1da6059d4684c2cae342107a04e61262ceec26fa","datavalue":{"value":{"entity-type":"item","numeric-id":4664255,"id":"Q4664255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"178e24c7d6a4c612adbe90eb2bfe73461d305be7","datavalue":{"value":{"amount":"+0.7870255708694458","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":"Q2333326$1E861934-79AD-419E-A35E-36A42B00AC73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e952094e2719c457cc65ccf17740b1c48f29693","datavalue":{"value":{"entity-type":"item","numeric-id":4412848,"id":"Q4412848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab1f5debc9dd628d3dbbde3be8e498ec8fd4c71e","datavalue":{"value":{"amount":"+0.7796651721000671","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":"Q2333326$5458B8D9-0CBC-4CFD-85D4-F1F76E9123EA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanizing focused linear logic in Coq","badges":[]}}}}}