{"entities":{"Q1012129":{"pageid":1013977,"ns":120,"title":"Item:Q1012129","lastrevid":50632733,"modified":"2026-01-14T15:26:16Z","type":"item","id":"Q1012129","labels":{"en":{"language":"en","value":"Coinductive big-step operational semantics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5543809"}},"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":"Q1012129$ECC2033A-8F4F-461C-AE75-8785742188AE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"67bb8667471a101ea893fa27a7c3af4d7204035d","datavalue":{"value":{"text":"Coinductive big-step operational semantics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1012129$6C02B426-A187-465D-9753-7B148849771A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ab825c4409e9a6a50a45f739a3ab0bb96af5698b","datavalue":{"value":"1165.68044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1012129$7827A29E-431F-4284-9513-4965B9166BD0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4b1e35c1c4bff0a8e8e775e8600e2e952b118ae","datavalue":{"value":{"entity-type":"item","numeric-id":848738,"id":"Q848738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$164585F0-0427-41F1-A5A0-A93841010928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a40248fad80fa4ad96948500440bd77ae86db171","datavalue":{"value":{"entity-type":"item","numeric-id":1012128,"id":"Q1012128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$62285930-48A3-4751-BA6B-C70CA1E04F78","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$07A2C40A-2861-452D-A48E-70C79C1F4E40","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"a70e3fb7efc077ae8b5215707528be5246c293fd","datavalue":{"value":{"time":"+2009-04-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1012129$8930CB1F-5366-4A79-9179-D9F322D12709","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1012129$0E99DF8C-B660-4AFA-8E1B-1B95C12BAC89","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5755c152c2393340873216106f076e5a38ddc2fc","datavalue":{"value":"5543809","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1012129$20CB579F-122D-44D1-A7CE-234D60D0C458","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fafcf953018573f92a433319a1c11197d7661331","datavalue":{"value":"coinduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$3F622D62-12A3-4AFD-B5DB-CEEB73DEBDB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d15a5b88457b15e43f49d0900c124a1c1adc72df","datavalue":{"value":"operational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$6CEACFB6-1965-4591-BCF5-EC0D98E93E99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7faeb5d0135023e1eb500475334c837141ddc600","datavalue":{"value":"big-step semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$E22DDDCD-E06D-48A1-8FD2-436F76171CE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6e064560fc1e96295608eaef7e624b550d9ed81","datavalue":{"value":"natural semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$EF969569-5825-4209-81F4-1FE87DFA9E6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6e0844ef240e4441240d555db59921800e44368","datavalue":{"value":"small-step semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$BB2C9ABC-8263-4DBA-A4B3-AAC90F69EA5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0d4b32c3545e15184907a7757d0ac00169973cf5","datavalue":{"value":"reduction semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$1CCE24FF-4C64-4780-916B-97FDB67EB14E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb0a5068a4946316d3ae87a58ec5f376a10a19f0","datavalue":{"value":"type soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$DB6C38D1-EE80-459A-B18C-D0D58AB70144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2d958ef02bdf074a60d670471cc677567c94c4a3","datavalue":{"value":"compiler correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$0CAFE526-04CE-41E7-BFCB-7654171331D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dc51f01424a0e99c13f7faf4f8814ddb154b736","datavalue":{"value":"mechanized proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$8E6E7446-338F-44DB-9679-305D440CECDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c2d2a1a08df66fe5c39138de0b82bec648e2dc9","datavalue":{"value":"the Coq proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q1012129$BF0EDD06-45F7-4982-885C-112677ABE87A","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":"Q1012129$47B379C0-A34C-4A55-BA44-432B1E2C51AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4feaea7961d9cfdcd7e2968b41cc11ecb0c87f44","datavalue":{"value":{"entity-type":"item","numeric-id":21716,"id":"Q21716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$18DC2AF7-64EC-4355-B909-C2B36F494970","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":"Q1012129$B4100E40-EEEF-4708-B66F-8A8DE122C4A9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c3f0c68c1c545974a1ed0c9f35590c01c461b436","datavalue":{"value":"https://doi.org/10.1016/j.ic.2007.12.004","type":"string"},"datatype":"url"},"type":"statement","id":"Q1012129$FE97F5C1-432A-4B40-9D09-5DF47E186762","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b597a4a7f56b8519333728313cb1e2f3c5cd9258","datavalue":{"value":"W1982866418","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1012129$F272EF2A-E0BC-46EB-8878-5AA6709B7A35","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"573c6c41ed26aa070e75225c6352a26e064dd624","datavalue":{"value":{"entity-type":"item","numeric-id":3774923,"id":"Q3774923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$ABB27CB5-6B9E-4CD4-BAEA-C137AC75D7D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66d102eeedc0eb3199ce5808a637283d2af0ab5d","datavalue":{"value":{"entity-type":"item","numeric-id":1878719,"id":"Q1878719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$D0E462A2-9DDE-41A6-915F-03751FD1A4A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f77790f3de0e7a5198a8f1c64a8023dd2bee09","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$599E5AC9-2385-4310-8BE7-08A670C51A50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8acbc35a8cddd0d4b3e090c62de84c098dad3c37","datavalue":{"value":{"entity-type":"item","numeric-id":4236754,"id":"Q4236754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$1AC187F1-971C-4502-A73F-83F7E12D5BA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$F8BD7545-96EE-4A82-960C-1E7DF8AA32F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acc1f3fbb4fbad3f8876f0ad83aae7b512e54cfa","datavalue":{"value":{"entity-type":"item","numeric-id":1177158,"id":"Q1177158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$B8150DC2-F03C-4B78-975D-56DAE8859B5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1cc8600e335c4acb5a5e79706ce4f0fb2de7299","datavalue":{"value":{"entity-type":"item","numeric-id":4709841,"id":"Q4709841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$B068573F-44D6-4231-AEC8-7C87D61CB8C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e320d5ab20d9378e83c08a862b63bf2725892d4a","datavalue":{"value":{"entity-type":"item","numeric-id":2653567,"id":"Q2653567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$E52BF4EC-A4A8-43E2-9BF2-454764CEEE99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b16ad904f76e6f0cc6057e01088da66a8b30e916","datavalue":{"value":{"entity-type":"item","numeric-id":4192947,"id":"Q4192947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$D320696C-A658-40AD-BD1B-7E7EEDC65C06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9901a00b49868594909cfecc127baac906dcdfd9","datavalue":{"value":{"entity-type":"item","numeric-id":5449611,"id":"Q5449611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$FB45099C-FA72-4B41-87BE-292922E402ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"882c8be91e9dd6a679904905a7a40337caaa7a1b","datavalue":{"value":{"entity-type":"item","numeric-id":1341754,"id":"Q1341754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$A13456C0-7F8D-4519-B220-72116F58FBC6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e387d9ec8ebd28bf4345fa4a7e714b612041f4c","datavalue":{"value":{"entity-type":"item","numeric-id":5482279,"id":"Q5482279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$3CB9EC5D-05D2-44D7-BD72-35FD49C57298","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87f7bcfffc49742b219cd84a695191ca8beef7cd","datavalue":{"value":{"entity-type":"item","numeric-id":5734774,"id":"Q5734774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$A60E495E-1C8A-4BA2-8C1E-FCB03E11D2B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e0bc180311b57c62eeb872b6b44fa7298188cae","datavalue":{"value":{"entity-type":"item","numeric-id":1097043,"id":"Q1097043"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$650A3C9A-AFA7-41D2-8CD9-911CAAEF058D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6473cef3ce337243e0f2ba4aef7103911e4b3591","datavalue":{"value":{"entity-type":"item","numeric-id":5704032,"id":"Q5704032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$2073C665-369F-48B3-94DE-BF22355E3322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3e199d7d938ae880ab0718461b42c95bead819c","datavalue":{"value":{"entity-type":"item","numeric-id":2871828,"id":"Q2871828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$950824EE-A14A-4756-B070-0744B97FC8CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"232426b4a336ce9f56636b166cfd296a7cb0f2d0","datavalue":{"value":{"entity-type":"item","numeric-id":4225152,"id":"Q4225152"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$145EDC67-B22D-417F-A774-63827596C07A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c2fea1c1f3bbaa5cfdd6d15172b810d0b5c9f01","datavalue":{"value":{"entity-type":"item","numeric-id":1318702,"id":"Q1318702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$E1D9A125-EDB5-4BE5-BDC9-BDE649BE0366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e1a5e7f94427d670644e085b2be0d1c199024796","datavalue":{"value":{"entity-type":"item","numeric-id":1392145,"id":"Q1392145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$B984DA0C-56B1-4B7F-BA65-A0A45A46338A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58b992789dc6a373764c584611377191d36e19f1","datavalue":{"value":{"entity-type":"item","numeric-id":1275621,"id":"Q1275621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1012129$3BEFE38E-7ABE-4682-ADA1-4267A8FE671C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"85c29cbc0da57a66b7ca37bcdf602e451aa48d41","datavalue":{"value":"10.1016/J.IC.2007.12.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1012129$550DF450-0646-4329-B1A2-549453AEFC8E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"63151ed46874ccece56eaacc3e40d1bbdc8a366d","datavalue":{"value":{"entity-type":"item","numeric-id":5899008,"id":"Q5899008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4e13c295d13cc0fcdb2be2359fd6f0caea4b5dc","datavalue":{"value":{"amount":"+0.9698588848114014","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":"Q1012129$99A9B768-BE37-4324-96D9-F98099A82A03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f11d2cc288a3be67e5555c897fd4877436ce85a","datavalue":{"value":{"entity-type":"item","numeric-id":3183540,"id":"Q3183540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cf3a7540da5570906c95870c2d8133d9df06bc72","datavalue":{"value":{"amount":"+0.8062071800231934","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":"Q1012129$8EADD2D0-9A45-49C0-ABDE-8E4C0A31C035","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f51d1f32e7941ce3a983b025e8fc6ea29cc9d5b3","datavalue":{"value":{"entity-type":"item","numeric-id":4963901,"id":"Q4963901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"344b56ac81a88360c16c822aa43d27547ffcf6fe","datavalue":{"value":{"amount":"+0.7873305678367615","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":"Q1012129$37749F81-D785-4BBE-8AD1-86F6804242EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4049e7cc6a821dac13d7ec0fd4eb1d29e360b5f9","datavalue":{"value":{"entity-type":"item","numeric-id":1012127,"id":"Q1012127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b83438fed4e2a2123bc69cee20e97338d944ab93","datavalue":{"value":{"amount":"+0.7536155581474304","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":"Q1012129$E58BFB79-30A4-4156-AED1-09388525CCFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f93f9fa52e38d89d72b9582c53c30d550d6e7375","datavalue":{"value":{"entity-type":"item","numeric-id":2871828,"id":"Q2871828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61b3f852efac95f29c68146846e2c072fc558497","datavalue":{"value":{"amount":"+0.749890923500061","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":"Q1012129$AF680AAC-0169-4CBC-B9FA-C1C1E3FD13EA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1012129","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1012129"}}}}}