{"entities":{"Q1194249":{"pageid":1204998,"ns":120,"title":"Item:Q1194249","lastrevid":66830685,"modified":"2026-04-12T13:08:48Z","type":"item","id":"Q1194249","labels":{"en":{"language":"en","value":"On the adequacy of representing higher order intuitionistic logic as a pure type system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 64034"}},"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":"Q1194249$AB9ADBA7-DA2C-4BB6-9981-1693897C96B1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"24415640eddd0d3bafe290fd780ecf98a7f4d64c","datavalue":{"value":{"text":"On the adequacy of representing higher order intuitionistic logic as a pure type system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1194249$FBE4E420-4D91-47B2-96BC-6AF2CD935404","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c2ca8eb3701da7d849d9158799cedb4ef177240b","datavalue":{"value":"0763.03007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$60550C09-A7B0-4F35-8826-0764F47886B5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"16a1981d8b1f9284b14540550d3cfe8d9ff44891","datavalue":{"value":"10.1016/0168-0072(92)90044-Z","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$94914658-5296-4305-8ACF-BD5B94B3254F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2394892864430a7d655d06a6458e94fb8e590974","datavalue":{"value":{"entity-type":"item","numeric-id":1194248,"id":"Q1194248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$3C1375AC-831B-4E9D-8841-6151AC999F71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"647c63bfabe2cc5aa72008693495435e80f88915","datavalue":{"value":{"entity-type":"item","numeric-id":402116,"id":"Q402116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$65A676AA-C74C-4A18-BA20-FB968D650C4A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$FDBC32A7-4F2B-45B3-81B5-82BEB41F6492","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5fd62271fe98c7ff9916cafed51cf35315eeeb31","datavalue":{"value":{"time":"+1992-09-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1194249$E1A96012-5019-4F8F-8F36-C5981C3B3B5A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$2BFAC6AB-8D98-4A09-9CFB-6D4A4C20A6B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2337f934f367559a8ee0c48540aa4d52d0fa385a","datavalue":{"value":"03B20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$FA6ABF16-7610-477B-9161-66ADB91DDEDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$55A5C5AE-B2E8-4560-B6A7-4D1033DEED90","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"50d79cba1e04def17172b1d2c16da007528e2e80","datavalue":{"value":"64034","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$4BA72A88-F404-469A-A795-12AB18E645C0","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3c4c88b6c047cc3cb93785d00d698227a2ef545f","datavalue":{"value":"higher order many sorted intuitionistic predicate logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194249$5C0ABBA4-2B80-46B7-970C-045642DBF555","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aacdd9e6b1e081b5de4688ca768accb91a2c66bc","datavalue":{"value":"calculus of constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194249$3D4F3099-09A2-45A7-9B4C-568F28C42A52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f383f0654f5901fb84059190f1909ba97246c04f","datavalue":{"value":"pure type system","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194249$5A9216ED-55C0-493D-B04A-4E6E35A26BAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f8cd212e16e9535ba72e2d13114050e14cd03d2a","datavalue":{"value":"Curry-Howard-De Bruijn isomorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194249$F795FBA9-7DB3-44CF-AAE9-4C893A05CC2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"595a1e75b49a7c35cfd3caaaff3a4e298be5d31b","datavalue":{"value":"proof trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q1194249$97979338-CE7F-4E0A-9B63-B4CD4CA3CD78","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$6B7EDAF8-E404-495F-9C1C-07FEAA56013D","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":"Q1194249$1E47F3C9-272F-46B1-AAC0-CF08B3480276","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$E839D7E9-7A04-4956-8708-E6DD081FA60C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98f21a4a0099d31e158836c7dcfba6aa43c852ab","datavalue":{"value":{"entity-type":"item","numeric-id":3342534,"id":"Q3342534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$CBAA6D61-A611-4253-BDA1-01EF98DAD737","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$ED03FC40-16F5-46FC-BD7E-B8EB4DFD3A9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad80344fc1eac9869a64dbac310f2d1dda233df0","datavalue":{"value":{"entity-type":"item","numeric-id":4939698,"id":"Q4939698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$035649C8-868A-4225-B341-B7DEF0F316DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c9e886b9360a3e41cc1b6bf60219a57e89b7504","datavalue":{"value":{"entity-type":"item","numeric-id":4692468,"id":"Q4692468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$82A50930-4320-4BDE-A44C-F0AA1B0E3364","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1194249$36362ADE-00FB-4D65-B745-EE19E8C21A1D","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"6cc0322c0edc1e624e56b5599db7ef69fd433e37","datavalue":{"value":"Q126352769","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1194249$913DB80D-A938-4B26-B2E8-E72859200A09","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"380fe67206fa9f7f0a415ba641a43eb156d4dc86","datavalue":{"value":{"entity-type":"item","numeric-id":5390279,"id":"Q5390279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"af583d205585fa1819c281fb875ea37bb1ffbbff","datavalue":{"value":{"amount":"+0.9186816","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$FEC0387E-C942-4E1B-BE4B-2997C0DA7191","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a2a627e29f2871ae1ff628bc0545f5102ac3722","datavalue":{"value":{"entity-type":"item","numeric-id":3612441,"id":"Q3612441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8386cd6a135505947dec9abbc4dd5974a47e6c25","datavalue":{"value":{"amount":"+0.90935475","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$5D125D92-FF70-4F46-9441-842962E00A97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1cd34f784ebf777742449a1a890f3271c0fbdbe5","datavalue":{"value":{"entity-type":"item","numeric-id":2565990,"id":"Q2565990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a184928d06de88c763085c2e6fa266d28b4641b7","datavalue":{"value":{"amount":"+0.9078374","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$2E892C9E-C859-4AA2-985E-8B08E8A0368B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e63968eb3680f1e5453af52986bdc1b38147093","datavalue":{"value":{"entity-type":"item","numeric-id":4703134,"id":"Q4703134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f3808316c3da491999f960e663d6a297214d3b9","datavalue":{"value":{"amount":"+0.90620685","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$018D8E73-81FC-4D90-8066-11EA5ACCD5C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"371bdefbc7d26a872e6752b3d62fc9ba2e00e071","datavalue":{"value":{"entity-type":"item","numeric-id":3832535,"id":"Q3832535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc57301abb275facef229dc4a3fc49385866515a","datavalue":{"value":{"amount":"+0.9000215","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$C67A7C29-1B2E-4870-87FB-EC2616ECDAD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"920cea9b47420f3404cc2d0764270e98aa7d1cf3","datavalue":{"value":{"entity-type":"item","numeric-id":3995928,"id":"Q3995928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc57301abb275facef229dc4a3fc49385866515a","datavalue":{"value":{"amount":"+0.9000215","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$2BFADE54-8F45-4203-9BB1-8FC72B33DC67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"50f559e33bdae5d6031398bd74dad7b706db362e","datavalue":{"value":{"entity-type":"item","numeric-id":4282512,"id":"Q4282512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c280af2b9e5584ef81e7394e24440c8d6afe641","datavalue":{"value":{"amount":"+0.8939682","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$B802EF84-AC4A-430A-BA7F-1BA614009FF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cff221fdd8db17edfab39af5ce22245787dd86a","datavalue":{"value":{"entity-type":"item","numeric-id":1886324,"id":"Q1886324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c76ee986b1a3fce1e1a55ae181337fe2fd004f40","datavalue":{"value":{"amount":"+0.8909479","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$6FD2BC38-CC73-4D9A-9784-E25649EFDD3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a79efe2c6dbd42e36766761e062876f07ca1c2de","datavalue":{"value":{"entity-type":"item","numeric-id":4281475,"id":"Q4281475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1dcdcee94b424bdc7a83d18f7fcad97cbdeda9bc","datavalue":{"value":{"amount":"+0.8907827","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$48837DB5-516F-45A7-8492-5947979F3A54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6009f229da9cc183ad7bbbc5dd4ed923406f6b8e","datavalue":{"value":{"entity-type":"item","numeric-id":5862337,"id":"Q5862337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37ab3f5a13697dd5c6cc78cdff8a6cf673da8ebc","datavalue":{"value":{"amount":"+0.8890998","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1194249$9376317A-177A-4CC3-871C-E527ED067451","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"On the adequacy of representing higher order intuitionistic logic as a pure type system","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/On_the_adequacy_of_representing_higher_order_intuitionistic_logic_as_a_pure_type_system"}}}}}