{"entities":{"Q4645754":{"pageid":6675335,"ns":120,"title":"Item:Q4645754","lastrevid":53316794,"modified":"2026-01-24T17:30:51Z","type":"item","id":"Q4645754","labels":{"en":{"language":"en","value":"Coq without type casts: a complete proof of Coq Modulo Theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7000001"}},"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":"Q4645754$601A3538-2F63-4B09-A2CA-51EA1E4A946E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2c3ca637150b9215e118ac05c9bfee2f54cf100d","datavalue":{"value":{"text":"Coq without Type Casts: A Complete Proof of Coq Modulo Theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4645754$C8C66166-CC5B-4D4D-9241-B97C2E9C193A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a277482f2352c7224ac37ff0adc1f0945e3bf819","datavalue":{"value":"1403.68227","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645754$0C957DD4-942D-4980-9E7A-475ECC7314A0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1b1bfbcb4e8f5871a00d29a6022e3016b3479851","datavalue":{"value":{"entity-type":"item","numeric-id":235599,"id":"Q235599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645754$BE8E2EDB-F7BB-4BC2-A1CF-C3B48D1423AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1745bdeb092262739da6d0fd18a64d1c3c06446d","datavalue":{"value":{"entity-type":"item","numeric-id":2323969,"id":"Q2323969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645754$E5985811-6C85-48D6-AE50-7EADE9D40A17","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eae4601ff702bcaa610b94b3434abd8165930c5d","datavalue":{"value":{"entity-type":"item","numeric-id":4645721,"id":"Q4645721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645754$87CBFE00-2683-4B27-AB0A-2A6A38B7B601","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"412b474a973c0dfa7488c61fc45fdeec318e212e","datavalue":{"value":{"time":"+2019-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4645754$A0A3ACAD-F692-4336-977F-B326C0784205","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645754$4A592E58-11CE-46D4-8D11-D60A77829E32","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6d38eef5f84e82aeb7ef76a1cb9eb6e7aefdbccb","datavalue":{"value":"7000001","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645754$67BA54B7-6BA0-49C4-AF1C-71C009A66241","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645754$F8893223-ED7F-4DFD-8AD9-2AB858C79188","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"263805638d1e63a79a3c591e1ad14e8148fe9595","datavalue":{"value":"first-order theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645754$833AD704-F700-4036-A340-6AD45CE1E97C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645754$BD5BB614-0577-4257-B531-56127BB87188","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645754$4095018C-8A92-4207-83AD-F256BEF22AFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645754$BCADFCDA-CD18-4549-92D8-2B6B5303E421","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":"Q4645754$EA83AC84-D844-49F4-B5A3-460C262208D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"5a61edfee27b9a0d876bc3ac3487da750de8fe51","datavalue":{"value":{"entity-type":"item","numeric-id":30968,"id":"Q30968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645754$A64C76ED-288D-4C62-8C71-5E9A726C007C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8a38d0c3b215ef345f4b9f6556e53256642a6db2","datavalue":{"value":{"entity-type":"item","numeric-id":30969,"id":"Q30969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645754$51CAC5E5-C2B5-4AE3-A79F-6D4CF61B35DB","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":"Q4645754$76C624D4-B8E5-475B-A048-0595737ABF88","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"68b1a4881837ad5d04b26c9d7093c6fcd25bdf1c","datavalue":{"value":"https://doi.org/10.29007/bjpg","type":"string"},"datatype":"url"},"type":"statement","id":"Q4645754$C84263DC-ED72-47B1-9EEB-B8CDD7EF57A0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b6275be53c9705787d4eb0a4929e93721f6de5b4","datavalue":{"value":"W2739481936","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645754$8EA0CD28-1188-41DE-8E5E-9BD2F61F46FE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"18921cef6da14b0a64224ab20f1bb4970798be2f","datavalue":{"value":"10.29007/BJPG","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645754$B758CAAC-0077-444B-BD5A-75379CA77652","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a118a4ece8b2c99ea89a5fa8f825fe971e3d149e","datavalue":{"value":{"entity-type":"item","numeric-id":2958550,"id":"Q2958550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad60ea6fe85095d820f811b0b7a066206d977134","datavalue":{"value":{"amount":"+0.8784863948822021","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":"Q4645754$3E0CECD5-A49A-4AB8-ABB0-62EA1BA65D23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"210fc6ea1c74927f8cc30615348c9f5912fd19d2","datavalue":{"value":{"entity-type":"item","numeric-id":3586063,"id":"Q3586063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a27d7aba2fdd0cba69e15124d6596dd21b6182fe","datavalue":{"value":{"amount":"+0.8403854370117188","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":"Q4645754$B5491468-0307-4C93-8AF8-D5D303316689","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fb28a2fc25f31c29f2999deca4bd9cba21f958c7","datavalue":{"value":{"entity-type":"item","numeric-id":5394575,"id":"Q5394575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9263b13d1d1231598307257dd39d435ceab52b72","datavalue":{"value":{"amount":"+0.7596313953399658","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":"Q4645754$2E6C5136-A5AA-498E-BC5F-F008D771378F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9b4abdc9d1a3f44352b0bd6028169b366ab5c6d","datavalue":{"value":{"entity-type":"item","numeric-id":4623435,"id":"Q4623435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3306d4b388c04131cb18e8dec8d3067f21ee93b","datavalue":{"value":{"amount":"+0.7573139071464539","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":"Q4645754$82BAB7C6-8A40-459D-B416-FBFE34B4E223","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"918f2781deb536cb7abada9a9087642f80fd8cef","datavalue":{"value":{"entity-type":"item","numeric-id":4699295,"id":"Q4699295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e44c225e50304ca37e93d41c49d9dbc00ca47651","datavalue":{"value":{"amount":"+0.7497309446334839","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":"Q4645754$7EADB9E0-9B5F-423A-BF17-5E91B5FF6DAF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4645754","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4645754"}}}}}