{"entities":{"Q4647576":{"pageid":6677157,"ns":120,"title":"Item:Q4647576","lastrevid":53321225,"modified":"2026-01-24T17:45:06Z","type":"item","id":"Q4647576","labels":{"en":{"language":"en","value":"An application of co-inductive types in Coq: verification of the alternating bit protocol"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7002050"}},"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":"Q4647576$82F1BC23-2B5D-4D66-9E2E-507B674B49A4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bff17dacad41f76adc4ad926a71e5e350971c32a","datavalue":{"value":{"text":"An application of co-inductive types in Coq: Verification of the alternating bit protocol","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647576$4B0BA338-A722-417F-86E5-9FC5C38A2230","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2d7a1aef7622d0399ab7afbe944925905b833bb1","datavalue":{"value":"1407.68435","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647576$5F9C60C1-5227-42B7-9027-ACA34C6B4DBD","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0253d05064612d505321d4681d7961c6b51eb7db","datavalue":{"value":"10.1007/3-540-61780-9_67","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647576$3B47FFAE-B3B3-4FEB-862A-461B77198D63","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$5855DF05-91D9-44D3-B285-C2CBADEEC1E2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-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":"Q4647576$602DDCEB-1FE7-4B71-9A77-360EB8CD39CF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647576$AB727EFB-CB54-4BBD-BEE0-53AF63D204A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647576$471C14A0-B3F8-4591-8498-B451694AD4C0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4acb480b247635b7e97acefdd8955b1a55c2b7e8","datavalue":{"value":"7002050","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647576$2DC875A0-1ED4-48AB-B42D-CD29392CA41A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7d55f58e4831d77db7a5c91bd18c574bc0f4b78","datavalue":{"value":"transition relation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647576$9E89F0C2-5492-4DB1-B111-2EF8859F2A4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f4a800b667c18214ff04425473d9ae2da328b894","datavalue":{"value":"recursive call","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647576$69DE06F5-4BD5-4FE6-BD72-32F26BA12465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"26ed17f0fa3b284d6eda2a0b6f59f94f851c6b48","datavalue":{"value":"elimination rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647576$60B8782D-673D-49D3-8122-CA69B6FD6728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed28ff65c7143ccab364c3b93115be1e84f3431a","datavalue":{"value":"inductive type","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647576$DA1AB805-0C17-4B1C-BBDF-8F54ED14BBD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1cfd20602a5575e2ca9cd7bc684bba55b948e1f2","datavalue":{"value":"broadcasting system","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647576$E47B41E5-6E28-4B88-B8BB-FFD79B9CAAE6","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":"Q4647576$7531345D-F6EC-4DF6-8DF7-A45F41C52CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05e19126d9e9907924a4600d0a5598afdc2c5f70","datavalue":{"value":{"entity-type":"item","numeric-id":20609,"id":"Q20609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$9382E0E9-8801-4CBF-ABF8-3A556E9F582D","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":"Q4647576$8716228F-8373-4505-B56A-DB65356DA0FD","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3390df9f1d7f721d0d55a7871e0281008e2acbc7","datavalue":{"value":"https://doi.org/10.1007/3-540-61780-9_67","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647576$256B2BF3-27C7-44B8-AD06-068A8093348D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7ba59cc375f4f9d17532de5e75fc73de0bb8bd36","datavalue":{"value":"W1480957705","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647576$CB263D29-865D-4A96-BFFD-068DC285BCA4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2edbd4db20ecbcbb1c315d5320a38ebf3acfa299","datavalue":{"value":{"entity-type":"item","numeric-id":3992552,"id":"Q3992552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$8DEC976E-4B27-4E5E-BE86-A79EA8F433CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05ea7e81c6de0065717c066fc903d6beef24bc1c","datavalue":{"value":{"entity-type":"item","numeric-id":4647573,"id":"Q4647573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$92496EDE-485C-4A28-B14B-F2ADF77245DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dffad437e017fdc15baf42ce447a323a98e8dfcf","datavalue":{"value":{"entity-type":"item","numeric-id":4133603,"id":"Q4133603"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$D4363B3B-5090-47ED-8E66-B81C8A401B23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f7e92412f6b79d84af77b11b1aebb79e0508b8","datavalue":{"value":{"entity-type":"item","numeric-id":4138147,"id":"Q4138147"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$4415DAAB-A6EA-4886-89EE-AC1CFC94A657","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647576$56CD1374-4425-4D3B-A977-4A35701CCBC0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01017b3d1c200749df743ffbc642572962518ffb","datavalue":{"value":{"entity-type":"item","numeric-id":1355748,"id":"Q1355748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"20ed52c0f0a34ed2f186e64d27777b1a6360e786","datavalue":{"value":{"amount":"+0.7447890639305115","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":"Q4647576$CE104EF4-B557-4241-9EFF-613E59CCB5FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3759b7d7dc516dbd11ddc44d79565c29c01c078","datavalue":{"value":{"entity-type":"item","numeric-id":1764432,"id":"Q1764432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"542887a7e048458539707e9ce81772718dd63cc5","datavalue":{"value":{"amount":"+0.7284479141235352","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":"Q4647576$2AFCC471-A0E0-4A3D-94BC-C43663617D4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea5ab6fce12ac3d4a28e92f06d387b18aea79387","datavalue":{"value":{"entity-type":"item","numeric-id":4312490,"id":"Q4312490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4b12c11cdfbca05b680f5c31bfa0ef76b837add","datavalue":{"value":{"amount":"+0.72104811668396","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":"Q4647576$F193E6F4-05FA-4B40-9E64-E25D90392EBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"058d0a25272db99d2dda9d0b9e29bc68206441dd","datavalue":{"value":{"entity-type":"item","numeric-id":5327356,"id":"Q5327356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ee4135a266e2076d437d59774005b7aeead874a8","datavalue":{"value":{"amount":"+0.7198719382286072","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":"Q4647576$6BC37F86-D8BC-4041-AF28-48CA77722D63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a9063ce4f8ee99742dba24e7a6d1df1ef75eacf","datavalue":{"value":{"entity-type":"item","numeric-id":3727367,"id":"Q3727367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"329b2c17e0c991d11b5e74652b0b45322d14a7a4","datavalue":{"value":{"amount":"+0.7164345383644104","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":"Q4647576$DAE536E0-F555-454F-9AE8-F22C5D3EAB52","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647576","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647576"}}}}}