{"entities":{"Q3075245":{"pageid":3085961,"ns":120,"title":"Item:Q3075245","lastrevid":86150000,"modified":"2026-06-03T15:39:11Z","type":"item","id":"Q3075245","labels":{"en":{"language":"en","value":"An introduction to programming and proving with dependent types in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5850141"}},"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":"Q3075245$274B894C-48EC-42DC-9B38-263F4C83C67A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3dc7cdf1242a0b8172b19e3dfe00452a244ef9c6","datavalue":{"value":"1211.68367","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075245$3C80789D-514B-4FBA-BDDE-794E8E04518B","rank":"normal"}],"P16":[{"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":"Q3075245$ADD5F768-716E-456D-87F4-0A8955C6AECA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"76c08091180089def748f7e20273d2f981bdee68","datavalue":{"value":{"time":"+2011-02-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":"Q3075245$71345E64-50D8-4498-ACB3-4E72B595040E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3d3fb0424e37b18f09899673c17fa542b71109b9","datavalue":{"value":"http://jfr.cib.unibo.it/article/view/1978","type":"string"},"datatype":"url"},"type":"statement","id":"Q3075245$E5BE8ECD-6BA2-4C3F-8B19-09A09ECCAD3E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075245$D19966C3-C4C0-4B5F-A75B-E6DE3034F908","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"809e8cf9c328896917a2a297260f5cd9d07de426","datavalue":{"value":"5850141","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3075245$46930919-76F7-4CF1-8A62-A43E22712325","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98456cd4cdf0db037b678749018452921ff9260b","datavalue":{"value":"Coq proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075245$B3B23822-CD42-49C1-9AC2-09A6F3458E9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075245$3E786A57-246A-4F88-BD2C-3E0B4632A474","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2b7890291191cf10c124ea03ee5d280f0e8f3007","datavalue":{"value":"programming with dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075245$BB46052D-90E0-4834-8D4D-D53C0C6F33B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q3075245$9099E5FE-3E68-42E6-921A-E71B769D7702","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":"Q3075245$3AF12882-8DBC-4ED5-ADEB-2AA6C6AE54FD","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":"Q3075245$76ADC63F-1F7A-413D-AE34-F859F717571C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1bf37c15e48fc38e72aa136040f068ea21e0838","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ef3e75032dd41f1c22a2c9465c6a35644607ca00","datavalue":{"value":{"amount":"+0.8533845543861389","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":"Q3075245$DAE6E2EC-4076-4A00-8D10-846699C7B679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24cdcf48e2229f3526631ece2a3e1a80cc930fcc","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0e2dad83dcd47dfffa956aa4498ba04cc4ce23f3","datavalue":{"value":{"amount":"+0.7967949509620667","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":"Q3075245$251BF72F-A78F-4BA9-B579-0A74A50E7BF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c8fc519c81890f963ff41e9abebedea516f59fd","datavalue":{"value":{"entity-type":"item","numeric-id":5371944,"id":"Q5371944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5c9fe64a1ff10523555b3dae6662cd5e5f65af9e","datavalue":{"value":{"amount":"+0.7823894023895264","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":"Q3075245$015DA07B-6D04-47F2-A911-BB85C18EF10C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bdd8eb245e282dec7a4076b897d6aaeb7848435c","datavalue":{"value":{"entity-type":"item","numeric-id":3543643,"id":"Q3543643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc87a8dc6deb32be585b0f7af6c85c95cf784cc3","datavalue":{"value":{"amount":"+0.7781417965888977","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":"Q3075245$D38DA95A-24EC-411F-B9B0-3555860B24AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fdc61f049f8d0b30109ea2633d86e084029eda8b","datavalue":{"value":{"entity-type":"item","numeric-id":2751370,"id":"Q2751370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"30ab6d5bd41fafb05cefd1c8a3c57b1d07c67a53","datavalue":{"value":{"amount":"+0.7692345976829529","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":"Q3075245$AE05EFBC-C400-4D08-A1DC-002F0925521B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An introduction to programming and proving with dependent types in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_introduction_to_programming_and_proving_with_dependent_types_in_Coq"}}}}}