{"entities":{"Q5875425":{"pageid":7904976,"ns":120,"title":"Item:Q5875425","lastrevid":93267509,"modified":"2026-06-05T04:06:29Z","type":"item","id":"Q5875425","labels":{"en":{"language":"en","value":"A certifying extraction with time bounds from Coq to call-by-value   $\\lambda$-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7649966"}},"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":"Q5875425$88CEBE99-BF46-4AEE-AE3F-A5EBA4432790","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c7e7e54e22918a5af75f6588d5e6c4a6d7874c28","datavalue":{"value":{"entity-type":"item","numeric-id":1687734,"id":"Q1687734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875425$B86DF2D3-3418-4E8B-8E42-CA96515EA669","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b01c8659d438f464113b8c77203eb524f1a37c70","datavalue":{"value":{"entity-type":"item","numeric-id":2209540,"id":"Q2209540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875425$26D2C746-B910-4860-BF51-6B3DCBD55642","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6695abe38664d65c38747de7b5fe54d9caa92dea","datavalue":{"value":{"time":"+2023-02-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":"Q5875425$84BA97E1-2C01-40C8-BB9E-225E6ECFB697","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b7d067a18d4266a85209dbb7fc35ddfaf64d34d1","datavalue":{"value":"https://arxiv.org/abs/1904.11818","type":"string"},"datatype":"url"},"type":"statement","id":"Q5875425$526CD20D-4156-427C-89E1-228A7902497A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875425$155B12BF-F95A-490B-B1F0-E9C21B2A8FC3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4a08fdff39dcb13e51182b56722944dcfb8c1bfd","datavalue":{"value":"7649966","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875425$EAFF9883-8972-4441-BCB7-9376D4EB730C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0023655cb58cff7dfa4411698356799107789a6f","datavalue":{"value":"call-by-value","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875425$11C25443-97DE-48B2-9746-2934EA8479C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14d84a39f7d277d59bd9e0565999aa9a6eed7d1c","datavalue":{"value":"\\(\\lambda\\) calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875425$12FDE91B-830C-418C-A82E-968CE841D634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875425$5229F44C-1064-4C09-8E88-B56ACFE10970","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875425$7F1B23BC-2B86-421C-8666-5F85A380D18A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aa8f407250beeb2bd358124707dee09a1fc727db","datavalue":{"value":"extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875425$C4B1189C-C019-4AB3-B3E4-27260DEC501B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4f2891ec95ee556b0ac2cc2dddee3d77811bd94","datavalue":{"value":"computability","type":"string"},"datatype":"string"},"type":"statement","id":"Q5875425$5F25919B-92BB-4A4D-B5DF-8FD7C22B6F76","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c299164581226a4d9e689eff045a50090a5543b0","datavalue":{"value":{"entity-type":"item","numeric-id":39285,"id":"Q39285"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5875425$1B9A37A9-95AC-4A37-A73B-4618B148AAF2","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":"Q5875425$928BF1F8-BA37-4F4B-B0B0-1394A0F93413","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":"Q5875425$D0FECF1E-89BC-40AD-8C22-A9EE0AD57591","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":"Q5875425$A277B24E-691E-489E-83AB-5025228EBDE0","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":"Q5875425$552D0BCD-02AA-43CF-A611-A445162173FB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"aba9671e9d7ee4f4c7f66af9a34c0cc34ab2e2ea","datavalue":{"value":"W4311008361","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875425$90212E29-D258-4749-8ACC-A43F8EE152B4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7a0dc1836eae7ec8515c7f4400bdf55f3a97b961","datavalue":{"value":"10.4230/LIPICS.ITP.2019.17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5875425$F429AA16-166F-43AB-9FCA-85B1D7EC5145","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7f801aafcc86381b3719b2d0e06449667a434e36","datavalue":{"value":{"text":"A certifying extraction with time bounds from Coq to call-by-value   $\\lambda$-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5875425$A52A9622-5E55-476B-806A-16A1F80F38AB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A certifying extraction with time bounds from Coq to call-by-value $\\lambda$-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_certifying_extraction_with_time_bounds_from_Coq_to_call-by-value_$%5Clambda$-calculus"}}}}}