{"entities":{"Q5327346":{"pageid":7356920,"ns":120,"title":"Item:Q5327346","lastrevid":51794033,"modified":"2026-01-20T01:59:35Z","type":"item","id":"Q5327346","labels":{"en":{"language":"en","value":"Pragmatic quotient types in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6196166"}},"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":"Q5327346$4576D9D7-A80C-443F-906D-75A3C33A08FF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"701c08e331ebeb001f944186e5e3f6f7603e1ef6","datavalue":{"value":{"text":"Pragmatic Quotient Types in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5327346$96B5B50C-9CF2-43DC-A549-5515D1910B17","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7833ffc68302887a1a255a72a7a388b96e952806","datavalue":{"value":"1317.68207","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327346$9EBF9972-613A-4389-B5EA-9D888EC0C8AF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a09655a68af28dcc2ab8e576fedc6476493e1575","datavalue":{"value":"10.1007/978-3-642-39634-2_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327346$0D91C29D-B1E5-4EDD-9886-0EB37BFCFE44","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"110c9b9e0e852b5bffe2fcd42275bf67a9f49ee7","datavalue":{"value":{"entity-type":"item","numeric-id":375195,"id":"Q375195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5327346$11590221-F9E9-45F8-8AAC-F36F9F4EF2EA","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":"Q5327346$02D80BC2-2387-4F32-8123-F65DEC311170","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"00eca6587536a1681b3f41d63f34e248b2e37166","datavalue":{"value":{"time":"+2013-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5327346$EF839470-38A8-48E3-BB60-5E39DE63C948","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5ce9bbf6c530eeae5372a189f691fd2f8ef98a3f","datavalue":{"value":"https://hal.inria.fr/hal-01966714/file/main.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5327346$7DCF2801-0D87-49C1-B4E4-D086E7008DE8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327346$11C29C4C-4BCA-4028-9025-F14EFCB40DE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327346$ED1DB8BB-785E-42A4-BFA5-478E5511A5EA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8d7921b48cdafc1a3b103fccb44a74ea36be88b5","datavalue":{"value":"6196166","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327346$A3E97AA7-ED0C-45DA-923F-6B6183BA9BBB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8f4279fb8c3183f0411f8d67db2d74e3d3f5f235","datavalue":{"value":"quotient types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5327346$6AB37008-18B6-4343-91F6-A96BCF82D123","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5327346$DDF4A2E6-8A0B-4B48-9C38-00EAAF142D7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5327346$59B5588F-4FE9-4E79-ABE9-961FB65655F5","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":"Q5327346$1A7A8B30-696F-4D6F-91DF-1B712FCE2256","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":"Q5327346$08701D09-5F1E-4B1B-822F-4CF8D6DF09BB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3722cc20823e3f939483aa9fd7188c3ad354319e","datavalue":{"value":"W25515096","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5327346$0346E84B-F8CB-4381-A8A5-EE74A809B9B2","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f01325a2d6096e882a8190f8ecbd6a21ce18c70b","datavalue":{"value":{"entity-type":"item","numeric-id":4435464,"id":"Q4435464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"719d12fc2c0e055b5da8a6990107a07c6dc797ef","datavalue":{"value":{"amount":"+0.796236515045166","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":"Q5327346$343FDA06-0320-4B7F-8C40-475111595B23","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":"d78413cf3b81911b9a8c0f9243179d3b11643f8b","datavalue":{"value":{"amount":"+0.7720065116882324","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":"Q5327346$F6B39985-A49F-4263-A139-86747968131E","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":"817b0ef70b7b61b5a18ecf5b6953131963cf62a4","datavalue":{"value":{"amount":"+0.7348445057868958","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":"Q5327346$5BD6A549-A3DD-4785-BED8-27863EAFEE42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7e4383c2ecd4e64a678e674cd670b84f21f373f","datavalue":{"value":{"entity-type":"item","numeric-id":4484345,"id":"Q4484345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8095106d20f01b077e16ab36d51085e80eb9af96","datavalue":{"value":{"amount":"+0.7302942872047424","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":"Q5327346$C002F8B4-0DCD-47A6-903A-538DD58578A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80eee57571fdbb56a12fbb8fc8ab44a57cfd5c63","datavalue":{"value":{"entity-type":"item","numeric-id":5094144,"id":"Q5094144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2d8982cfc3ece42d9ad63b0c012e71a531cff34c","datavalue":{"value":{"amount":"+0.7295486330986023","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":"Q5327346$CD6B8C19-F9F9-4F34-B01E-9DA521733FD9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5327346","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5327346"}}}}}