{"entities":{"Q5300899":{"pageid":7330473,"ns":120,"title":"Item:Q5300899","lastrevid":51761546,"modified":"2026-01-19T21:40:59Z","type":"item","id":"Q5300899","labels":{"en":{"language":"en","value":"A type-checking algorithm for Martin-L\u00f6f type theory with subtyping based on normalisation by evaluation"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6182518"}},"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":"Q5300899$F47DE903-079B-48BF-995E-CBDC62F2B2DA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e919133a688419fa6e49851c536dd0f6a42b2de8","datavalue":{"value":{"text":"A Type-Checking Algorithm for Martin-L\u00f6f Type Theory with Subtyping Based on Normalisation by Evaluation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5300899$5729AED1-181B-4DD0-B56A-B8CE46054658","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"59ba65f4ab921c76924161ef7890f2bd9f8aa69e","datavalue":{"value":"1273.03106","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5300899$393F2FDE-381F-4FD8-AF32-BC01723CBB47","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"089572f4e620ea429b2cd12287a14fc81defd38f","datavalue":{"value":"10.1007/978-3-642-38946-7_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5300899$41B30B7E-2913-4ECE-8BA4-407343B5918B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"55e641319c011b54f0c69b6edb09640a3dbb847a","datavalue":{"value":{"entity-type":"item","numeric-id":1744422,"id":"Q1744422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5300899$E9B74485-7D30-4C76-B8B3-3AA4288B1AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"09573ab70c9d986235750625015542077d5f5980","datavalue":{"value":{"entity-type":"item","numeric-id":1744421,"id":"Q1744421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5300899$A2F35A1A-65BA-4D7D-8527-48D96F46535F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5300899$D3C9EAF1-1F02-42C6-AEC7-F7FA8BEC2467","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b3abb5fb4ae7972a30f51c8d6a09a9ae6d81d017","datavalue":{"value":{"time":"+2013-06-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5300899$361489AE-94E4-47EB-B222-22BCC9A9B092","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5300899$68D9F5A3-A239-4223-A0DD-BEF04C4950DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3068729a394ad5bf58a1a3e5b5d24254d962e1a7","datavalue":{"value":"03F55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5300899$B7D67301-A987-4F06-B01B-7DCF88ECED2A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8e1e4efdc6493dbbabbb516131b17fc328de4411","datavalue":{"value":"6182518","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5300899$06D01A0A-BA86-4DBA-8535-E15F8AC02481","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"33775f26030d071074f6e677c78b2fdd4159a0c9","datavalue":{"value":"Martin-L\u00f6f's type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5300899$A86256CD-CD74-497D-917A-FBC4F504680B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543b5b6936751d447dfb75294948e5dafde0cec3","datavalue":{"value":"subtyping","type":"string"},"datatype":"string"},"type":"statement","id":"Q5300899$3DB7C015-35EE-42A5-B3A0-D3A7CEEC7832","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"486173fdea484958e371bcc478b16d274811d71a","datavalue":{"value":"intuitionistic type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5300899$EE476F8F-D969-4BB2-8C0A-DB8F232C931E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ba5620c65b3b1616ab8ae31e5468b0e08272974","datavalue":{"value":"type checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q5300899$2F6EA9EA-7B86-4736-9E81-9D88A543D7C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb038c8b7f7ce216a311d4c4251554bd66a91dc8","datavalue":{"value":"normalisation by evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5300899$AE985EA8-CC7C-4E7A-847A-218222957F2A","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":"Q5300899$A0D6CD21-012F-41AE-9FE2-E6B096BC6BF9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1c5c83b7e799d6afe0141782db2cb8665b43e18e","datavalue":{"value":"https://doi.org/10.1007/978-3-642-38946-7_12","type":"string"},"datatype":"url"},"type":"statement","id":"Q5300899$504F9D7D-0DDF-4EDE-9578-BC7A980A45FE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b2a8fbe6b3257615d5d25beed78ca6dc64a34bb1","datavalue":{"value":"W2184421553","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5300899$E8063E69-C8BF-41A7-B356-DC041FD7BAEE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"953159312b7424abe16acfaed309cd34802f4340","datavalue":{"value":{"entity-type":"item","numeric-id":5262927,"id":"Q5262927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9bc817156df74f8bb2fab283f01c1b4999d2239","datavalue":{"value":{"amount":"+0.8306096792221069","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":"Q5300899$CC5B074D-5D54-4751-B870-FC520BFC2CF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e703c12462fa3c0b4409c4b169c76db5afa7ad9a","datavalue":{"value":{"entity-type":"item","numeric-id":4500363,"id":"Q4500363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19fe9bcb5adb0ff633be8b0caddb1469ef9d139e","datavalue":{"value":{"amount":"+0.7662056684494019","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":"Q5300899$F8ECC2D1-8E3A-4D77-998F-6730C3B01F55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"918f2781deb536cb7abada9a9087642f80fd8cef","datavalue":{"value":{"entity-type":"item","numeric-id":4699295,"id":"Q4699295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9483a992816a4b6f0ba0865772341872f5f4ce1c","datavalue":{"value":{"amount":"+0.7654258012771606","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":"Q5300899$6E30E6F4-22DA-4AF0-A68B-52380B0712BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"53cdad27cec952b4a067ef178a26a1ca88d8989b","datavalue":{"value":{"entity-type":"item","numeric-id":2841227,"id":"Q2841227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce116239889531fe777ef7e6f88b94b5c2d43ead","datavalue":{"value":{"amount":"+0.7631782293319702","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":"Q5300899$23E8B364-EB14-4AA9-B09D-15C1F654789D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3cd02653a0f5288cbd7583c98894a5128fb01b60","datavalue":{"value":{"entity-type":"item","numeric-id":5958760,"id":"Q5958760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b56bf84eb896e69f3ec2efdee4d5869716ceaef8","datavalue":{"value":{"amount":"+0.7541555762290955","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":"Q5300899$87737A73-0F6F-4FAF-8994-97385F790727","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5300899","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5300899"}}}}}