{"entities":{"Q4916212":{"pageid":6945793,"ns":120,"title":"Item:Q4916212","lastrevid":91002434,"modified":"2026-06-04T22:00:37Z","type":"item","id":"Q4916212","labels":{"en":{"language":"en","value":"On automating the extraction of programs from proofs using product types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6156020"}},"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":"Q4916212$307768C7-7478-418D-956D-1B82A5012191","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"eecc26b9e46a9457e42d77151c8ad7e05c2005e8","datavalue":{"value":{"text":"On automating the extraction of programs from proofs using product types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4916212$99BF4C0E-1834-4AAB-8304-3FE9B6F7DCF9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"500bd82af95ae2a7a3096ad62f36f4491d0faca0","datavalue":{"value":"1261.68045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$F3AFD588-3C4A-4B3F-B3C5-C56D99DA22EF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5bf1ad6be7097dac5fb479e2bedbfa1f00b36d5f","datavalue":{"value":"10.1016/S1571-0661(04)80551-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$AC21131E-B6B6-464A-B447-55F4FAC02E11","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e789e7d13968ff4d1bb0c8502c94008354a07915","datavalue":{"value":{"entity-type":"item","numeric-id":195251,"id":"Q195251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$7BD3D233-39B6-4A74-9D63-EDC9B0AAAD3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fb39c66b74dd471ce57c28215b275dfb915aaaa4","datavalue":{"value":{"entity-type":"item","numeric-id":529653,"id":"Q529653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$F08C082F-49E5-4893-9744-9F79BA3D1998","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"69111b29da1a9ff727b31d3492d0ce1a50b7b942","datavalue":{"value":{"entity-type":"item","numeric-id":2576569,"id":"Q2576569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$2F384FF1-DB1A-4C09-BB6D-7D7676ED5446","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$BD7879F4-7003-4DFB-AA71-21569573ECEA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"09328fefd4bef3fd48b14da7de769686b3303861","datavalue":{"value":{"time":"+2013-04-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4916212$7CAF470C-0D76-40E7-87BA-FD8AD5A221AA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$B5D2AA7D-20BB-4261-B29C-4B70B9FF28F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$594FC82F-740F-4D93-B0A9-A5C374CCFD84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$4C6CBFF3-3B40-4D54-BFE3-313CB7A97881","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"56a9a80170b5f7146ccc7b3b406e09c6b59514c0","datavalue":{"value":"6156020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$5AA0D9E1-919F-4CE4-98F6-6385D8B0ADDB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916212$5EB0D9C2-AD08-404A-9C86-2E680278C056","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"20bcf30e806e78e6b76011d1a742c32070761968","datavalue":{"value":"automated termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916212$A98935F1-0DC4-4532-8011-6D6DEC11AD6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"491e8725c8651263a210dc15dfabf985196b0a39","datavalue":{"value":"product types","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916212$3F29FCFA-2D77-4897-80E2-40AF1F23B0E6","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e84ba849f39966de2e974f600f062c98070e7d90","datavalue":{"value":"Q58001562","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$14E9204E-8DA5-4A10-9F99-A6F26EDBFDC9","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":"Q4916212$2A145C62-D7BF-4743-9F2E-EF309D7DA4A3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c02ff547cfaf7e165513cf8f07ad1a1e28baa67e","datavalue":{"value":{"entity-type":"item","numeric-id":1367078,"id":"Q1367078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$D203E8A7-A01A-42E6-B55D-C4B0DA54FF15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c6423ee1d4a298e225f00d1866983999d6c69656","datavalue":{"value":{"entity-type":"item","numeric-id":4501582,"id":"Q4501582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$B83CF042-ACFF-4625-A5DE-16FA47C789D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da959d914d1d83a9e3841136ad94d4a2ffd0893e","datavalue":{"value":{"entity-type":"item","numeric-id":4494365,"id":"Q4494365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$2F0E5374-8EF0-4CB6-BA62-F6DCE3CE28E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"050744ad710b2732fc1db2e9f7bd06de890ca43f","datavalue":{"value":{"entity-type":"item","numeric-id":4274979,"id":"Q4274979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$47CBF744-6AC0-4644-B421-F8ECA133D460","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36b355c034a15b6951cab8a2fb9dd01fb3be3dbf","datavalue":{"value":{"entity-type":"item","numeric-id":3477935,"id":"Q3477935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$E8144404-91D4-4BCD-8057-052721924DD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9f2f195c49df82c9cda56f240abd57e5287f8348","datavalue":{"value":{"entity-type":"item","numeric-id":1819575,"id":"Q1819575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$3892EEC4-EEC9-4775-A67B-9CED58019917","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b67f62053c0da9e304f60e65a89efe6ab3bb050","datavalue":{"value":{"entity-type":"item","numeric-id":1346629,"id":"Q1346629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$DEA129E5-F290-4DA9-8B0D-B8DF2F0D621C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3971ba2331f7aa9b95b29397d426f1fdd2e462a9","datavalue":{"value":{"entity-type":"item","numeric-id":5940917,"id":"Q5940917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$9D4F59D1-9091-488C-ACF6-1CFC8A803410","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e98a0291d6b416afdf61c3b8456fe8639369f4a5","datavalue":{"value":{"entity-type":"item","numeric-id":1190480,"id":"Q1190480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916212$F3CE9E62-BE0E-4508-9042-C3AE2E3B3D94","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bc38b5e7a331055a4ef4e65ad4e465cd01b54e89","datavalue":{"value":"https://doi.org/10.1016/s1571-0661(04)80551-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q4916212$4F720FB6-E438-4122-BD05-97F357C3A50F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4603636db39d6b9aff160294e390b97ecdd286b5","datavalue":{"value":"W2092505298","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916212$A2FC5927-405F-416E-B345-D0775927D9FE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81235c4d3f4c66b6911717e8cbf43cd34a5bdfea","datavalue":{"value":{"entity-type":"item","numeric-id":912594,"id":"Q912594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa5459caae6817e42a2919eca885d5e0d13f7e51","datavalue":{"value":{"amount":"+0.8119969367980957","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":"Q4916212$642F53BF-7222-4CF7-A4D2-55E52C0DCBCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26cb5cd464b164ea1acb873ebe4a85f44b92d6d2","datavalue":{"value":{"entity-type":"item","numeric-id":912589,"id":"Q912589"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ad46af9cc3abd1fa8ecf52667a5ae10e95ee23a3","datavalue":{"value":{"amount":"+0.7901213765144348","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":"Q4916212$602D7143-CBEC-45C0-A7A2-B946666E36AC","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":"a022cc1e8140312d1a5281c4e005148c813fe977","datavalue":{"value":{"amount":"+0.7783193588256836","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":"Q4916212$83DE100F-739C-41DD-87AB-8AAE319BE699","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b2ef1dfb8450e1a64b77276d877120e7c94cd7d","datavalue":{"value":{"entity-type":"item","numeric-id":4023948,"id":"Q4023948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"992d6de5861e9018d2423bd573f71f65d8fbf95e","datavalue":{"value":{"amount":"+0.7732345461845398","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":"Q4916212$1728BD0A-A1E7-4AC2-8C46-678D961DFF96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7dd57a5527789a549fb0c9bbc13052ba553d7ba3","datavalue":{"value":{"entity-type":"item","numeric-id":4202961,"id":"Q4202961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7eb34af399e469c79f844822d65a34ba3b1dfac","datavalue":{"value":{"amount":"+0.7719460725784302","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":"Q4916212$2B1625AE-DAB2-44ED-B784-398CE486E35C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On automating the extraction of programs from proofs using product types","badges":[]}}}}}