{"entities":{"Q5145348":{"pageid":7174919,"ns":120,"title":"Item:Q5145348","lastrevid":58456629,"modified":"2026-04-05T07:30:25Z","type":"item","id":"Q5145348","labels":{"en":{"language":"en","value":"A sequent calculus with dependent types for classical arithmetic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7298797"}},"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":"Q5145348$227D5AF8-45CB-4A3A-9CAA-7D1772FF8E74","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dd9d9c99a5adde41f528639991379587213a273f","datavalue":{"value":{"text":"A sequent calculus with dependent types for classical arithmetic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5145348$B484A5D9-F81A-43C0-AC78-3910644BE843","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4a4b0a67f3246e9e0bd9df55361a6aeb1b5dea18","datavalue":{"value":"1453.03010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145348$8C20EFEC-13C4-40BE-A005-0E3FA02689E9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"46f5d75b91e88aa1b2e40091d382e8e87829fa89","datavalue":{"value":"10.1145/3209108.3209199","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145348$3D7AAE49-3C4B-41C6-A8F4-4A027BF22CFD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"32d25e6dfe9704fbad90bb3edf4deb2c92e5bbbb","datavalue":{"value":{"entity-type":"item","numeric-id":1652989,"id":"Q1652989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145348$CB34C162-9FF7-4728-883C-2CEBF2D7E189","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ee82b0c640d35f6663be3f8a5187d8cc540da0b3","datavalue":{"value":{"entity-type":"item","numeric-id":5145269,"id":"Q5145269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5145348$55AC7E9A-E5E4-4DDC-8CEC-E397B00BB8B8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"233394734482eba32ed4ee15da745b1ac2b96149","datavalue":{"value":{"time":"+2021-01-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5145348$8F1A80CA-C13F-49CA-B3A3-E64A9D03BF32","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cfafd30d0910cab71e868169a25619d1efa196a3","datavalue":{"value":"https://arxiv.org/abs/1805.09542","type":"string"},"datatype":"url"},"type":"statement","id":"Q5145348$39D9926D-C97A-4785-A4AE-3921B674B329","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145348$0D430790-2DA7-4AE2-826A-60752CA4642A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c15287dbb142f8dc10ab92a91b8457ac3c169cd3","datavalue":{"value":"03F30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145348$BF96DD64-44C7-4685-8279-1ED70B3BE784","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1064c909d8b86b3ba4bf91ba9b0b08c334ade997","datavalue":{"value":"7298797","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145348$268EDD4D-9733-4C41-BDEE-CF769048E192","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c441b3dee73de3d269547b272c1f7cdc085a924","datavalue":{"value":"Curry-Howard","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$90696E82-1580-45F1-B37B-1229D448F0D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"745fec169852dccc23ff4583447d1e5556dd5648","datavalue":{"value":"classical arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$97B804BB-2547-4069-87E5-A56F4E737B36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3329e5ddc19ec41605ea21e54e688588faa574a2","datavalue":{"value":"classical realizability","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$66D86867-62B2-46E0-A6FC-7E2FADB4E4D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b554279a6b3d2763e31e966664501fdd51a92def","datavalue":{"value":"dependent choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$CADA19D8-B091-495F-B93B-342A21B0D7D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$DA0001C7-B2E4-4CD9-81D2-B6B7F34D2D02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$69BD2767-5B0B-4E71-A85D-B65B28B46FDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73726f805dc1edf70c39fc6c6a87bf6a1a269b24","datavalue":{"value":"side effects","type":"string"},"datatype":"string"},"type":"statement","id":"Q5145348$0AB70A3A-8E32-48BD-8A7D-1DB68D0A0302","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":"Q5145348$8312CD61-2494-4FF0-90C3-C7A765C961DF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c2aba2ec5c824908f839fad35955a5fa1183bd92","datavalue":{"value":"W2786132250","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5145348$68B36E4A-1FFA-4341-81E8-4F2B87D1B3D1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e48efc657fbe12f180d5e73f6fa3735cf8cd1bc3","datavalue":{"value":{"entity-type":"item","numeric-id":2988668,"id":"Q2988668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1953f5cf477df7886c02fa318f1a5e77afb58c53","datavalue":{"value":{"amount":"+0.7969118356704712","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":"Q5145348$FEED8BB0-5476-41AB-A273-1EE0DDBD16BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee5bc9c6b51c4631c5a8db5b114549e49c9d5594","datavalue":{"value":{"entity-type":"item","numeric-id":1652990,"id":"Q1652990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2641ee402a67d81daa6da669e02894c11ae1f450","datavalue":{"value":{"amount":"+0.7653531432151794","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":"Q5145348$93F6518D-02B7-400E-95BD-847C7DC8A075","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52a879a36070095bb20e1d6cbced7ef6874943e1","datavalue":{"value":{"entity-type":"item","numeric-id":1884884,"id":"Q1884884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3766b27b56a16ab9280337699adde82d8aa83315","datavalue":{"value":{"amount":"+0.7604460120201111","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":"Q5145348$364D7D32-9B59-4142-8D7B-53740C8C49E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dba42c8b31e2765c0a227cbcb4e2d0116b353eed","datavalue":{"value":{"entity-type":"item","numeric-id":2986812,"id":"Q2986812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bf78a7a845839b9a6f383b061909e25c66cb539","datavalue":{"value":{"amount":"+0.7503553628921509","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":"Q5145348$9C446D09-F9AC-46E7-8FCE-AABB89372F07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51bb6c0a493875b35b3625aaa97838d37e568702","datavalue":{"value":{"entity-type":"item","numeric-id":5387838,"id":"Q5387838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4f64860a53dc423813504471c4edea6139639f49","datavalue":{"value":{"amount":"+0.7360435724258423","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":"Q5145348$4D358DF1-1324-486F-981C-4210B8EFF308","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5145348","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5145348"}}}}}