{"entities":{"Q1267035":{"pageid":1277785,"ns":120,"title":"Item:Q1267035","lastrevid":70035552,"modified":"2026-04-13T12:00:06Z","type":"item","id":"Q1267035","labels":{"en":{"language":"en","value":"Verifying programs in the calculus of inductive constructions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1206843"}},"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":"Q1267035$77A48C1A-C137-40FC-B810-672EB838A9BC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8844b1e41b52729b30943fb6496a58e5dcc7d829","datavalue":{"value":{"text":"Verifying programs in the calculus of inductive constructions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1267035$A9695BEC-BF92-488F-8A91-21C32526344D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"935387d0bfb3db87b564d3377e62ad3c0c4fd0bd","datavalue":{"value":"0905.68092","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267035$8B55E824-0754-43B8-A96D-6D5716723AF0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7b7b6d6a07726cc796419216bb290a211ea3915f","datavalue":{"value":"10.1007/BF01211457","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267035$409A24FB-5C26-4A7B-9D06-A1B297831257","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7a43a26eb8132e63e90175dc572b52878204e34a","datavalue":{"value":{"entity-type":"item","numeric-id":1267034,"id":"Q1267034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$6D50D6E1-F98D-4A13-89DE-530FCBCC94A9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d9925518446645d219093152a820aba790417b61","datavalue":{"value":{"entity-type":"item","numeric-id":164203,"id":"Q164203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$6BC14AAA-E97F-4C6F-97DD-305A951D27B1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0fe267c563c8885d3725e93df6ade60a9cc5dc4b","datavalue":{"value":{"time":"+1998-10-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1267035$71EEC3C3-6FC8-4216-92CC-2F378A553FE6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267035$A5135F46-72C5-4DDC-BBDC-87206D484F5B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"91a7cd08ac3451aaa5f449fddd7324057aad4a1c","datavalue":{"value":"1206843","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267035$530C7735-2C75-46DB-BCF0-169D1B6BF9CC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5988cdfcbf1ce6e4802e928cc064e7f5a87bcfa5","datavalue":{"value":"functional programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1267035$FCFE3E91-8A25-4AC3-810F-2D889BF0DD48","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$FB6484F7-40BC-40DA-AD71-E78F83D2EBD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$96DF10F6-2D55-429B-A584-AB9652C3E9CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$BF81DC6B-09B6-4F02-A4A0-D8A7FDF789D2","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":"Q1267035$2E70A699-70B8-4330-B658-239CEC377C8C","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":"Q1267035$47B6AD30-554B-4C71-AD2D-881CA36E9055","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$064E8764-1B9A-4E32-8947-5A22BA10B499","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$692DB243-8E16-4951-AE3B-D485E67B51E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$DB315E7F-D3E5-4417-9173-82C72490EAAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab9b65cfb64d46fb3b8d3a90a31654248ac77d25","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$EFB4C0B4-8F32-448D-AD74-BB79D7A7E513","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ae5a24b84d8598cf63278ea844cb1aa9d0f8824","datavalue":{"value":{"entity-type":"item","numeric-id":4310027,"id":"Q4310027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1267035$2B9B9E8C-673D-4CA9-8FF0-409CDDB09066","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3ff67cd13712911dba8cbd6de3db0dddb42790f3","datavalue":{"value":"https://doi.org/10.1007/bf01211457","type":"string"},"datatype":"url"},"type":"statement","id":"Q1267035$D7C704B0-E247-43F1-BCDF-0D0C83332ED8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e19fdba3da7b3753a7530066c61d151813084042","datavalue":{"value":"W2038724494","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1267035$ADF40F19-8F5D-4C8E-A6BC-BCE3F259CCE5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab116f62a0b733ec0afd5e508aec01a388df675d","datavalue":{"value":{"entity-type":"item","numeric-id":3685173,"id":"Q3685173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9b7907b6e1d4df0c31ca2c9523af63fe6fdcdca","datavalue":{"value":{"amount":"+0.9410445","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$71EFD488-0B88-420C-BE14-A5F3563032C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45b8da30769ee0bf991601e0428f66c15b4fffec","datavalue":{"value":{"entity-type":"item","numeric-id":5278212,"id":"Q5278212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"11d353a82c2c34f5a500288f5a1b6cbaea27edbb","datavalue":{"value":{"amount":"+0.93006843","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$1B8A7311-5D45-40C7-B2C3-9657F278693A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49c0e4996fa4fa732707b33cff8f2c5c612917a0","datavalue":{"value":{"entity-type":"item","numeric-id":757077,"id":"Q757077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"983ced789c3446fe3b2b5168a426ebfff1a1290f","datavalue":{"value":{"amount":"+0.9230726","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$897D7AA6-2B42-413F-919C-B035DFB25AFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65783770f753a60e730e2f256403c2da900bb4d3","datavalue":{"value":{"entity-type":"item","numeric-id":3766816,"id":"Q3766816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9df529cf03b7604f23e295619d2f06939553a03b","datavalue":{"value":{"amount":"+0.916087","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$641E5D4B-EFAF-4E4E-8691-B2268D551D74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ea95e49f05526edb7368d843c6ed27a9c17b632","datavalue":{"value":{"entity-type":"item","numeric-id":4923522,"id":"Q4923522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a947051bccd5495fbc3d070af1e9acb465a34e2","datavalue":{"value":{"amount":"+0.91028136","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$53715209-8F0B-4C38-B55D-371E809036FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b9408453aa7df27a59323e790e1dd4ca591280e","datavalue":{"value":{"entity-type":"item","numeric-id":3783512,"id":"Q3783512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5fcfda3b6b7c57e88fa2b9cc4b00074ff03b30d","datavalue":{"value":{"amount":"+0.9095533","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$EC35BFB4-D8FC-4B84-BA6E-385AF87A13F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8266f2c8ef040bdae8a8d17dbab7410a4f0f3244","datavalue":{"value":{"entity-type":"item","numeric-id":4923368,"id":"Q4923368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91d4feb60b000c91aeb2ecc62f0b150467da20b8","datavalue":{"value":{"amount":"+0.9093379","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$8F2AB617-4477-4123-AA2D-8BB16A66BBA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5547e7f140f28686cbd763d65679684df419834d","datavalue":{"value":{"entity-type":"item","numeric-id":4551152,"id":"Q4551152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f352450f461ea35e7025e529a2b4531fde4e393d","datavalue":{"value":{"amount":"+0.90794814","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1267035$5F0BA47D-4124-4246-A5B1-DD705BD0A81F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Verifying programs in the calculus of inductive constructions","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Verifying_programs_in_the_calculus_of_inductive_constructions"}}}}}