{"entities":{"Q2031429":{"pageid":2042171,"ns":120,"title":"Item:Q2031429","lastrevid":55386673,"modified":"2026-02-17T15:16:23Z","type":"item","id":"Q2031429","labels":{"en":{"language":"en","value":"An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7356982"}},"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":"Q2031429$F079A473-99D6-4D91-9614-430AB522681F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"49207bad1300cea78edc21067f775d027050b63a","datavalue":{"value":{"text":"An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2031429$044B9466-4D78-424E-A274-771F41E45CE7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2bcd82e5ab38b299bdbc22cf18fea63d821286f7","datavalue":{"value":{"entity-type":"item","numeric-id":1687745,"id":"Q1687745"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$63A72838-AB9D-4F8D-B4EB-1A59E26C6416","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5a952aaaf69ec7d1e12fb25db578dd88a813b537","datavalue":{"value":{"entity-type":"item","numeric-id":835782,"id":"Q835782"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$C47461EF-9FD5-40CF-901B-D0A87DDFDA50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9eef155c744fb52510f238bbd2aa5c13b3ad5589","datavalue":{"value":{"entity-type":"item","numeric-id":1687746,"id":"Q1687746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$1A9BD143-12B6-4CA8-A4DE-2064CA1042E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f3208ee20c85d475090d794dc3c7087da944dc6f","datavalue":{"value":{"entity-type":"item","numeric-id":488228,"id":"Q488228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$F6F81997-A970-48C5-A60C-399E3DE17945","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"73fbaffdbd1d77b06dc298a3a9404cc6e379e3e7","datavalue":{"value":{"entity-type":"item","numeric-id":2031428,"id":"Q2031428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$649F3874-5090-469D-9FDE-F9D3E2F092A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c058afea036303a407f9ed86b611b84df43ce2d6","datavalue":{"value":{"entity-type":"item","numeric-id":488230,"id":"Q488230"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$0B2BC521-F453-4B03-AB99-F3B067003494","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$026D4AA9-5057-4938-A96E-72ECCFC00636","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"77b5c623a3a71eb9e2cd375aecfe8a36962b32c7","datavalue":{"value":{"time":"+2021-06-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2031429$E8AD7328-CBFF-46DF-917E-0FB383AF7F0D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"65d4e269e78769f8404058e5e9ac589a648a2235","datavalue":{"value":"http://hdl.handle.net/10072/396682","type":"string"},"datatype":"url"},"type":"statement","id":"Q2031429$13FB4013-78AC-438A-A4A1-CFAC66DD44F2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2031429$499819BC-E16D-4E72-A6BA-6F8AB1AB8BEA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"15f1e0557325d5ac904919d7d43aa4375fc801ed","datavalue":{"value":"7356982","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2031429$378906DA-2720-4FD9-92D4-C224EBED3899","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ad65f4f31918a750bc0b43986ae093159972c1c","datavalue":{"value":"instruction set architecture","type":"string"},"datatype":"string"},"type":"statement","id":"Q2031429$611DD863-3AF0-4093-BB53-4CC2BB6E7998","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"005d5dc458737473c7ac1711c9dd4164ffa7e528","datavalue":{"value":"form verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2031429$C8BA88B2-3C2A-4CA6-A78C-2D9507D2943E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2031429$7EA9CE42-9599-4566-B0B4-A37AD1094190","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b3f0f30b182e40766212b93e7136ab4a7492e57","datavalue":{"value":"weak memory model","type":"string"},"datatype":"string"},"type":"statement","id":"Q2031429$2788AEC2-0E9B-4180-9DE3-EA3C9957D843","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"52deb7337c5cdaacf9769ce18dbaeba4d2b6c6d4","datavalue":{"value":"TSO","type":"string"},"datatype":"string"},"type":"statement","id":"Q2031429$52960DA2-4961-445D-8E0F-2FF9171F2AA4","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"61c2f486dc1b6a94dcf7f6d557b47e6cf2b00825","datavalue":{"value":{"entity-type":"item","numeric-id":55278,"id":"Q55278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$1BD20A9D-8124-4B73-8254-0EF671D8FB58","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":"Q2031429$D15F69CD-8104-4F52-B86B-39199BB10690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"170ccf721178258c21fb4fe9c26f36046af0ecf8","datavalue":{"value":{"entity-type":"item","numeric-id":22099,"id":"Q22099"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$8061768B-6A69-46E2-AF34-A9EA97ECEE45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d8c9ff4a9eac2a34ae6381abc2842acda7fc49e9","datavalue":{"value":{"entity-type":"item","numeric-id":43968,"id":"Q43968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$568F72EC-E086-4769-B33E-D8BDCE4109BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$51B0B821-B03C-425C-B7C8-93710E12E2A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ad0c9888f19e605bfba04523c628f3bab7224e29","datavalue":{"value":{"entity-type":"item","numeric-id":14550,"id":"Q14550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$AD1116F9-9518-41F8-8D9F-BFD3CDBF358B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$B0EEADA5-1D3D-409C-921E-08B33A4996B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6c52e95f9193b2def647e07a619d3a4f4f54b285","datavalue":{"value":{"entity-type":"item","numeric-id":21378,"id":"Q21378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$6075F7A2-1294-41B6-80F0-C8A1A2E7D5A6","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":"Q2031429$14263922-70B8-4103-9C95-D821E4301285","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3ba66b1bd6246975124e7f25c3fe8cc4152a06ef","datavalue":{"value":"W3049189160","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2031429$04C13E22-D8CE-4E6A-BC4A-DCE18F7DF13E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"381701828d1cd2d1d2fea906d017e00eb31e908f","datavalue":{"value":{"entity-type":"item","numeric-id":453523,"id":"Q453523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$ECC526DA-7B40-48B8-9125-B1F0E302B604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0a457c597040796c8cd7d073008378e688faa21","datavalue":{"value":{"entity-type":"item","numeric-id":3523163,"id":"Q3523163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$602A1E8C-45A4-46B7-8641-4521005355E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de81de14e0ab1d1e609635ceacd0ffe5821f453e","datavalue":{"value":{"entity-type":"item","numeric-id":3499747,"id":"Q3499747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$4EDF45E8-79E8-4E76-8F6E-B0CB644EA444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4571140468827117de9ef82d7ef08c246a067fd","datavalue":{"value":{"entity-type":"item","numeric-id":5261535,"id":"Q5261535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$DCAED0F7-B127-469B-BD0C-1974CB049E78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"28d7b9e297fcd76c14248efc49c105939c29438e","datavalue":{"value":{"entity-type":"item","numeric-id":3512487,"id":"Q3512487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$CFE61F01-346F-4AF9-B98A-9955893646A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a386259d7b6de278f96d59178a0ebe00c941a927","datavalue":{"value":{"entity-type":"item","numeric-id":3543657,"id":"Q3543657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$B5E36760-3776-4D8D-B6DE-4EDD2314A060","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"287fdce4dea49dde3238be777f60e985e5d19fc4","datavalue":{"value":{"entity-type":"item","numeric-id":2819850,"id":"Q2819850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$6EF341C8-2B54-4CF4-B5DF-2342E8E85380","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a25e78acad58972c7c0b482a487b0ac7d56989a6","datavalue":{"value":{"entity-type":"item","numeric-id":2945632,"id":"Q2945632"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$2D094170-C3BF-4EDC-BB71-46322E5209D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c51840355e08753d0377af591c495ff9f8053cee","datavalue":{"value":{"entity-type":"item","numeric-id":5747653,"id":"Q5747653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$B245A3F3-5143-4BDF-9A2F-C99ABCA3B684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a8148157c1da91618824ba90e4cbff20a301faf","datavalue":{"value":{"entity-type":"item","numeric-id":2938055,"id":"Q2938055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$82E48191-45DE-4A1D-A4FD-B443D341823B","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":"Q2031429$3943A697-FD69-4977-9FCF-97BD5E1CFBE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea140d80bc2e8eb3a8f68cec269c5b0a87847df9","datavalue":{"value":{"entity-type":"item","numeric-id":2819676,"id":"Q2819676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$53209FB5-0DE4-4BC4-A3C0-5F1E6C27340D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23623728af77877c2c658b5f16ea2ac66fec79f9","datavalue":{"value":{"entity-type":"item","numeric-id":987974,"id":"Q987974"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$21F8E26B-041B-4A3E-9CBD-434D73088752","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a1ac20aef2f2fa3a1493f669811757d690a0798","datavalue":{"value":{"entity-type":"item","numeric-id":3167025,"id":"Q3167025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2031429$BC887E63-34E5-4C45-9A20-CDC1A4BA24A6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4dba1ad35522472cf36dd2faf3a9f0b5e8376e8e","datavalue":{"value":"10.1007/S10817-020-09579-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2031429$2742781A-8751-487E-BEE4-9E0DBBF566FE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f2dc9bd6dbc1f155afd372f6c99fa5e842bb1a5","datavalue":{"value":{"entity-type":"item","numeric-id":5045393,"id":"Q5045393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d5425e67a234673d8a6a61d15f4978d38dfbab4","datavalue":{"value":{"amount":"+0.8348327875137329","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":"Q2031429$44B17B30-088E-4B9E-809C-240F8DFA752B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e65dd9541a1dbfd1ad7026b9e1124c3d9e26f061","datavalue":{"value":{"entity-type":"item","numeric-id":5747653,"id":"Q5747653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba289b4616ad35704889e201e284d15aad876942","datavalue":{"value":{"amount":"+0.7604661583900452","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":"Q2031429$40927475-7FF8-4408-A8D6-44CC1F4314B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69d43a21496ab28993cbdc8cb7ade250536a0eed","datavalue":{"value":{"entity-type":"item","numeric-id":2754045,"id":"Q2754045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6f2dce05bd2e899df347c3ab8c4bb85c323b9a08","datavalue":{"value":{"amount":"+0.716684103012085","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":"Q2031429$3BC78C85-AD0A-4B20-B5BD-233A2F40E798","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb57dac5e9733bbbaad6a936013c102dabfd2939","datavalue":{"value":{"entity-type":"item","numeric-id":4419604,"id":"Q4419604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46e1c8bd872d930bcda1f7262aae0d4808c4882b","datavalue":{"value":{"amount":"+0.7048449516296387","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":"Q2031429$2DF1DBA5-D702-4E0D-B1C7-689AE462B550","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5cffecdcb0abfeae6e20c257833dc680e32399a8","datavalue":{"value":{"entity-type":"item","numeric-id":1791136,"id":"Q1791136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"938092c00ba1eafd8725238cd6e76aff212a1ba0","datavalue":{"value":{"amount":"+0.697084367275238","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":"Q2031429$F0A54DD9-04B5-4B16-8E2E-7887D94DE674","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2031429","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2031429"}}}}}