{"entities":{"Q3637183":{"pageid":5667089,"ns":120,"title":"Item:Q3637183","lastrevid":50704211,"modified":"2026-01-14T21:02:05Z","type":"item","id":"Q3637183","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 5576316"}},"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":"Q3637183$D774BB24-0A69-438C-9581-C14D33FCE393","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"824de59008ed4048af7b6a4e40c070aa8cac6961","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":"Q3637183$CE36F25C-8C86-497E-9928-15A93B2FC326","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"65664758d88e8f08a10d986205f8d2bad9d4a5d1","datavalue":{"value":"1246.03025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$31F6B342-2E50-4DBB-81E3-03A1BAF3D7E4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c9ea2f6b99172a396fb4cf7a07d5b1c4220b35c7","datavalue":{"value":"10.1007/978-3-642-02273-9_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$5F439BCF-AEFC-4773-B913-92E26EB329E3","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":"Q3637183$065996FA-90C4-440D-9214-6A782D42B99B","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":"Q3637183$FC314E92-D224-4165-A50C-F0DBA1951F7B","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":"Q3637183$B3392C15-9492-45D6-8918-8B7713FABA77","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":"Q3637183$FE4F4785-BB48-4658-BAE5-9DC3AA1A25B0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"94035e3f051d88ae4ad052aa0269faba85e94c5a","datavalue":{"value":{"time":"+2009-07-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3637183$138C864F-BC44-49FE-B5DF-35609AF912D9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$F80BD94F-4F72-4139-AD06-651A7AC65ECD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$619B98C4-7F10-443B-8B36-DB5B2A553E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$3DDA652A-5F20-48D1-96A5-41625D0E2186","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5ccd99ff4a306bf542aa1ddefb3c4f99dd72c11c","datavalue":{"value":"5576316","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$95222CA0-1CA0-4B89-B823-91BD4CCDC31A","rank":"normal"}],"P1463":[{"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":"Q3637183$0140F752-E22E-434E-B7DA-FA01D9AB4A5D","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":"Q3637183$4ABFB544-EE75-46D0-BCBB-09D35D9B3BF4","rank":"normal"},{"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":"Q3637183$5B38B86F-6FCE-432F-BB9B-76CABD251AB0","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":"Q3637183$2005428C-5516-461D-A3B8-DE30F0BC5CC1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2fb4b3548c91c3e1f3aeae8d44d680f1e40a1261","datavalue":{"value":"https://doi.org/10.1007/978-3-642-02273-9_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q3637183$F88174D4-FB61-4DF2-B4B5-2248679BA1C8","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"696d9ca427a1f79f91480cd52880ec49dd49db2b","datavalue":{"value":"W1690628218","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637183$00591A43-E7D4-4642-A3F5-0039C63A3C48","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc9da8b27e8c6da641f5262b1040f7a5bd1721a1","datavalue":{"value":{"entity-type":"item","numeric-id":5262927,"id":"Q5262927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$8834D72A-BFDC-45F0-BDAF-08A013BBB9F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7d336268e40135c3453860ef42d03950683322d","datavalue":{"value":{"entity-type":"item","numeric-id":5458424,"id":"Q5458424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$66156141-0F4E-4FEF-A185-746406AD258E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75ea65729b1033e784ad198279fc14710fe85dc0","datavalue":{"value":{"entity-type":"item","numeric-id":3521979,"id":"Q3521979"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$2783FBCC-FCB5-40F1-B592-F36E0C1A4679","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42678821b5903d8d124dcb34366f2cb77d790e5b","datavalue":{"value":{"entity-type":"item","numeric-id":3003322,"id":"Q3003322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$77B278EF-961F-43D8-9CE5-B9E510D5BD28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba169da5300e1854434b7f89c8efeea407859e4f","datavalue":{"value":{"entity-type":"item","numeric-id":4818938,"id":"Q4818938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$E4D2A3DC-CB7B-4541-B331-1B9954A04640","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eff1fd92245df38d7ffeae1e590de1b0d5007c30","datavalue":{"value":{"entity-type":"item","numeric-id":4474826,"id":"Q4474826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$03D57708-5D93-4798-A6E1-6A278D7538A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fdc692fbbee7be9789734e7cf9dcc396f1f0927","datavalue":{"value":{"entity-type":"item","numeric-id":4823804,"id":"Q4823804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$61A09F3F-8310-4E56-A4FC-E8F771061BF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5adae15f6654acfbcf7621f32cd882969fbf6d8f","datavalue":{"value":{"entity-type":"item","numeric-id":1096716,"id":"Q1096716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$8A2D6FAC-4430-4CDD-9D5F-50C41B32DCB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6224dd9008c6167ab2abbf67da65d1f726ff5d94","datavalue":{"value":{"entity-type":"item","numeric-id":1916364,"id":"Q1916364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$A6D75265-3ED1-4056-87ED-C20CD5391846","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3715e78f290cd3087a3394a679a7aadcb0ddba8","datavalue":{"value":{"entity-type":"item","numeric-id":4681364,"id":"Q4681364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$AAA7A3BD-6C24-4C40-8D2E-5603CD4E4E1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"364525b70d80e5ad032dd4bcb752b39f36195669","datavalue":{"value":{"entity-type":"item","numeric-id":4508246,"id":"Q4508246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$EEC7C313-F198-4145-B86E-04860CD21070","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"901ba45472e1a0a3be8b2e40215973355027ef09","datavalue":{"value":{"entity-type":"item","numeric-id":2949209,"id":"Q2949209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$9C8FE9B0-C377-4B71-B0E0-F856D5CD5023","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$F9265F90-1791-48FF-A395-84C78E3C3B23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6063e4a144bafe1447ae8b10555347d26c418f1d","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$D0214D90-C455-493D-9DAE-4D5D68EA021F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$A128E536-6EB6-42B1-99DC-BFE3E63DE11B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cfd356224155dbd75db29249481baba3510e2a8","datavalue":{"value":{"entity-type":"item","numeric-id":5394302,"id":"Q5394302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$ECC7DB9F-D4E6-4C76-9C03-0AE456A083D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"492542c2fa16745b6c1ab27c66663c1aea1182a1","datavalue":{"value":{"entity-type":"item","numeric-id":804559,"id":"Q804559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$9517EED3-902B-4FC4-B7CC-3BEB78650223","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$0BB321BA-91B5-4776-A9E0-13A87788BE18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a574e5aa189b3fc2747ed9f87d92c59b775e8e6b","datavalue":{"value":{"entity-type":"item","numeric-id":2722014,"id":"Q2722014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$7DFE1FE0-9C0B-459A-971B-E1248F6ADD13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ba8bd57f8794d317056b114a38bf751913f81c7","datavalue":{"value":{"entity-type":"item","numeric-id":3612448,"id":"Q3612448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$B28D7356-5344-4BC2-BF40-7F7FAE666FFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69fe664aa22c6ba1ea6d9ba12c2b4c3da0298ee2","datavalue":{"value":{"entity-type":"item","numeric-id":5277760,"id":"Q5277760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$16FD6B17-91B3-421D-9CBE-8FFF9683AD11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"becfd9a090d306eb2c018b96115467fea98076ae","datavalue":{"value":{"entity-type":"item","numeric-id":3535620,"id":"Q3535620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637183$9ABDC4D9-18E1-41E7-84BF-FAC9DEC5A5F8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad8400280694217f7467aa7b38aa90d07462da14","datavalue":{"value":{"entity-type":"item","numeric-id":3003322,"id":"Q3003322"},"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":"Q3637183$BE160562-535A-4BA9-8683-3B6101510A7B","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":"14f5b894fa1c86eac6e8a05bc3d85652de7553af","datavalue":{"value":{"amount":"+0.7490886449813843","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":"Q3637183$9A9A63CB-9151-4950-BDAB-FB20A7F8AB2F","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":"eeaacf51f8192db17bc23984850f92662d53ca46","datavalue":{"value":{"amount":"+0.7395481467247009","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":"Q3637183$A3FD50A9-4093-45ED-8C91-FC9BAB1FB6CD","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":"eeaacf51f8192db17bc23984850f92662d53ca46","datavalue":{"value":{"amount":"+0.7395481467247009","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":"Q3637183$40DFBE4D-27B5-4339-9DA2-C99A7A61BD65","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":"2cdb5c57661846f755fa0f245b49d6f922b88e2d","datavalue":{"value":{"amount":"+0.7388139963150024","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":"Q3637183$D66DF357-1DFE-4B61-A864-6A48A7891851","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3637183","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3637183"}}}}}