{"entities":{"Q3003322":{"pageid":3014046,"ns":120,"title":"Item:Q3003322","lastrevid":51254189,"modified":"2026-01-17T11:33:10Z","type":"item","id":"Q3003322","labels":{"en":{"language":"en","value":"A modular type-checking algorithm for type theory with singleton types and proof irrelevance"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5900073"}},"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":"Q3003322$91DE8951-7E80-4919-B24C-A83B0F9491CD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"06f40b0ea360e730267e93e7210277334806eab1","datavalue":{"value":{"text":"A Modular Type-checking algorithm for Type Theory with Singleton Types and Proof Irrelevance","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3003322$6FB978CC-1704-47E6-A2B0-AC4864310343","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0a9b5cccfaafeb1e6756b3d88efacbabd5ab5294","datavalue":{"value":"1213.68199","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003322$0F195B29-4ED0-4473-8B1E-7A9DA9967234","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ff2ef30eb29dc0f6dc3edd9e7f01deec456e93cd","datavalue":{"value":"10.2168/LMCS-7(2:4)2011","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003322$637A3702-278E-42A1-9EBC-5AF44996A9DC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9fd295c773add0c694cee3f65e8e7cf93dc4bc27","datavalue":{"value":{"entity-type":"item","numeric-id":923882,"id":"Q923882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003322$200E1FD7-58C0-4828-8A71-CB22AC64E603","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5aad179d365c253d181fa8115a831f46e7923370","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003322$1FCA92C6-B415-47A4-9490-E25A211C137C","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":"Q3003322$DC717637-C3BF-4CC5-BDA2-94575D1CAE5C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003322$202761E7-5C2C-4704-A7DA-8A145D32E354","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d0d41ce3332fcf97fd23ad798d4a05a02b8284bd","datavalue":{"value":{"time":"+2011-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3003322$11138751-44FD-4C6D-91C3-236AA143F0C1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003322$535FBCEA-0C0F-4ED5-99E3-F45E8BA32F8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003322$937DAB04-62AF-44AA-A8C7-F29F7212FEBF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ffbddd0ca3f4a2b855e7b2cfffa34795db848ef5","datavalue":{"value":"5900073","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003322$9AB6240D-28C3-4435-98F5-8E01499087FB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003322$35F6A591-0138-4769-99F0-BE0D913C4FE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca5e78b438b6b1c09f22af7529224da8edd3a394","datavalue":{"value":"type-checking","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003322$9A9C6711-A33C-4448-A80C-23BD4F299F20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2db2592bddc30f2c314c26f3465e01aa7200f3a1","datavalue":{"value":"normalisation-by-evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003322$0414406B-164C-4DF2-B448-E9014F60178E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bcd490e3b7e6631b271c94b30df463e7a259d332","datavalue":{"value":"singleton types","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003322$8B4A8447-6456-4C3B-998F-703DBB1D4D5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fda5d8057392e50193b0eca80d9562ae727873ec","datavalue":{"value":"proof irrelevance","type":"string"},"datatype":"string"},"type":"statement","id":"Q3003322$11F103DF-51C0-4852-A6D7-0B3467A49CF7","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":"Q3003322$802DC726-13D3-4BD9-8745-79D926A04E5C","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":"Q3003322$C08A4A4F-A0C1-4209-BB31-ADDDA54C92F9","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":"Q3003322$F6E6A533-2CC1-4EE8-954E-36FD53BD7388","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":"Q3003322$9D0E9D03-9340-4D62-B4D4-BAE40B0E0285","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"595380fb5f71ee9bc16bd62600d04dd487c01c89","datavalue":{"value":"https://doi.org/10.2168/lmcs-7(2:4)2011","type":"string"},"datatype":"url"},"type":"statement","id":"Q3003322$22C068F7-ED30-452C-863E-106EBD3ADE6C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"81823b914b96c49acee9c33bfc5015af195eccb0","datavalue":{"value":"W2951383623","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003322$DAED3BB5-EC89-40D5-9DF1-919783861656","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf6171f0b09d240cdab1c5988ac08fee2e637217","datavalue":{"value":{"entity-type":"item","numeric-id":3637183,"id":"Q3637183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b242f90eb6234418c4f2f72a881d55c5c3ddfafa","datavalue":{"value":{"amount":"+0.9999992847442628","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":"Q3003322$5424C26A-2EB6-4533-B1A0-D692B371376B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71ebe4ddd848408e9a3abdf05ed75657754d1412","datavalue":{"value":{"entity-type":"item","numeric-id":5277760,"id":"Q5277760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03d7507902ac043721dbb7a8a04319d73cef4910","datavalue":{"value":{"amount":"+0.749088704586029","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":"Q3003322$2840A404-CE49-4992-A3FE-23E85E6107C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b180fd7c37aca86db24433ac508ad2c0acfe7e62","datavalue":{"value":{"entity-type":"item","numeric-id":4012882,"id":"Q4012882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ec7f4b2530c422934627ce52c3d1b42119e4cb6","datavalue":{"value":{"amount":"+0.7395480871200562","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":"Q3003322$ADFAF3A3-DDE2-459A-9CAA-C75AC882802A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a16a5f952fe65580ad3102001ed35bf577f03a9a","datavalue":{"value":{"entity-type":"item","numeric-id":5028472,"id":"Q5028472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8ec7f4b2530c422934627ce52c3d1b42119e4cb6","datavalue":{"value":{"amount":"+0.7395480871200562","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":"Q3003322$08F0DE7B-5793-46DA-AF78-77C71D47CE84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac0e6455d64c974c18e666d579868b607d74d057","datavalue":{"value":{"entity-type":"item","numeric-id":5166618,"id":"Q5166618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a490f39a09212f2c5ba4661203f4b512c1cc86f9","datavalue":{"value":{"amount":"+0.7388140559196472","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":"Q3003322$B11AEBFB-6E64-4D08-9AFA-AC16A97BCB97","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3003322","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3003322"}}}}}