{"entities":{"Q5957918":{"pageid":8134720,"ns":120,"title":"Item:Q5957918","lastrevid":102076709,"modified":"2026-06-06T03:26:02Z","type":"item","id":"Q5957918","labels":{"en":{"language":"en","value":"Coercion completion and conservativity in coercive subtyping"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1719233"}},"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":"Q5957918$B106A1E6-AE02-44DB-9989-02B5D42FFC82","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a3f6a7a53f63c5a72a80cb122b6359f17b07261b","datavalue":{"value":{"text":"Coercion completion and conservativity in coercive subtyping","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5957918$981509A6-DBFE-40D7-83BA-1C8E2E62EAFB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"158193f116cfe3f02d37379b817f8f6cda2f098a","datavalue":{"value":"1011.03017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957918$C76F501C-9D99-44AE-9FCF-1522C07C6652","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"54a40f96699e660471eff2dc00c9e7e125b8b993","datavalue":{"value":"10.1016/S0168-0072(01)00063-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957918$1CC0FA8B-2456-4410-800C-6BD687795996","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9b243572f25465f3ae7a32f2d3b06ae2073b8520","datavalue":{"value":{"entity-type":"item","numeric-id":590478,"id":"Q590478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$7CC0963A-3E9A-4633-88A9-09FD0A94C890","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5113b34e3bbf27434e01e2c75e261e7834776faf","datavalue":{"value":{"entity-type":"item","numeric-id":220709,"id":"Q220709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$A717EF0C-4EC8-4F69-9B4F-AEF9387A9E6E","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":"Q5957918$250664C7-18FA-49F5-88D1-0DEE02B96D69","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9bbc9c127b1d81211c5164932dcbd7d39ee216ac","datavalue":{"value":{"time":"+2003-05-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5957918$1BDC4010-D20E-48B7-A880-F49D15317920","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"115d68ce4cae497f165435c17a6df87d8b6ffa16","datavalue":{"value":"The idea of coercive subtyping is to consider some given maps as coercions. One main application is in proof development based on type-theoretical systems [see the second author, Lect. Notes Comput. Sci. 1258, 273-296 (1997; Zbl 0882.03029), J. Log. Comput. 9, 105-130 (1999; Zbl 0920.03062)]. This can be seen as an extension of type theory, in this paper a typed version of Per Martin-L\u00f6f's logical framework. It is important for this extension to be a conservative extension. The main result of this paper is that if the given maps satisfy a suitable coherence condition then the extension is conservative.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957918$179D648B-D30B-47E6-AE86-2D873F50B0AE","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"256f7e8a78354c9241b063a26583c1bfdf31ddc2","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$F2151970-AB2D-4C63-8CDC-74DB7E865768","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957918$484D7686-0E91-457A-B80B-F4B72427B0CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4cb4544bfd0397cd4a315ee326499c372f013de5","datavalue":{"value":"03F35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957918$3ACB654D-6004-432D-9327-5B688066605C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957918$950CA646-05EB-43C8-9ECA-4E166D380938","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"504450e8b55ea0ca8c71c4d233b4f5f2ba0db40e","datavalue":{"value":"1719233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957918$8D6A44A3-91F0-49A4-9598-AD363E49F497","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"272575b0b40558680152f7adb35b1b864229b47e","datavalue":{"value":"type-theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957918$8B5953DB-4005-4A9C-8A55-3ED3F4623C2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957918$489D1DC3-861A-487A-B926-10B38A1C53A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e7165fec9115f05c93be2e6750db8f2bb02167cc","datavalue":{"value":"coercive subtyping","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957918$B718880B-2923-43A4-974A-D02AD10AC46C","rank":"normal"}],"P1463":[{"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":"Q5957918$A53DD536-3351-480D-B7F9-CDCBDA570C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0043252eab773bb3d2cd954b74fc157019506249","datavalue":{"value":{"entity-type":"item","numeric-id":19435,"id":"Q19435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$EDDAD46D-00CA-4078-A19B-CF8F48DF2E10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$5CA7B24F-D540-4616-9629-BA3140EE5DAD","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":"Q5957918$4C8246E1-5085-4367-8843-67B633F0E882","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7d3128c33a17fc4f3e7b89ceb3e22b9648f4405","datavalue":{"value":{"entity-type":"item","numeric-id":3204024,"id":"Q3204024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$815D5EC4-1C06-44A8-9799-34AB19C436CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3247948db76f97fed8d70bdc01ad427c970bc38","datavalue":{"value":{"entity-type":"item","numeric-id":5951521,"id":"Q5951521"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$793224EE-9397-414B-9A2F-0E06EA63C4AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0b5b3e1d2709e0f5c17896cdfac83364e530049b","datavalue":{"value":{"entity-type":"item","numeric-id":4012883,"id":"Q4012883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$B52590CA-E3D6-4A1A-AEFB-D79900A2AC11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"782451ce427981fde209c5291352bfb752852e68","datavalue":{"value":{"entity-type":"item","numeric-id":4246948,"id":"Q4246948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$48D5740C-35EE-4001-AE71-E591D3149277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba3bc1b1f9403e20d87198bb25d0434276270b4d","datavalue":{"value":{"entity-type":"item","numeric-id":4507489,"id":"Q4507489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$1E08164E-F8B6-4158-9229-691C6FB684CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37bc8dae1994f1675072ec162c7c6788e05d8d41","datavalue":{"value":{"entity-type":"item","numeric-id":4296744,"id":"Q4296744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$96D1E027-5EBB-4681-A64E-E1644115FD17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aafffdd0b071666063f891cfea9298aacdb7897a","datavalue":{"value":{"entity-type":"item","numeric-id":4362923,"id":"Q4362923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$75CBA4F0-42E2-4932-B8B7-5E546718E417","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3bbf5c4acba1e943106282227d496dff22117d6","datavalue":{"value":{"entity-type":"item","numeric-id":4238487,"id":"Q4238487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$B9A24ECE-CAF5-4637-8117-544F6A47CEC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8be63c5f271ce7f1f200c26e0ab76283f6d86ebd","datavalue":{"value":{"entity-type":"item","numeric-id":1322473,"id":"Q1322473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$11069FA5-E55B-438E-A86B-CB1FCE4DE2BA","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":"Q5957918$73E649ED-4E92-4882-9128-C0E3B604177B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1670b5cb5391b0c5080176ccfa24ce24d6ef8735","datavalue":{"value":{"entity-type":"item","numeric-id":2956681,"id":"Q2956681"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957918$8F63F1E5-3330-4EF2-8452-543E2F1F94F5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"648908b5d41c6c11916370c6ee58e60f77eb1f1f","datavalue":{"value":{"entity-type":"item","numeric-id":1951591,"id":"Q1951591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb49dfbae095eb1ab25ba414e7f39e380873fd64","datavalue":{"value":{"amount":"+0.8556169271469116","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":"Q5957918$1BDE49AD-D891-42FE-82FD-9284B5B12465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b715475a5e4b33503e21e86d37cb680ba74d1b5d","datavalue":{"value":{"entity-type":"item","numeric-id":4238487,"id":"Q4238487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08b720b6cab247d9f41e64d059dd7ec6acd74521","datavalue":{"value":{"amount":"+0.8548206090927124","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":"Q5957918$801EE71F-428E-4F38-B508-990FC2B23F24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"66debf8c513c428c59edcbf061dbfc4c87ba8625","datavalue":{"value":{"entity-type":"item","numeric-id":4362923,"id":"Q4362923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb36f19741ccf132201a55be63d0c03f2efe949b","datavalue":{"value":{"amount":"+0.8544475436210632","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":"Q5957918$E6479C1C-2256-4ADE-867B-C445574ADA70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"594fdde212ba489ae68158839e8132d1f16cba29","datavalue":{"value":{"entity-type":"item","numeric-id":4820474,"id":"Q4820474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb36f19741ccf132201a55be63d0c03f2efe949b","datavalue":{"value":{"amount":"+0.8544475436210632","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":"Q5957918$9BC526C2-BA66-423A-80A6-C3084739D81C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f29371f29340ab7599f22a7c91c5319d3120fea","datavalue":{"value":{"entity-type":"item","numeric-id":2996166,"id":"Q2996166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0bdbd94ffafaadbf19e1eed610e94fa5544f811a","datavalue":{"value":{"amount":"+0.8365567922592163","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":"Q5957918$9D9004B0-5B64-4780-983B-6FA70A5B01AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Coercion completion and conservativity in coercive subtyping","badges":[]}}}}}