{"entities":{"Q7361736":{"pageid":31520747,"ns":120,"title":"Item:Q7361736","lastrevid":105368471,"modified":"2026-10-07T13:37:30Z","type":"item","id":"Q7361736","labels":{"en":{"language":"en","value":"Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming"}},"descriptions":{"en":{"language":"en","value":"AFP entry UTP"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"50a35d26b1f9e882d31251a8300b076a5acd90da","datavalue":{"value":"https://isa-afp.org/entries/UTP.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361736$47A1092C-919A-42A7-8F0A-0DBB371D26F9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3f4145805478faad59761c3ff4a8cc3fff513172","datavalue":{"value":{"time":"+2019-02-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361736$A83D1B09-BB5D-4647-BBDA-58EAB126C090","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c9ddb9cb8edac3e4e3079ad62f4b03206fa5cc4b","datavalue":{"value":"Simon Foster","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361736$27BC3AFE-EB96-4B8B-A33C-4A64BEE9E906","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2c5b18ebe11027a9cddf39baebf8dac2c938457c","datavalue":{"value":"Frank Zeyda","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361736$2C69D535-A085-4762-8A64-0B25C74F11E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"7a2acdf8ea1a4d9f71e469cf7cf3bfea114d33de","datavalue":{"value":"Yakoub Nemouchi","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361736$7F92195C-B3A7-48AE-8158-F750DEE5B0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"2057b98ca1137be3269eb5199838e37fc9503100","datavalue":{"value":"Pedro Ribeiro","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361736$E65B9AB4-06C3-4F35-B68C-F98603699D79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"9f417d50d28c3248f72294b3f5970214162e0fab","datavalue":{"value":"Burkhart Wolff","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361736$0A7C7772-5EF3-460A-9420-A74D2E5BA57D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"64e13bd7f7d532be9dedf9d3588ee772571fffe3","datavalue":{"value":{"text":"Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361736$83A05F5F-6406-4B58-95F7-5A5B7B3DD2EF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7e90383ae9e869acf093e6a01492ed373a15deee","datavalue":{"value":"Isabelle/UTP is a mechanised theory engineering toolkit based on Hoare and He\u2019s Unifying Theories of Programming (UTP). UTP enables the creation of denotational, algebraic, and operational semantics for different programming languages using an alphabetised relational calculus. We provide a semantic embedding of the alphabetised relational calculus in Isabelle/HOL, including new type definitions, relational constructors, automated proof tactics, and accompanying algebraic laws. Isabelle/UTP can be used to both capture laws of programming for different languages, and put these fundamental theorems to work in the creation of associated verification tools, using calculi like Hoare logics. This document describes the relational core of the UTP in Isabelle/HOL.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361736$C0157691-C36F-4BEE-A89E-55E6A12E93EB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"13b2e611a60bbb1cbb1ab23d8301e40dbbe2b3c5","datavalue":{"value":{"entity-type":"item","numeric-id":2915136,"id":"Q2915136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$BD675D8A-B5B4-400C-A8AD-7C5872B5463D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cad5dbbae1e8a09daaaad27474e686d1687d9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":5327345,"id":"Q5327345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$E6C41BA7-1985-4ED3-89D6-E5107B659B1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc62f32ebe5f2c566c09500f98ee202c262830a","datavalue":{"value":{"entity-type":"item","numeric-id":736461,"id":"Q736461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$B5EF4FEC-02AA-4681-B167-3C08E1BA524A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79e807f14dcd5f9ad4f6bbeb1f8ea3c4bbb7d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$BCC29BF3-E47C-4B75-AAAD-A60A398B42B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9689d3285995afb42633d6587b8f7ef68cfb9e38","datavalue":{"value":{"entity-type":"item","numeric-id":5756774,"id":"Q5756774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$C12A34F8-56D1-47EA-B250-82CD07C5A743","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad5469f72b3d14e0a040a00af8c98b8e5cf4cb2b","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$B6D0ED3F-A5EA-4AFE-B004-B9011922B68D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2df24839d625a390053c16402f9628907f226566","datavalue":{"value":{"entity-type":"item","numeric-id":5901607,"id":"Q5901607"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$86433645-1413-4F7A-8771-01BCB47C60CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1265d63b4599a3fae507d9b15943296bbefa977b","datavalue":{"value":{"entity-type":"item","numeric-id":4066568,"id":"Q4066568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$B333D58F-3180-4C3C-9EA3-AEDE7EDC8B6D","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":"Q7361736$88CFDCBF-3530-400F-BFA1-FEC8209F7C52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ea00f9571a2f3eb35a08ae82329dd711da0dc8b","datavalue":{"value":{"entity-type":"item","numeric-id":2814613,"id":"Q2814613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$5E510DF7-EBD0-4DF2-A452-331A39000E8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5981e1168811f3b1a276d506216532fa05a55595","datavalue":{"value":{"entity-type":"item","numeric-id":3179407,"id":"Q3179407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$1FAC0A49-BF9A-42DD-8EC4-CFDCD4D96B4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23a4f79d5a209fbc2d0b0773de40c58b9c966c61","datavalue":{"value":{"entity-type":"item","numeric-id":2971180,"id":"Q2971180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$48526D23-DFFD-425B-BB5A-79FC1DA7607D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bcd3d912fbc11a09800564de2ac48525b4612f1","datavalue":{"value":{"entity-type":"item","numeric-id":1617824,"id":"Q1617824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$EAAD1D8C-4284-4D2B-AD68-E2CABC4AB599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d0e3a179147832b2b1c96869b8d44ccac54dac91","datavalue":{"value":{"entity-type":"item","numeric-id":4343990,"id":"Q4343990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$7A2715C5-F0A7-49D8-95CE-10CFE96AF9B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c82ad10c73e928271f482901deda0f097caa8289","datavalue":{"value":{"entity-type":"item","numeric-id":3723675,"id":"Q3723675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$7B7A6869-4C11-4905-9725-71515BB0121F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1300e3eec1483356f2aa40f3f69ca17003308951","datavalue":{"value":{"entity-type":"item","numeric-id":1094864,"id":"Q1094864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$BB9A96D8-DBAE-4EE5-BE60-09E56809EA64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc474b97bf58673fb5d3311c2f358b1d99bb6b18","datavalue":{"value":{"entity-type":"item","numeric-id":808685,"id":"Q808685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$9B13D170-0A46-4773-BCC5-CDC6FC776D20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e27ad4b2994da46e11c5d31647a6af63a7a804b","datavalue":{"value":{"entity-type":"item","numeric-id":4282663,"id":"Q4282663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$07624B44-F24B-4D91-9FC8-C6D40EB97BFA","rank":"normal"},{"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":"Q7361736$20A27040-A75E-4E44-BE39-05D2102E2E59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$FAD139AF-66CF-435A-8A9C-5A12737E1366","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8576dc8df0d7857399ab718724b601efc6d9d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3996918,"id":"Q3996918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$619A6833-33F9-4490-9608-F34C1A160B7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"deb9865b9ec7d75ea6408f7463449ba93e2c161e","datavalue":{"value":{"entity-type":"item","numeric-id":5307478,"id":"Q5307478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$3E6ABCC4-A8D6-4AA4-99E6-CDE1E75C5487","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":"Q7361736$D57003EF-0D61-4EB1-B73B-00C2ED073D0E","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"38013d195453d9de6ec304fa06493915c9a40199","datavalue":{"value":{"entity-type":"item","numeric-id":7361308,"id":"Q7361308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$524D85D1-C5E0-4B26-B2D5-C74D9BF06899","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aa8f6bd5a2b4440f838b34acf103bdf45fee4f56","datavalue":{"value":{"entity-type":"item","numeric-id":7360797,"id":"Q7360797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361736$8915E984-2331-49E5-91C0-A3E17CDD4EE6","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":"Q7361736$E7EDC79A-DB49-4E2F-B565-EC551600C85A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Isabelle/UTP:_Mechanised_Theory_Engineering_for_Unifying_Theories_of_Programming"}}}}}