{"entities":{"Q7361762":{"pageid":31520825,"ns":120,"title":"Item:Q7361762","lastrevid":105368918,"modified":"2026-10-07T13:37:39Z","type":"item","id":"Q7361762","labels":{"en":{"language":"en","value":"Isabelle/Circus"}},"descriptions":{"en":{"language":"en","value":"AFP entry Circus"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"297e467c576c7aea384acbc4c54c9ea8870b90e1","datavalue":{"value":"https://isa-afp.org/entries/Circus.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361762$B881A193-F7E5-4031-B854-525E44D8A32B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d7aa46a407435e78975f422998431677cd43fdcf","datavalue":{"value":{"time":"+2012-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361762$3611DC0C-D9DD-4621-9512-25C3ACD0D9C2","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"78d101a50e92266d533fd90602aef7ed09416f92","datavalue":{"value":"Abderrahmane Feliachi","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361762$8FE4536E-DD70-4B3C-A77C-853A4770F729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"9f417d50d28c3248f72294b3f5970214162e0fab","datavalue":{"value":"Burkhart Wolff","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361762$5EFB0ADE-FD38-4E6F-A81F-359D4F01D157","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3c12113446d9784fae563df157d536da6d3bebcd","datavalue":{"value":"Marie-Claude Gaudel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361762$43CA6D48-0BA7-42D5-A644-87213E1F7040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"e7790b9f43c65f254faf9a70608e17eb5346a140","datavalue":{"value":"Makarius Wenzel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361762$C546A836-935D-4314-A0F8-48153D4CE50D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b66164cb83e4436f0e4cf17b4c47e1f439cd7632","datavalue":{"value":{"text":"Isabelle/Circus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361762$49677434-9F1D-450F-8B6E-C3EDAE57A117","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fe084b1a16d46cde5f9a21a5ce8e7bf6d40c3006","datavalue":{"value":"The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's Unifying Theories of Programming (UTP). Isabelle/Circus is a formalization of the UTP and the Circus language in Isabelle/HOL. It contains proof rules and tactic support that allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). The Isabelle/Circus environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus. This article contains an extended version of corresponding VSTTE Paper together with the complete formal development of its underlying commented theories.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361762$E929E593-E8AF-4B1B-B76C-B8BCCE4D0C36","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b11646dfc2677d6614fa16128dbbd7844776606d","datavalue":{"value":{"entity-type":"item","numeric-id":1847766,"id":"Q1847766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$31383133-EF63-4EAD-B671-6F1DB74B6C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d081ee1c24ec3a9e4358e339c8f9e821269780b4","datavalue":{"value":{"entity-type":"item","numeric-id":5938702,"id":"Q5938702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$B129B431-9418-4F39-8093-010BBFE5A319","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75490664644708b71efbf3d600a47f7540edb1a5","datavalue":{"value":{"entity-type":"item","numeric-id":766162,"id":"Q766162"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$C3E2D3EE-6CD8-4248-B0B6-A2C2B5E67662","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba16d3643e7f45b2a6fcdd3509fdca985c4702c9","datavalue":{"value":{"entity-type":"item","numeric-id":2589521,"id":"Q2589521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$117FEB06-36D7-476C-B968-D62BC20BD6BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2179d8546d5ce60e354479db662e7bc4b3f5aef8","datavalue":{"value":{"entity-type":"item","numeric-id":706512,"id":"Q706512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$8C3B4E5D-0B40-460B-907E-3FB08A0B3098","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0553013dea0f84550c63421029d2112e466e081e","datavalue":{"value":{"entity-type":"item","numeric-id":664863,"id":"Q664863"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$29F87C37-C672-4587-9ECE-42A0493CAC18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42e8700434177609e5f649d1f5a0b31b34ec0771","datavalue":{"value":{"entity-type":"item","numeric-id":3055747,"id":"Q3055747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$AD672421-5D31-49B0-9822-F98F43E7EEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$2D0C9F10-8FAB-456E-8539-D98A56983FFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"447925236d6fa2fa96ae6f5f44bf9565bc2da05f","datavalue":{"value":{"entity-type":"item","numeric-id":2368940,"id":"Q2368940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$7E5FF72D-77C8-4F98-B23A-A93277CD3C43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc019e2b4d5136976181164b24b3484dcfaaead6","datavalue":{"value":{"entity-type":"item","numeric-id":4808845,"id":"Q4808845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$47DA7FE6-7993-4192-A895-D3822C0A605F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0198e68f6dc9303aefc05c74bbadbddc5c16bbc","datavalue":{"value":{"entity-type":"item","numeric-id":4472182,"id":"Q4472182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$8CA1EFB9-601A-463A-AE48-1B6AB2CBF88B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1252c469c33fc6d71cdacfbdf2f44a54668edad4","datavalue":{"value":{"entity-type":"item","numeric-id":3585033,"id":"Q3585033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$AB3CA5C1-B7C9-41B4-AEC5-A492F979735F","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$A919D875-5DD1-45A5-8C39-22EC260AD8E6","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"147d947971425f6e481a02787827e4705017a40a","datavalue":{"value":{"entity-type":"item","numeric-id":7360786,"id":"Q7360786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$3A72FA22-AAD8-436E-A90F-50037BF0F68E","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361762$C343A2F7-61ED-43E4-A952-A63951F070B2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Isabelle/Circus (AFP entry Circus)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Isabelle/Circus_(AFP_entry_Circus)"}}}}}