{"entities":{"Q817701":{"pageid":819549,"ns":120,"title":"Item:Q817701","lastrevid":64565421,"modified":"2026-04-11T20:44:49Z","type":"item","id":"Q817701","labels":{"en":{"language":"en","value":"Program extraction from normalization proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5013035"}},"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":"Q817701$76BAC09B-AB85-4D70-BC32-EA8E1F1C88A2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c8c39c5b4dc09abe847c310285f5f01637721d42","datavalue":{"value":{"text":"Program extraction from normalization proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q817701$06EC931E-BCF5-4B25-A464-9C878E2010B9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"69c650d2284a55f5d5a4ed52c064dafe483b2348","datavalue":{"value":"1095.03016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$607BCD9E-BADB-4C50-A0C1-1DA090A82DB5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"56802c23e662b5a0028381459762dce10bc420a6","datavalue":{"value":{"entity-type":"item","numeric-id":234584,"id":"Q234584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$9034067D-01F6-41C3-9D5F-B9A5C86FB7D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"886664d698445e1702c39c62a8e99a722a88bdd6","datavalue":{"value":{"entity-type":"item","numeric-id":817699,"id":"Q817699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$1B694114-1B21-4099-951C-EC6FA0FCAC4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a987ef8f6039e424f47a977407df7137ed1919b3","datavalue":{"value":{"entity-type":"item","numeric-id":817700,"id":"Q817700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$1093DA05-1736-4355-AAAE-6D7EBB5B63C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d89967a655d20159aa875a5d9fe1d91c6683b97","datavalue":{"value":{"entity-type":"item","numeric-id":234585,"id":"Q234585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$D6508906-61AF-48D3-B564-069BA9D002A9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$4F9D6978-0A53-4C2A-A5AE-F1E9DDE807E3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"46a32b96026a1aa43ce9bf7d3e87290deb94d5e1","datavalue":{"value":{"time":"+2006-03-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q817701$05AE6EF3-E69B-4832-8943-E69320C06C90","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$9F015B97-DBA5-4BA3-88ED-091B788E174D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$1ACED27E-A29C-4167-BD0A-C116507BF0BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$D49D5EA2-9731-43A8-A565-6CD6B529EC5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$F755997A-2D9F-4253-B12A-0DBCA4BCE4AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$9AE22919-1688-4B0F-A1B4-426A7363CD7A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ee667595bd9161eab4e213a4c4cee77508652557","datavalue":{"value":"5013035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$B51424DE-300F-47D8-AED0-7CA013A80E6D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5fc3a911bf4ee189b0729d59cbe22419b062b296","datavalue":{"value":"Normalization by evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q817701$875BD6E3-ED6B-4DEC-A300-3AA7598B35E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"01f639a56e1e38a2490c4463ce011c878a3d36ab","datavalue":{"value":"typed lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q817701$ED7A54DC-8AA3-4A90-8A96-B729B81D58A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"53d61092cbbff856a3b199e03225e42bcac6db78","datavalue":{"value":"realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q817701$22F0FFB4-C75A-459F-89EE-3381F481E686","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"65ed99d94397511bd8e22ab2437f30b726b49b0b","datavalue":{"value":"program extraction from proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q817701$1FE71732-F09F-4897-836A-AFE74A49AACD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q817701$A5B0FB2B-DFFD-4366-8A49-FA88E9CBB28B","rank":"normal"}],"P1463":[{"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":"Q817701$58FD966A-0D9C-444F-AA3D-577F8A0F2064","rank":"normal"},{"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":"Q817701$93A50797-D337-4E96-AE4D-109B2ADE3FD2","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":"Q817701$915542F8-2E00-4CC9-93E9-15B1071254B6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5bc0dc0bef758426fb6c15dfa9b1e738c13e0416","datavalue":{"value":"https://doi.org/10.1007/s11225-006-6604-5","type":"string"},"datatype":"url"},"type":"statement","id":"Q817701$134927F3-E8F2-4B71-87C0-06532D20EDE7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"18f715c876c9064b86c5664b4ecfe82eaf92b7f2","datavalue":{"value":"W2020747436","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$F973EE1F-7E3C-4F4D-AEBF-681BE8D4CFC4","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"59cb59848a25a21640623c0b047a52c256087175","datavalue":{"value":{"entity-type":"item","numeric-id":4281467,"id":"Q4281467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$159E4512-2FE1-4A02-BFB2-565006867B54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58fc67f4df0f685e08e46a27070f76b58928a24e","datavalue":{"value":{"entity-type":"item","numeric-id":1401941,"id":"Q1401941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$18FDE84F-C461-46A3-A4FD-7287DD938183","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"15b3cd59cb558f44d816b8e669a26d4f97ad2145","datavalue":{"value":{"entity-type":"item","numeric-id":4435458,"id":"Q4435458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$F70C978C-E200-454F-82FD-2BF76F0E033E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b4749998a63e8333eabd57d6ad134faa39446f2a","datavalue":{"value":{"entity-type":"item","numeric-id":4525278,"id":"Q4525278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$E72DB559-1842-4748-B6AF-C0E4CA315F3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"730be61f324b593b9cdcf693cd18218da2ef3707","datavalue":{"value":{"entity-type":"item","numeric-id":2785696,"id":"Q2785696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$6C5B73B4-F7D0-4E3D-A549-EC2D72E22A0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70d5dcacdf82491509f047ffa7adf630e71ade90","datavalue":{"value":{"entity-type":"item","numeric-id":5667469,"id":"Q5667469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$64DE49A4-C322-48AF-ACA9-8103CEC076B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ac3bd59819bab3c20ab46afa2f257091fcd8fbd","datavalue":{"value":{"entity-type":"item","numeric-id":5344164,"id":"Q5344164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$4BF46303-8422-4EBD-B8D0-D5CE1AB8D262","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f3c530cc07456f63649e40272ce15d885679b0e","datavalue":{"value":{"entity-type":"item","numeric-id":808273,"id":"Q808273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$F70817DB-5161-4A49-A0F9-0B8C7E9D6F21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb1812a83c3a4aee25d6a67b2527c143aea9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$E780FA36-DA32-4980-BBA8-4CE96E81B46C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82af13d5271451c4bb72d7b055064b56ff1b2fb5","datavalue":{"value":{"entity-type":"item","numeric-id":1322847,"id":"Q1322847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$83449A48-C2CD-4273-B334-082F95A2F9DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe420790aaa202d504d047412b1e69b630045474","datavalue":{"value":{"entity-type":"item","numeric-id":5464715,"id":"Q5464715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$559BC0B2-93D6-4296-8EEF-DA9DF8C00EDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q817701$7F83A711-AA5A-403A-8970-E1B2435A4321","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd4631d035516741304e472a6a3766b61dd83f6c","datavalue":{"value":"10.1007/S11225-006-6604-5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q817701$70CD1E97-48B7-4358-A412-C9582D63CA9E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f65ccfe89edfee7e808370feea971f6c76e59d31","datavalue":{"value":{"entity-type":"item","numeric-id":5898172,"id":"Q5898172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c7406c42c05e86e88a342cf6fa6a2612685097c2","datavalue":{"value":{"amount":"+0.906866729259491","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":"Q817701$4C80272F-AF68-4BDE-A373-1FC5D7C25FF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a8c39ff1703fa649627f769e20a60cac8c6f394b","datavalue":{"value":{"entity-type":"item","numeric-id":4281467,"id":"Q4281467"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1a2a36984c1d6a185ed11b23f358057c6de914b9","datavalue":{"value":{"amount":"+0.9061567187309264","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":"Q817701$F8BD7E3C-A89F-4DEC-8E84-F4E89D3C09AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bddae59653a1d3ed8fd5fe3ab91bd959e5efd41","datavalue":{"value":{"entity-type":"item","numeric-id":2852349,"id":"Q2852349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e1d761ac7bca8f660a41e85f6f0ca161f7eee17","datavalue":{"value":{"amount":"+0.8925981521606445","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":"Q817701$79707E19-A0E0-4608-8DC3-AF6690BAFB01","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":"79ca3f6bc581fb2f3f3c89a17cf7d915a78a386c","datavalue":{"value":{"amount":"+0.8255695700645447","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":"Q817701$E644AF13-AF55-457C-8236-DA1198AFECBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"73311121b3c8f4ba9b82f27416e15f4893fbbc45","datavalue":{"value":{"entity-type":"item","numeric-id":2844809,"id":"Q2844809"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fc5e60a9945c062cc03ce2c861343435a4fa4e09","datavalue":{"value":{"amount":"+0.8065148591995239","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":"Q817701$37FECC62-31C8-4CBD-9FA0-C1B241EC3E77","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program extraction from normalization proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Program_extraction_from_normalization_proofs"}}}}}