{"entities":{"Q5408400":{"pageid":7437974,"ns":120,"title":"Item:Q5408400","lastrevid":51972023,"modified":"2026-01-20T16:09:18Z","type":"item","id":"Q5408400","labels":{"en":{"language":"en","value":"Combining proofs and programs in a dependently typed language"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6282410"}},"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":"Q5408400$12DE4B1A-7F0D-4801-99D3-859B84B9B7FE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e0e3429ae92ac9b46e6ded66b58a03ef2d1a2de5","datavalue":{"value":{"text":"Combining proofs and programs in a dependently typed language","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5408400$B4BFD4A1-D622-4736-8345-AA8555BC6C2D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"198a0f3ebe0598e8edb45e68d24a0a2e5a46557a","datavalue":{"value":"1284.68125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$E9AC4D02-D230-485A-8F96-D5F3864B30AF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"92184334fb54fa58bc5ba5a6de2e7abd408daac7","datavalue":{"value":"10.1145/2535838.2535883","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$50634A50-ADDB-4F2D-BA51-F66DDF3514C9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7865d4042300a36d5f610a5866166ce8e94d5d91","datavalue":{"value":{"entity-type":"item","numeric-id":4649381,"id":"Q4649381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$83E25970-85F7-4381-8802-ABCDFDF8C71B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a6f44d708e4aeb966dda281a5c72d40fc429c0e9","datavalue":{"value":{"entity-type":"item","numeric-id":2670833,"id":"Q2670833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$84652015-5BAA-43E0-B588-A4F0C1B79360","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fe52ffa1b7468cd548841738a45dc4a65b5c47ca","datavalue":{"value":{"entity-type":"item","numeric-id":2763692,"id":"Q2763692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$0DB26DBD-FF04-44E2-9A2C-CD43ED04C8DD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"640f3283bf4ebaf19f5992b18fbb1bf0f8463c2b","datavalue":{"value":{"entity-type":"item","numeric-id":5408394,"id":"Q5408394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$3D6AC75B-3658-4178-9F4B-E5CD71B850E1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d29d162184913e14034b04455ad3f441d2a1856b","datavalue":{"value":{"time":"+2014-04-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5408400$925AEBD6-8772-472C-A422-AE64C342DE98","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fec30692f6434b7f583708e9d4ee424c051e0bba","datavalue":{"value":"https://repository.upenn.edu/cis_reports/985","type":"string"},"datatype":"url"},"type":"statement","id":"Q5408400$5CA57121-8DF1-4396-8EE1-80E2BA7A789F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$96A5266E-90ED-4C26-AA00-4CA3F191CF88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$05089A67-7262-499E-BF96-B4B90B41EDED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$5AF2ACF1-98CE-42A1-8E8F-0DA45A949D66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$2C31FB3C-11F4-4A9E-97C4-C79998EB4912","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$347C51C9-CEC6-473F-8D95-5ABC7882F894","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$2885F55C-A642-4EF8-AF69-1DD4A5936C48","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"34491a000dce2a99f4b81cf212c74daffb365159","datavalue":{"value":"6282410","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$1173F536-FABB-4F1C-A7F8-23BF38E210BD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408400$AB730351-4854-4A79-851C-5FD20E5C58F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b3215a37f2f3e4759778d3eb8b23b9eede7c28f4","datavalue":{"value":"general recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408400$8F41066D-4A4C-4B28-9A1D-9F52D3BFA5DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408400$09B2E93C-7C34-4960-895B-8443DCD4773B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$8385A507-8000-460B-ACE9-002AA0CEE1D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$09056666-DEE7-43F2-A894-BEFFD6803268","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3b770a87ca9a9c88e8d7293f2ff0eb880186c71f","datavalue":{"value":{"entity-type":"item","numeric-id":21669,"id":"Q21669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$0DA9FB9F-002D-4E50-BB63-E3972BA2F154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a36bc1f7bbc81ffc389d921a198394ecc3bd746b","datavalue":{"value":{"entity-type":"item","numeric-id":23424,"id":"Q23424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$8A79C51A-366F-44C6-BA32-2AA1C6375295","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":"Q5408400$47A4A19C-0BB5-4676-A06C-F66E314776FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e74e65aea50b572ed5cc320d9d0d7a2d70ec494a","datavalue":{"value":{"entity-type":"item","numeric-id":21666,"id":"Q21666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$47053A2F-67EF-489F-BAA4-C5768853286C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4dfe52116eea178df8e98fcb66fd7e4802fcbfc","datavalue":{"value":{"entity-type":"item","numeric-id":24263,"id":"Q24263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408400$72903051-F93F-4E28-8976-0ACC51C6796F","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":"Q5408400$7248AEB5-9DB7-47C1-9D1F-1899AC860B98","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a554d6a2472722484c46a01beabc2eef4e995c8b","datavalue":{"value":"W2048536148","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408400$1657CCC1-5F67-4F94-8CFB-D6F8FC02F6DC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af4f211bb387809534c3a4f022fd139f46c066a8","datavalue":{"value":{"entity-type":"item","numeric-id":5191088,"id":"Q5191088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2627a57a14f1486b66c63e087c7151a50752bd64","datavalue":{"value":{"amount":"+0.7836742401123047","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":"Q5408400$9D426FC0-6B06-4DB7-A258-7085F3CF3EF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"881379a3fa914a298d877b279ed01bf7e4e2ddbc","datavalue":{"value":{"entity-type":"item","numeric-id":3086789,"id":"Q3086789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"152c380494cb58fe4bdea1f5d392f2896a9e078d","datavalue":{"value":{"amount":"+0.7647117376327515","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":"Q5408400$264015E4-34C9-43C6-83F4-A4D56890661E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"968ef3c413e5fe02e2d496a820a84be2c7737a1a","datavalue":{"value":{"entity-type":"item","numeric-id":5255080,"id":"Q5255080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f1cb1de27f4085ca745871e382b627bb7188ddd","datavalue":{"value":{"amount":"+0.7457249760627747","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":"Q5408400$0C9BE4E9-E5E1-466B-9B99-6B3BE2B8950C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d790df35eefe2e96f852fbd8027802e91f7f931a","datavalue":{"value":{"entity-type":"item","numeric-id":5491909,"id":"Q5491909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b00dd96dfb90dc6cb93660ab63d5f3392a19a1d8","datavalue":{"value":{"amount":"+0.7441160082817078","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":"Q5408400$D9A025EF-C427-43F4-9A13-04C42A95D29F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"357860675d9d6383009814e1650bf925597a610f","datavalue":{"value":{"entity-type":"item","numeric-id":4819651,"id":"Q4819651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a3bb8b5c134772cb15af60f2378b98b3989d7ce","datavalue":{"value":{"amount":"+0.7309068441390991","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":"Q5408400$E106476B-E305-479E-98FA-F9C7757DD392","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5408400","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5408400"}}}}}