{"entities":{"Q40296":{"pageid":40352,"ns":120,"title":"Item:Q40296","lastrevid":105426908,"modified":"2026-10-09T10:06:25Z","type":"item","id":"Q40296","labels":{"en":{"language":"en","value":"CryptHOL"}},"descriptions":{"en":{"language":"en","value":"AFP entry CryptHOL"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"cabad2fb12901a6505ae42b260aa5d983c19cd6e","datavalue":{"value":"28582","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$E41C55A5-CE3C-4EE1-93F3-B56ACF8AF007","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":"Q40296$BA3536A2-77C7-4340-A318-8FBC597BCE62","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"059fb2b13a18f1da3027e294a232b964d9cb33a1","datavalue":{"value":"https://www.isa-afp.org/entries/CryptHOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40296$5B54C722-4433-44DA-BD5E-E832057A13E0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$379E65FE-20FF-4E53-A863-9D0568C3B70F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f50a93e1fa52c1f7a63c5e1d98864f256220e6f","datavalue":{"value":"18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$47402FE5-557A-448C-B827-A6258CB107C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$4F5DCCDC-833A-4D2E-9287-1CF34D0BC8C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a438efc028ac8f007fcfec586995516429ecdd8","datavalue":{"value":"91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$FD3E96A4-BBC5-4913-BBC5-471B9FC488A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$581F59F1-B3A0-4286-9717-FC3711D41CE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$B6EFDD61-B64F-43D9-86ED-A02561878910","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6e6992288898c4b84d0375236ed98d3bb5559a8c","datavalue":{"value":"18.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$BC7DEE81-68FC-4DDC-B794-8D7B6CCAD5BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$DFF72ED7-A367-49F7-B0D7-1C2591A9908E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca6833d3c12e329e13f5f7a45eb21803ac988009","datavalue":{"value":"91.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$BB93D08B-EDFE-457B-BD05-CD4E4FF8F71A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fb7b2d196cb181e838b342f41804d522dff44830","datavalue":{"value":"94.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40296$5391B641-B590-46E3-96D1-D2CBD4935AC6","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$732492CC-9FCE-49D6-AFF2-894F5B080C48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$E5779D3E-CA96-4003-91F5-6D0368527386","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a3f9d192df50f24767772f5b218635cb7747b820","datavalue":{"value":{"entity-type":"item","numeric-id":21717,"id":"Q21717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$1E188A21-75AD-47A0-9635-DBC72B191B04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$5521BD4D-88E7-4E2B-ADDD-22640A1C5A52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$2442BB26-E2C2-4F1F-91D4-BB0398B06114","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$7662D893-412E-4834-9D29-DA43E7FE5F98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$3D5E9566-B87A-4CE3-B80D-D00C2DD23509","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$1A7060AC-2D25-4C11-ADA5-D86408948292","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4eea1e5549472c93f3282a38917960fdec6b61a1","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$9B63F726-C3A2-4A99-BD52-0BA2B4539896","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c73982343825451091ce3b213d9159c64b1144a0","datavalue":{"value":{"entity-type":"item","numeric-id":5973029,"id":"Q5973029"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$DA867841-739A-499F-A11D-E79E886492DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$1B382D52-8B00-4D7F-BE1C-9C84FD28F631","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$5030D562-9AC8-48B6-B896-D290C95F81A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a9ae85a42a9389273788ca575d22b851b09f7a98","datavalue":{"value":{"entity-type":"item","numeric-id":40297,"id":"Q40297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$CEC3A8A8-9E45-470F-8CE4-8770F4CFB215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b49b6cd0d730920a3a4cd5d33a24263cc6515903","datavalue":{"value":{"entity-type":"item","numeric-id":43940,"id":"Q43940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$77E68310-8E29-412E-A4C6-32A3FFE91BE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b339d0b6ae133d11e46b5f2af365ae2fb7bbb5f7","datavalue":{"value":{"entity-type":"item","numeric-id":24595,"id":"Q24595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$8384DC98-6BC7-44CB-92DE-8197BB790B57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"3a073d1e3162db58b1a890386d8dbe9eebb4637c","datavalue":{"value":{"entity-type":"item","numeric-id":40373,"id":"Q40373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$0F0289CA-44DE-48E5-BF6F-F73796D9E5DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b74075817e632ca235b8b1333580f4f12e29f9fd","datavalue":{"value":{"entity-type":"item","numeric-id":40372,"id":"Q40372"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$A643B9BA-747D-4917-8FEF-F7183AD67D67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"868d665ea0607bf8bd28ea3e3872eb2ea87bd3d3","datavalue":{"value":{"entity-type":"item","numeric-id":40371,"id":"Q40371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$4E3324B4-23FD-464F-B02F-5EE33475E3A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"246d8bcd4bf1600a7c6d2b07f9f11f8689d33486","datavalue":{"value":{"entity-type":"item","numeric-id":40320,"id":"Q40320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$D5B490AB-C33B-48D6-9785-EF8D89DEB636","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"25f6d9b193c13b90e6fa0378c3168d17ddc9f6de","datavalue":{"value":"https://isa-afp.org/entries/CryptHOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40296$7040607C-C3DF-4B94-A566-41F89FCDF8A5","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"480a99c095fd0e6e30ce40dd951da46a627a2bb9","datavalue":{"value":"Andreas Lochbihler","type":"string"},"datatype":"string"},"type":"statement","id":"Q40296$9EA8D4A3-4C74-42E3-A029-CA8EA410AE9B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"1e23c47b87c1adc06781ea373424ffca790da10d","datavalue":{"value":"CryptHOL provides a framework for formalising cryptographic arguments in Isabelle/HOL. It shallowly embeds a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. All operators are defined in the new semantic domain of generative probabilistic values, a codatatype. We derive proof rules for the operators and establish a connection with the theory of relational parametricity. Thus, the resuting proofs are trustworthy and comprehensible, and the framework is extensible and widely applicable. The framework is used in the accompanying AFP entry \"Game-based Cryptography in HOL\". There, we show-case our framework by formalizing different game-based proofs from the literature. This formalisation continues the work described in the author's ESOP 2016 paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40296$2438DCD5-871E-4461-9D67-ACD163381445","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bea8e9846e13a8715ab50748c9877999c599ec7","datavalue":{"value":{"entity-type":"item","numeric-id":3374913,"id":"Q3374913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$85D2A893-1510-451C-AE28-EF6CF6FAB5C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a334f4e96bc67eac9a5d7b987fa6f5d79a92b99","datavalue":{"value":{"entity-type":"item","numeric-id":2802495,"id":"Q2802495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$5986592F-5348-41AB-9DEC-14D26B2FC841","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"8cf17faf422fed75969aa9ebe32b8797880978b1","datavalue":{"value":{"entity-type":"item","numeric-id":7361733,"id":"Q7361733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$1C07979A-FA6D-417F-AD80-FA4CECBBBE53","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c9d73c02403c0af647a73b8da7299dbef78ebf0b","datavalue":{"value":{"entity-type":"item","numeric-id":7361764,"id":"Q7361764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$8B6D69A3-695F-4539-B00C-5849261C8891","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"4e61d5c4974522a5fe3780c9295027ba96d92743","datavalue":{"value":{"entity-type":"item","numeric-id":7361487,"id":"Q7361487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$E9048CCA-E8DF-4756-8F06-B7A43DF22857","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"ceeec1476c044e883da5dc800851f022e7ceae8f","datavalue":{"value":{"entity-type":"item","numeric-id":7361442,"id":"Q7361442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$9BD6374F-B21E-4E73-B1CB-0FF4B5BEDADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"abad7694171204674d0fda3827a1c54b91a3bcbe","datavalue":{"value":{"entity-type":"item","numeric-id":7361663,"id":"Q7361663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$A9CB2DA5-5CC3-4AA8-8F44-E29FBBE7AC1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"97f9bc766ccc3eaa2e22da53fa3df5f4950376fd","datavalue":{"value":{"entity-type":"item","numeric-id":7361635,"id":"Q7361635"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$4747DAAE-A5BC-414B-9B21-A0F05A42D89E","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"67cfe7e765f8f36de5d26ce854526f3fec39cd26","datavalue":{"value":{"entity-type":"item","numeric-id":7360802,"id":"Q7360802"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$EAE7BF01-0868-4658-B4A2-E3B82188D643","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"8efbe8612495bcc999dc22ed8b71d2801a69cc6a","datavalue":{"value":{"entity-type":"item","numeric-id":7360834,"id":"Q7360834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40296$142471EE-92A7-417F-815B-2FBECB4FF4E1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2521123b5dbe8709daed0db214711d9c66f9f8cf","datavalue":{"value":{"time":"+2017-05-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40296$C06434C4-59C8-4DD8-A4E3-82810E0EBFAF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"eba234e5ab58752f783078acbf4a7065493d7bae","datavalue":{"value":{"text":"CryptHOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40296$2B4147DD-08D2-465A-8EF3-1793FC5DF63E","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":"Q40296$0D54FD75-01EB-4203-A8F3-A7B66366A887","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CryptHOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CryptHOL"}}}}}