{"entities":{"Q43946":{"pageid":44002,"ns":120,"title":"Item:Q43946","lastrevid":105428525,"modified":"2026-10-09T10:10:01Z","type":"item","id":"Q43946","labels":{"en":{"language":"en","value":"Certification_Monads"}},"descriptions":{"en":{"language":"en","value":"AFP entry Certification_Monads"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"4ef4d1513cf4924355ac954e5b2e3f02d1d5f740","datavalue":{"value":"32235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43946$5E8B1401-3A5A-4221-9ADF-2EB1702DBAD4","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":"Q43946$12EC88EC-A23C-431C-ACA4-46F5D50BCD99","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"9c768c15da8e8fab2fbff5c02b0e96f2e0ff1518","datavalue":{"value":"https://www.isa-afp.org/entries/Certification_Monads.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43946$FD48E930-FF2D-4436-9D51-8355A0831E9F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43946$EB245395-FB76-4BAA-AE1C-631D05B154FB","rank":"normal"}],"P1458":[{"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":"Q43946$0B760542-7BC3-4C7D-967D-697EB3D99D4C","rank":"normal"},{"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":"Q43946$09D45403-B458-4238-A222-0A78B1387D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"acb83a4d262d787fb22b160cee44d797c18d249c","datavalue":{"value":{"entity-type":"item","numeric-id":1353374,"id":"Q1353374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$D493F871-7F07-4A68-A334-48251BA1E93C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"083108faf337c7af517e32b440172fa2ec83c61c","datavalue":{"value":{"entity-type":"item","numeric-id":5973381,"id":"Q5973381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$73B2ED51-FB95-463E-BE78-BDF81BD5C949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f5cf1c799fbe6d303f4d3cb6807bd68c09cb6169","datavalue":{"value":{"entity-type":"item","numeric-id":1353381,"id":"Q1353381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$1659D04D-78A9-47AC-B24B-A13C1DAE31D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"c07dad7b9d1fb6cf6c1ef6118cf06bc6823ad96f","datavalue":{"value":{"entity-type":"item","numeric-id":1353377,"id":"Q1353377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$46BE5ADA-5880-4D9B-899B-792E08100059","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"feccd3116831194613b0ee92ed8475cd8805d11f","datavalue":{"value":{"entity-type":"item","numeric-id":1353379,"id":"Q1353379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$8D760A35-E17A-46E6-AA0E-3F5D0BD2A4ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5be44e7d4be9fe3a06dc3ddef1f71816cb9bba8b","datavalue":{"value":{"entity-type":"item","numeric-id":40306,"id":"Q40306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$2CECA8AF-DC92-40B9-A593-34FAE989AB39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$27EBF953-4AC6-44F7-A4DB-17C42942FE40","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":"Q43946$2F0CBBF4-6470-4D3A-89B3-B9AA0792B30B","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":"Q43946$38C307E3-FF36-4185-BF8C-29C83BEAFC8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"47548059e3416b4b47c737ba6e24ccdeda7d9657","datavalue":{"value":{"entity-type":"item","numeric-id":40548,"id":"Q40548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$32597C47-79DF-4E20-B196-3F5E3B3A26D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b7f473d31c631be2f4d8cd38df4295d75e1138a4","datavalue":{"value":{"entity-type":"item","numeric-id":40547,"id":"Q40547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$9A9A22A7-D223-45D3-A2A7-DF321B48DA37","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":"Q43946$BA066456-BFCF-42FE-A87E-B5A5C4E1DCCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"61d0c0612cc30c9c51b93ddaf1f78ee1ae75f9fe","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$3B3B3B78-6235-4ADE-A42A-93E7D09D208F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4225824ce6a78acadc945f0e0004ed10ff6a0a1f","datavalue":{"value":{"entity-type":"item","numeric-id":43692,"id":"Q43692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$73323D05-BE9C-42BD-8F8E-D5FFB1A64A7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f01c83a5a54fee889f3ec90409eea63e50d19053","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$501D8D27-BBCC-4BC6-A413-6521C0283C78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cea2a7e9bb130921d12e1d361b3d4585036772c9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$740BD352-CDDA-4156-A070-5DD29D0E1D1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e5e8684e8339ba421338afd59297e657343b949d","datavalue":{"value":{"entity-type":"item","numeric-id":21785,"id":"Q21785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$CD244941-02FC-4CAC-BDAD-9FE38BFDE9DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$AA6ADFD7-2267-47A4-8DFE-6D8AD63A66CB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a101a4daa012838c07b12a4670e9398a3be0b205","datavalue":{"value":"https://isa-afp.org/entries/Certification_Monads.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43946$D46E74E9-4151-4245-9970-60735F1DCD26","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q43946$585220E9-E0A2-4AE2-BB90-6CE905351A66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3e961f1f2b2e533bd88ffdbcd178bd2ef2813f73","datavalue":{"value":"Ren\u00e9 Thiemann","type":"string"},"datatype":"string"},"type":"statement","id":"Q43946$B927A965-36B9-4E1D-8EF1-2FFC6E3C74E9","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"daf94c66b3f6032df5b7af0eccf6d8b3f3afaea9","datavalue":{"value":"This entry provides several monads intended for the development of stand-alone certifiers via code generation from Isabelle/HOL. More specifically, there are three flavors of error monads (the sum type, for the case where all monadic functions are total; an instance of the former, the so called check monad, yielding either success without any further information or an error message; as well as a variant of the sum type that accommodates partial functions by providing an explicit bottom element) and a parser monad built on top. All of this monads are heavily used in the IsaFoR/CeTA project which thus provides many examples of their usage.","type":"string"},"datatype":"string"},"type":"statement","id":"Q43946$085508DE-42AC-4B50-9656-FB30CC3DB3B2","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"1201acfd0ade107234c23996279076e377633ac8","datavalue":{"value":{"entity-type":"item","numeric-id":7361247,"id":"Q7361247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$1DB5FB34-3F8A-4183-BFA7-66C67E76D1CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c8b055357156b513ebffa05abff4ab0fc053c1d6","datavalue":{"value":{"entity-type":"item","numeric-id":7361662,"id":"Q7361662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$46224096-3571-40D5-9E79-789882F3B4E2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fc0586fb6d067887a01c3a487054385370fea97","datavalue":{"value":{"time":"+2014-10-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q43946$99F9810B-91A5-4AF6-856D-0F57429AD2DA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bd4f742780cf143290d872e4c57b2c7d3236fcdf","datavalue":{"value":{"text":"Certification Monads","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q43946$C94C0CAA-C7EE-477A-9D7E-E4E07991B83B","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":"Q43946$A4F0E0E1-6C35-430C-8B97-E615D33E1EBF","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"eff161b7dcf55a20ec4d840b7f18d4148cc115e3","datavalue":{"value":{"entity-type":"item","numeric-id":7360789,"id":"Q7360789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43946$F1BB751A-DA28-4BBF-AD1D-F36A2376CB1D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Certification Monads","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Certification_Monads"}}}}}