{"entities":{"Q4849649":{"pageid":6879229,"ns":120,"title":"Item:Q4849649","lastrevid":90905675,"modified":"2026-06-04T21:44:30Z","type":"item","id":"Q4849649","labels":{"en":{"language":"en","value":"Efficient Verified Programs in a Type Theory with Mixed Constructivity"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 802495"}},"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":"Q4849649$39B4E3B6-4E53-42AF-8F4D-3931057B3555","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ac8faa9587318e698085998a61b1883ae195510e","datavalue":{"value":{"text":"Efficient Verified Programs in a Type Theory with Mixed Constructivity","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4849649$1D4D36FD-76E9-4EEA-80CB-A4A4E15B7E5D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"48815d1293a0a837bc24e25da154532db35dcca7","datavalue":{"value":"0829.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$1C8FF659-84D3-45DD-AE80-18D569376D07","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3fe9d074de57a72c9505a3a766754150a85b8908","datavalue":{"value":{"entity-type":"item","numeric-id":4340539,"id":"Q4340539"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4849649$4532A834-74A7-4FEF-A602-BFC21E9EA430","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b12e332ffe60310d8fb0fe514e5f371c7ab5bea2","datavalue":{"value":{"time":"+1995-10-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4849649$0E7495C9-4692-444B-9559-41AFD4E57CC0","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$50ED576D-49D7-4803-B5EF-A62AC7AD9B61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$FC4BBEB8-B816-4A7A-B461-559F29A4822B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$7B2FEEEA-F470-447D-AC65-5D09524893E8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1e1b64fb740d2aca82622407963f77848634fa86","datavalue":{"value":"802495","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$86624DA4-8D51-45F0-ADA3-DD3589E9F31D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$22E96E22-841D-4250-BE56-AA75738840BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"502560d82f734e6a9be2e2c1123ac857af165e90","datavalue":{"value":"verified programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$7B5BEB20-0A6E-45CA-8096-60484BCD7144","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d450f4b3083fe34d24db452ee74b92106c27a96e","datavalue":{"value":"intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$874546B7-04E3-445B-B236-353A2166EDE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b902f2f025c0c986ef0fe1d8152327a77121bc6e","datavalue":{"value":"mixed constructivity","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$D454E852-82C3-4297-9D77-311DD2A00235","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6c5efd37e6d1917f93b6972913b3d19dba9b2e05","datavalue":{"value":"evidence semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$0BC5A507-01BE-45BE-BA57-F4DF1BB0ADB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b39bcd33ba55d4227ecae1456f6e1430405ab2d","datavalue":{"value":"programming logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$C6E19FFD-3EB2-4188-BB83-24535341A580","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f182e86329a34e1b4cc75d54bcc34cbb69c421c6","datavalue":{"value":"typed \\(\\lambda\\)-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$2FD06BC2-80D3-4014-90D2-0C14BD34D867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51802126f63d5102d578f2858428d5d0f09da73b","datavalue":{"value":"denotational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4849649$EC459455-8EEB-4C35-B747-D0E95CE9F590","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":"Q4849649$26105796-585E-49CB-868C-EF26D01350D1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9b111709d4eac02100eb663a1bb1ffeb2d98e98c","datavalue":{"value":"https://doi.org/10.1093/logcom/5.5.669","type":"string"},"datatype":"url"},"type":"statement","id":"Q4849649$182599BE-14F6-4211-B305-B89D03B3D508","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2aeecff5a784c1d78758143ae7e34bc2c680878d","datavalue":{"value":"W2034260705","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$C1B1F88A-AE25-4FA1-BB9A-FD5E5EBC7AA5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"014e212b753c90c08ce2c44fe3b4a007aa7b3bf4","datavalue":{"value":"10.1093/LOGCOM/5.5.669","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4849649$BBDC7D18-FC49-4D18-B503-6E21460FEFC1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa8d52c7593ff0d29df32ff6422f7fbff9926316","datavalue":{"value":{"entity-type":"item","numeric-id":2866340,"id":"Q2866340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ce6e605f26be548737a645bbbd2342a9a6ed351","datavalue":{"value":{"amount":"+0.90972304","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$492BEB51-253A-45C0-84A2-3F0DC930A064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fcaefb3b70d25c064a9f1741c555ddcca94f1c78","datavalue":{"value":{"entity-type":"item","numeric-id":953533,"id":"Q953533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3473cd4243591743c5e4d034d9c8fad4415b2b6","datavalue":{"value":{"amount":"+0.9082732","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$2169AE93-D309-45A2-A210-DADBFAF6B13D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f34b64a349c4606601cddb539d3c1e869aecca7","datavalue":{"value":{"entity-type":"item","numeric-id":5261537,"id":"Q5261537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"605ccc5524b271ab164fec226af58795b4b7629d","datavalue":{"value":{"amount":"+0.90632284","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$831FDB87-960B-4630-A007-B3A4E8611314","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb234b5551cae0af9257fe3eff72cf077bed7f0a","datavalue":{"value":{"entity-type":"item","numeric-id":4461768,"id":"Q4461768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53c4d4645b6edd54e4f9d11ab81aa618af9784c1","datavalue":{"value":{"amount":"+0.903581","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$DC4308FE-3DB5-4468-B7C1-D3C9347F0BBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"39325d0e1c9e9f212d366c917feb047ff194c278","datavalue":{"value":{"entity-type":"item","numeric-id":4015951,"id":"Q4015951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b03c5d72880ff2110588792f84f9956d2cffa481","datavalue":{"value":{"amount":"+0.89826405","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$1FFA20FA-B347-4ABB-9303-FC31E45D3536","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea5ab6fce12ac3d4a28e92f06d387b18aea79387","datavalue":{"value":{"entity-type":"item","numeric-id":4312490,"id":"Q4312490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9a563c07079458cc5a5a9b160d782cb6b50a8118","datavalue":{"value":{"amount":"+0.8976336","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$D8C53506-48AF-4F01-9BD8-9E0F58BEAA1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b54e411a1fa403497ad92093317d1d515a51d832","datavalue":{"value":{"entity-type":"item","numeric-id":5309417,"id":"Q5309417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d5054a4f9f56c67bd00c7b2495b78816cc115555","datavalue":{"value":{"amount":"+0.89739656","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$C54AE949-A3E4-49A0-BA43-A5BB32773626","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e624eff166aef0fa88875321d9d439e22120898","datavalue":{"value":{"entity-type":"item","numeric-id":2949206,"id":"Q2949206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f95a6841d0cf13216392bcf69afca1da7a1523ad","datavalue":{"value":{"amount":"+0.8960371","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4849649$03439335-0AE2-4E44-BADC-3BAB4339F50A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4849649$6E33D419-A9F8-468D-AA2A-8E2600D86A7D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Efficient Verified Programs in a Type Theory with Mixed Constructivity","badges":[]}}}}}