{"entities":{"Q3535610":{"pageid":5565514,"ns":120,"title":"Item:Q3535610","lastrevid":50492669,"modified":"2026-01-14T04:58:27Z","type":"item","id":"Q3535610","labels":{"en":{"language":"en","value":"Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5365477"}},"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":"Q3535610$13FB3CFC-41E4-4D96-983F-97C874D705F8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a4e73bb9f99128f8f43abb16f12b8a6283a334fa","datavalue":{"value":{"text":"Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3535610$CA01F51C-FB55-48B7-B033-BA332F5A8176","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d0f06eb67341cb494bed66b93f92352a7e104b5c","datavalue":{"value":"1147.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$08EFA426-EF8E-44DF-BB6A-1934BAD10995","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f72e70535e3cce2cfe9463fc0117033a56c5513d","datavalue":{"value":"10.2168/LMCS-4(3:5)2008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$5ABBDBDC-744E-4E3D-BAAC-2D6BF70F9E72","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7d45bc58b6343c85796331c2c0125934a8b7086","datavalue":{"value":{"entity-type":"item","numeric-id":408533,"id":"Q408533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535610$FC43EF00-9FE9-4715-B8D8-83B3AB06F2EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c9f99e72dec046038a5377ceee67d8841bab629f","datavalue":{"value":{"entity-type":"item","numeric-id":1051423,"id":"Q1051423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535610$F7739C36-1200-4B33-B85F-26158B36C078","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535610$021533BD-2CA6-4F4E-A1C1-85679BEAD761","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"27f25e9d3b3894d698b7ec67f164a27a3aba1f7c","datavalue":{"value":{"time":"+2008-11-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3535610$61DE28ED-2908-4FE5-8743-413E0381290B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$D0374362-96C0-4AD7-8E63-8BD88923AC1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$CF2008A4-D57A-430C-95C4-215D8A61A412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$C8F14965-5C5D-4620-A477-DA885405B164","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$82464F6C-BD26-47E0-B348-2B6791009387","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$EC7C286D-B625-4EB3-866E-5E095C3B885D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$E4D0A130-05C5-481E-A375-049B3FA96B7E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0473db15bc747165a6b3a942717d292777107004","datavalue":{"value":"5365477","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$02C2E382-C6AF-4DF0-9D44-9CCAB9FA985D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535610$70063423-E49F-46D9-829C-0004C26A9120","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"193e9e18264a324630ab056534b18c56c3a0c0c0","datavalue":{"value":"intuitionistic set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535610$991D58FA-108F-4089-9445-6CF1EB2E4EFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"58e4b0413b08e48e8d2490466e54c7de7bb508ec","datavalue":{"value":"constructive core of HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535610$B641DBE1-59D1-4C2A-A8E7-829D280CDDFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535610$42B81121-F632-43D2-B239-04DB07891984","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d52fedc06b05496f4c6f09890ca4e7c626a7a377","datavalue":{"value":"weak normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535610$0AAA7AE5-E902-43AA-A1B5-EA8F290EC8CA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535610$2D38A633-DFB9-4F7A-BB25-B29BFB4AB616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535610$73BDF44E-E6AA-4593-8F96-C01E4729A223","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fef5f048f2ff970244195639e7bcf4e64ea5e666","datavalue":{"value":{"entity-type":"item","numeric-id":16795,"id":"Q16795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535610$5A2B8A1F-AB5B-4025-8DD4-14E63D9821E3","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":"Q3535610$556F66E3-F046-4E6F-97D1-8A26DE90BC23","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"15afe67fdc66f2e53fc6ff8e70598c707a38bdb4","datavalue":{"value":"https://doi.org/10.2168/lmcs-4(3:5)2008","type":"string"},"datatype":"url"},"type":"statement","id":"Q3535610$01E26D49-B0FD-4C9E-898B-CB3C80068B68","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1d3e36021b5524c013001a5d7daffc6658226dab","datavalue":{"value":"W3100811144","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535610$4D1959D5-805E-4419-ADF8-803181739897","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a2e864e7792e61a39cdc1e1ab1bcc8cffe750872","datavalue":{"value":{"entity-type":"item","numeric-id":3613407,"id":"Q3613407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a36e2e421a08002796ed1c99046bd2fc92956916","datavalue":{"value":{"amount":"+0.9988774061203004","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":"Q3535610$2A025AFC-EC9E-451B-B57F-1EEAD4E61BFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cc18ee63967d27b68bef5b3a1749be5e3c0935e","datavalue":{"value":{"entity-type":"item","numeric-id":4435458,"id":"Q4435458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"506f2eaaee898671e640302bc040437a4cb780d2","datavalue":{"value":{"amount":"+0.8088686466217041","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":"Q3535610$FE10B399-4671-4794-BFB5-2E4A2F48D9DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"31e06b4fe6c983bb3ab4de626b40fdcb19de88e0","datavalue":{"value":{"entity-type":"item","numeric-id":1823656,"id":"Q1823656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"018b34714ece6f1fa1498f403e0647aa99f714cb","datavalue":{"value":{"amount":"+0.7908289432525635","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":"Q3535610$0A03A354-CA8A-4C7D-BCF8-373772EBDF08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"994abafcebf920ff08b53f01fe6fca3bc5aaf07b","datavalue":{"value":{"entity-type":"item","numeric-id":4038676,"id":"Q4038676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6fe8785ba519a2e8ef92707e9e3191d18df42d5","datavalue":{"value":{"amount":"+0.787056028842926","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":"Q3535610$A32B41D7-DB5A-47EE-9304-34DBBB0FAC35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"096d21890c1496138948b96dc35d29ed108a275c","datavalue":{"value":{"entity-type":"item","numeric-id":2852367,"id":"Q2852367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6fe8785ba519a2e8ef92707e9e3191d18df42d5","datavalue":{"value":{"amount":"+0.787056028842926","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":"Q3535610$A265249A-3EDE-4DA2-9D9E-415403FF8087","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3535610","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3535610"}}}}}