{"entities":{"Q2881085":{"pageid":2891805,"ns":120,"title":"Item:Q2881085","lastrevid":58048617,"modified":"2026-04-03T14:39:52Z","type":"item","id":"Q2881085","labels":{"en":{"language":"en","value":"A bi-directional refinement algorithm for the calculus of (co)inductive constructions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6021335"}},"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":"Q2881085$85FB873C-E2A6-44E9-B576-8EE36181110E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"13e0c76e820bd0fe6c852f87c3375c961fb22c73","datavalue":{"value":"1238.68145","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881085$6CA97765-200C-4158-87B3-41423318C01C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4a2f7b09820d94d5adf02f5fcb855991963ab0a0","datavalue":{"value":"10.2168/LMCS-8(1:18)2012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881085$205EBEE6-E17B-4FAE-893F-190F4CCEFBA1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b7eb816b28b9c1f72e9b0af72e4651889c7844f4","datavalue":{"value":{"entity-type":"item","numeric-id":287278,"id":"Q287278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$63270579-D7B7-4EFC-8147-A3962FFD0358","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aec9839e6b2c451febe526ce547ea5fd11508ee1","datavalue":{"value":{"entity-type":"item","numeric-id":744985,"id":"Q744985"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$57EBA687-FE60-4B86-8652-F1C908C1FCDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6fcc0863f3310792433a26fbf0220fe6380173d","datavalue":{"value":{"entity-type":"item","numeric-id":651318,"id":"Q651318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$EF143DBE-EA7D-41B4-B902-8CE584474867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"99729ea5fbac2e397c47743039765083a0ae1bb2","datavalue":{"value":{"entity-type":"item","numeric-id":205581,"id":"Q205581"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$653C7D64-9C97-4D3C-9E0D-81E13E11ADDC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$B33D2A85-1869-4287-A4B2-5A1DBD0720D2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d567b51f320d6b206f1e246178a080db047a3948","datavalue":{"value":{"time":"+2012-04-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2881085$1CD0D9AC-D386-4D36-9F06-34A0B02D9347","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1f0bb5ab2e6e8842e52ea863b446b09de5223cc7","datavalue":{"value":"https://arxiv.org/abs/1202.4905","type":"string"},"datatype":"url"},"type":"statement","id":"Q2881085$649A7F08-C0C3-4F63-B0B4-C66DBD318902","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881085$EEC0FD77-339F-496C-8669-D0B1C9E7C351","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"562ec530b5dce3fc204867ce91b5577fdbd0af00","datavalue":{"value":"6021335","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2881085$20C7B8FF-03E0-43AB-8163-AB8C58F178F5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c32d69c0855622a02c400aece3f47ba20c3f85f5","datavalue":{"value":"refiner","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881085$B448983A-3FFC-444B-9AE3-EEF6BDFCFC6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"07672cd9efb7a614e96dc9a58bd5b5685cbf3a1d","datavalue":{"value":"type inference","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881085$C2C28807-35FC-4A22-8049-7C29519F049B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73f877e2f1bc95df5bf8181b9880837b7bf0c2ee","datavalue":{"value":"interactive theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881085$A4C21CBE-234C-4FC2-9B69-9E78E0233043","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ee22a16b68ff7690ced49d39b0f7a8a6db96b60","datavalue":{"value":"calculus of inductive constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881085$CD060383-C34F-4BEB-A0EA-E3A4C69B6652","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b754569439d4565c57a4f9b6e4332c4f725dd3a3","datavalue":{"value":"\\texttt{Matita}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2881085$1279C522-2B2E-46B5-8098-342AB6414DB0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$5E82F39C-A940-45FB-B64A-CD924359F932","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":"Q2881085$83B66CF7-F4EA-4EE2-8D6A-CDE1CC0C1783","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2881085$66A16DBA-0DE7-4E1B-ACC0-52F62A7AAA1F","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":"Q2881085$B0CA6034-CADD-4B41-8A7A-8303D33791A8","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":"Q2881085$BFF043C7-4D99-4F66-AD1D-A46E337A213B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59baa381efe4724adbbe4deab319051b5344b208","datavalue":{"value":{"entity-type":"item","numeric-id":6099615,"id":"Q6099615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0584344212436bc5a9dfe1b4f10508ab3bc2d01","datavalue":{"value":{"amount":"+0.88711673","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":"Q2881085$7D860ED1-127C-40FC-8FBD-5958C7AE178A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6bcd34bb498d5a7074a2853aad6cd506d979d0dd","datavalue":{"value":{"entity-type":"item","numeric-id":3024916,"id":"Q3024916"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"215600ec9f22314d586dee04a3ba615134e8bfca","datavalue":{"value":{"amount":"+0.8803381","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":"Q2881085$65D06AE6-0647-4553-A142-2C99B1AA027B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd6d437810c57cc5debbc20171e5f9d59bdb9772","datavalue":{"value":{"entity-type":"item","numeric-id":1040007,"id":"Q1040007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"93357f5637e99605813263e629f771c8a3cbb188","datavalue":{"value":{"amount":"+0.87924564","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":"Q2881085$6044E36C-1F9F-429C-B646-EB6A9CF69EFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09a2b8953a21c0cfed364d884d74f23c033c1f66","datavalue":{"value":{"entity-type":"item","numeric-id":2866803,"id":"Q2866803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"65e9c3752bcf2b9ea94a02a5b70d2fbfb794a540","datavalue":{"value":{"amount":"+0.87705904","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":"Q2881085$A87F06F1-235B-41EB-A3E0-7BD31C298213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10cecb197cba373237d74ec245fe75d5b1a83f2d","datavalue":{"value":{"entity-type":"item","numeric-id":2914734,"id":"Q2914734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82d3fae3b9a49f307bbb8192b10df45a943e4286","datavalue":{"value":{"amount":"+0.8715647","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":"Q2881085$3EC87E33-473C-4D34-BB98-C27454D172A6","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":"4925a939408cd5fef093833b1e72f9e3909a6047","datavalue":{"value":{"amount":"+0.8711987","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":"Q2881085$40059FF0-4870-4108-AFC3-3842B9AF8145","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"387cce94216297b66f69d2aa4feef49d02d8cfd3","datavalue":{"value":{"entity-type":"item","numeric-id":4681362,"id":"Q4681362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4925a939408cd5fef093833b1e72f9e3909a6047","datavalue":{"value":{"amount":"+0.8711987","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":"Q2881085$3BEF452B-976D-41C3-BDF1-BFC160511FBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7e4e5f69ac10da5dfbf809d1b24702f6902e7150","datavalue":{"value":{"entity-type":"item","numeric-id":5747669,"id":"Q5747669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5213c47480b42536e43471b8db3552afaa1d15e","datavalue":{"value":{"amount":"+0.86808664","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":"Q2881085$153160BB-3F5F-45F4-9845-B6D694944948","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"75ee5105ce557480702c4228fc94eceba0497db4","datavalue":{"value":{"entity-type":"item","numeric-id":1111362,"id":"Q1111362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f02777c82876cca85117067d6337657805edab3","datavalue":{"value":{"amount":"+0.8654169","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":"Q2881085$6794F427-F0CB-4B91-8EC8-6EA032EB7B79","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1eb89ff33901fda21a6df8cb4fb4e8aec158f2a9","datavalue":{"value":{"text":"A bi-directional refinement algorithm for the calculus of (co)inductive constructions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2881085$8B438B71-8FEC-48DE-A999-03D9B3E0ECB3","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2881085","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2881085"}}}}}