{"entities":{"Q1799129":{"pageid":1809871,"ns":120,"title":"Item:Q1799129","lastrevid":53239796,"modified":"2026-01-24T12:59:52Z","type":"item","id":"Q1799129","labels":{"en":{"language":"en","value":"Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6958128"}},"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":"Q1799129$4CF7D112-9E4A-4869-972F-3C05CD6A5DC1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d6c79ec228df798fbff5f4578b60cf08607a3773","datavalue":{"value":{"text":"Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1799129$CF53E77A-80CE-4D53-8AFF-6CD3DD27F99C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cc0f330b320a3b429a8d74f1df4f5d443c70820a","datavalue":{"value":"1468.68060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$6C250A9F-8419-4F14-8222-505F0E49A791","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3364851d29dd837c92888345276eeb3f5b7a5566","datavalue":{"value":"10.1007/978-3-319-94205-6_42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$D0D4A54A-C3B2-4825-A69E-7FBD20AD38CC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"48bf256cb2060adcce83d6ff0339ba7814ac6cab","datavalue":{"value":{"entity-type":"item","numeric-id":1799127,"id":"Q1799127"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$45700C6F-B678-4836-807F-479ECCD950C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"62025305e3524f61b1fc8b1f7bbd2484241846ea","datavalue":{"value":{"entity-type":"item","numeric-id":287359,"id":"Q287359"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$3E02EE71-A2AA-4A03-929A-35FAE0C641FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c330e55e5dc72ba4e46dcf35457734e0df28701e","datavalue":{"value":{"entity-type":"item","numeric-id":286789,"id":"Q286789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$2F660BBB-3811-4B36-81D8-BE680B873530","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d8505fc68a1c1f3753cae6e600a747c5cc24257","datavalue":{"value":{"entity-type":"item","numeric-id":1799128,"id":"Q1799128"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$ED9120B3-7986-43D8-B1E9-50650CAEC701","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"145fb4ab3c36a5f99f91a0be2758a779e5bceae8","datavalue":{"value":{"entity-type":"item","numeric-id":386031,"id":"Q386031"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$BFF1B41E-D967-46B9-A17D-2EC9C25F9045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dfafe9df40e2ed15d699f18ea65ba347d60759cf","datavalue":{"value":{"entity-type":"item","numeric-id":684212,"id":"Q684212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$09EEE883-5D51-417D-81C1-C059A01667AC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1799129$B18AF627-CA5A-4874-9301-387E1BE7CDC9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$BC675D5F-3467-440E-ACBE-2C1BEEC1CB07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$C076D7DA-FAF3-4A50-8FCB-A6B598CE8740","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$5B1D32E0-C06B-43AB-B38F-1728A95439DF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9ccc71e8ce065a89f413932ec55de7b7c6e3f478","datavalue":{"value":"6958128","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$DD408DD6-5ABF-4F0E-9B57-6F253C9FF79D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$48E1EF47-EEB2-465F-B8EA-30C382542E3D","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":"Q1799129$ACC9413D-9028-47F6-8734-732A761C348F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$6AA27023-06AA-41AF-9459-B08D81AC1085","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$2772941B-91FA-4B6F-AEAB-5472E2A234F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d5319e1a94029ba2f1a7d93c4f21666dfa15bffa","datavalue":{"value":{"entity-type":"item","numeric-id":39198,"id":"Q39198"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$2633E676-A515-40BE-8785-2025D2518100","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6afb9e05f24776a03d7fcd415baf7b99112468c9","datavalue":{"value":{"entity-type":"item","numeric-id":34519,"id":"Q34519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1799129$3DCC3950-519C-47D6-9FD7-E126F4B1EE6B","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":"Q1799129$2BFF434F-826F-495F-8FCD-E301EEC6C2C5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9eec963e2c98b36adeae8d3bf92f4e984c9b171c","datavalue":{"value":"https://doi.org/10.1007/978-3-319-94205-6_42","type":"string"},"datatype":"url"},"type":"statement","id":"Q1799129$35FD2D3D-9517-419F-8DEF-BE3A26CB6B8D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"46677b5b46e1b74260899c9732209cee051a879b","datavalue":{"value":"W2810040629","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1799129$B6B8B352-1398-4A43-AC2B-4825A32429A0","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9556bf7f6ed0e05daee465305db68b6b32bd1c8c","datavalue":{"value":{"entity-type":"item","numeric-id":2208292,"id":"Q2208292"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2f2c1aa6bb36ed8703266900f561cd66c2646a26","datavalue":{"value":{"amount":"+0.980113685131073","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":"Q1799129$6F50DC16-1B83-478D-8D5C-1FA8540A60A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c8b9f7343efe63e57ddd2bd2ef0ae5831271484","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"255425dc9b2e538f8a3188e4da08465bf197e9b5","datavalue":{"value":{"amount":"+0.8034969568252563","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":"Q1799129$733F4924-34E2-4E27-BD56-DB7F36EDCD99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f111eac5ad767c0299626bb8fc33167280082866","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3a2a6ba000924d731ae9d04d3ee1c5d9f5f788b1","datavalue":{"value":{"amount":"+0.7780616283416748","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":"Q1799129$9FDA7A45-87BD-4AF4-9F76-C4147FBD3915","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"534ab4cc528829f573af9e6705220481f24ef1c0","datavalue":{"value":{"entity-type":"item","numeric-id":5168887,"id":"Q5168887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57fd4c625613a23865ebb2949333d9a90a57671e","datavalue":{"value":{"amount":"+0.7777986526489258","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":"Q1799129$955E8421-5736-462C-A87A-E2B853B2DD4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce4f46d2cdea2125b41d2d1fd3cc2b4dd8eb6de3","datavalue":{"value":{"entity-type":"item","numeric-id":5408415,"id":"Q5408415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c966a51e23bd036e0bf6cc2d8c4bf18d977802fe","datavalue":{"value":{"amount":"+0.7424537539482117","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":"Q1799129$31B30850-4BF0-4969-9370-7040DDD61B30","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1799129","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1799129"}}}}}