{"entities":{"Q4993361":{"pageid":7022938,"ns":120,"title":"Item:Q4993361","lastrevid":54021887,"modified":"2026-01-26T02:51:27Z","type":"item","id":"Q4993361","labels":{"en":{"language":"en","value":"Cumulative inductive types in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7359425"}},"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":"Q4993361$91899371-389B-4122-AAF2-5A3C70D8018F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f03cff513be239a1cef81dd7e3f1fab6643f9d01","datavalue":{"value":"1462.68221","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993361$D7C3DB5F-E2A9-4873-BEA5-80326346FC04","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"52254dabb8af5997f12cdfe0722d50f0619c8ae0","datavalue":{"value":{"entity-type":"item","numeric-id":2787452,"id":"Q2787452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$F6B27ECF-767E-4CEB-BD32-FC2FC47C2A44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9414558f268ee594724569b856f23c96f190f01","datavalue":{"value":{"entity-type":"item","numeric-id":1791139,"id":"Q1791139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$F65BBE7A-627E-44F3-A807-3089DAD11E81","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"19226134edc7102663c447aa756e808a7a8d2948","datavalue":{"value":{"time":"+2021-06-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4993361$2F0908BC-D29E-4D9A-BCFD-BAE811A1D800","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993361$41990BBA-D07F-4656-BD2E-8B191EA8EF19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993361$C915E69C-A378-4775-8EC2-1B7C028AA41B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d03765def5164a3f63048c2e9691c5bd3fea0df2","datavalue":{"value":"7359425","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993361$028E5A1D-7098-4320-BAFD-FBE47F054177","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993361$8054E8C2-40BD-4DE9-96F9-3150B5CFD41C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993361$DDBCA3FA-4E04-499F-8215-B7A8AF290E8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1202fa4aaeffc809043c1d94983ad89396bca2","datavalue":{"value":"inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993361$C34521F2-E448-4E3A-A562-A643A2A95A49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb8ff27bbbd9959dc9d199dde836f711285242b5","datavalue":{"value":"universes","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993361$4284CF75-E5A3-40BD-932F-9BB3ECB10252","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"10f0e5c37150563d1954fc00c5345e0fa968dcb8","datavalue":{"value":"cumulativity","type":"string"},"datatype":"string"},"type":"statement","id":"Q4993361$7CE5E8E6-298E-4762-8473-5E156F500C5A","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":"Q4993361$95560D7C-988E-44D0-A6F0-FCD5B780B16F","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":"Q4993361$108099BD-0A7B-4263-9C86-1BC4DC93C715","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee1bd5723754d3f3766daaae49b37c3f6d620266","datavalue":{"value":{"entity-type":"item","numeric-id":4944846,"id":"Q4944846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$E7A7A5B4-92F6-42AE-862D-A8E49709F6EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b5b3e1d2709e0f5c17896cdfac83364e530049b","datavalue":{"value":{"entity-type":"item","numeric-id":4012883,"id":"Q4012883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$2617DE62-8AFB-4FB9-A808-401208F0DB77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d623a8e65d7930da0f4edbbd56cfd23f3252fedf","datavalue":{"value":{"entity-type":"item","numeric-id":3024841,"id":"Q3024841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$5A3291ED-FD5D-460F-ABB5-8FF59E788E4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8859bdb6b4bc274ef2c6f9c1117c4e5c707d7424","datavalue":{"value":{"entity-type":"item","numeric-id":3224695,"id":"Q3224695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$6C3739A4-0CC1-4E10-93C9-0A3BA5DF52C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"681f6b991823ef1eb2ae5a0dc4952d80f163b9df","datavalue":{"value":{"entity-type":"item","numeric-id":2844696,"id":"Q2844696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$9E03C813-5861-4262-BD5A-DADB9903CD61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca5666f921e01dd97435dae76a72d1660a28c596","datavalue":{"value":{"entity-type":"item","numeric-id":2879272,"id":"Q2879272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$94CE3E1F-0D53-448B-86D1-83264E1C1F6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d70582cce52cae0af3a214a6e235592df5ddb652","datavalue":{"value":{"entity-type":"item","numeric-id":2787453,"id":"Q2787453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$0F84BF26-86BC-45F8-9A83-C410B975A5E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75a0652190fa525f5db8636304489797fd33778f","datavalue":{"value":{"entity-type":"item","numeric-id":5369495,"id":"Q5369495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4993361$5B921A35-002A-4216-A71C-2175FE661259","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"401fad6a195de3ba4e75f22b0239a6fb23c95b11","datavalue":{"value":"https://hal.inria.fr/hal-01952037","type":"string"},"datatype":"url"},"type":"statement","id":"Q4993361$566B7147-A287-4589-B499-20A2AF8DA47D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b64519104b573e3234033705bb84be4835a5f86e","datavalue":{"value":"W2887005952","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993361$C2A2D1BF-5923-4C9B-AAF6-430F5F8934E4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e10c2cd7e1a5b32a32d8a016a778d68d1de7b40e","datavalue":{"value":{"text":"Cumulative Inductive Types in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4993361$0D7C0ADB-7533-4060-BEAC-1A8A238CE424","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"39b5f086e97087573f8488ccf9d8dfda4cd8d0c1","datavalue":{"value":"10.4230/LIPICS.FSCD.2018.29","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4993361$1A3A464B-4016-41B4-8EEC-36B1E0A4B3CD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00c839c0aa8470b2188f6dd55eb1a4a77f974e30","datavalue":{"value":{"entity-type":"item","numeric-id":2787453,"id":"Q2787453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a8774ace51562d388648090fbd57e0a3ab913e7","datavalue":{"value":{"amount":"+0.91434907913208","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":"Q4993361$6D5C9DDB-9109-4694-9170-A5C4BA233714","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04fe00dd16f83f29e78f1f29866c0bdd4cd88a8b","datavalue":{"value":{"entity-type":"item","numeric-id":4457447,"id":"Q4457447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d948d72f582d6fdf1e3acc9319127f2ba8b0678","datavalue":{"value":{"amount":"+0.7852134704589844","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":"Q4993361$84B6AAD7-02CE-4D3A-A7DB-8358B35AE22C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dea9de8d016a1d49557bfa69a14fa567679694d2","datavalue":{"value":{"entity-type":"item","numeric-id":2879272,"id":"Q2879272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e3e1d941f71af8fb8768edf7d8f966ee10b91d48","datavalue":{"value":{"amount":"+0.7744300961494446","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":"Q4993361$FB6E50EC-7E00-4349-A15A-7D26EBE2F31B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f0d7e5f8e13bcfad3b90deb880cccfde5e25fd42","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ff0622a9373207696f582fc1c1157c6e2977289","datavalue":{"value":{"amount":"+0.7738906741142273","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":"Q4993361$C6022A80-642D-442F-A615-133565E19A33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a502128cfa1431cb223d8c606c833ea6b2bbaa6","datavalue":{"value":{"entity-type":"item","numeric-id":1193601,"id":"Q1193601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78e33e37911c8e321838f43f4de794e9c3f50d71","datavalue":{"value":{"amount":"+0.7507087588310242","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":"Q4993361$7DDF2C23-7E73-4847-BA19-FD93E9D80025","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4993361","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4993361"}}}}}