{"entities":{"Q1322473":{"pageid":1333223,"ns":120,"title":"Item:Q1322473","lastrevid":68461359,"modified":"2026-04-12T23:52:01Z","type":"item","id":"Q1322473","labels":{"en":{"language":"en","value":"An extension of system \\(F\\) with subtyping"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 563080"}},"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":"Q1322473$2727F107-051B-40B3-A715-B38E4EF5DDB3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"518138dab4d3c03db74716a93bf8b5904912e36c","datavalue":{"value":{"text":"An extension of system \\(F\\) with subtyping","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1322473$7E19F57B-CF5E-473B-9E65-3378CCFED90C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9521786ea21d2a00b87f65c15728dfd5612989a9","datavalue":{"value":"0805.03008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$DF984B56-14E7-4E38-9760-FD13EBABA076","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"391ea0a2eccd2e1ffb7d70cb5807f87e3011ae63","datavalue":{"value":{"entity-type":"item","numeric-id":418827,"id":"Q418827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$5BBC1383-A0C9-4161-BA91-FA32E0652932","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a7b0bfbbcf5657a8b101c8d9d79e6747c41c0556","datavalue":{"value":{"entity-type":"item","numeric-id":276486,"id":"Q276486"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$8F4E2BD3-2DBF-4E2A-83DF-09FEE12273D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7086b371037f8c6a4118ffbbe29f86ca9e6f2148","datavalue":{"value":{"entity-type":"item","numeric-id":596036,"id":"Q596036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$94F0F9D4-FF3C-4356-BF86-63838154345B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"183df695ae89db8e2a7647ddbe2de62ff0deb022","datavalue":{"value":{"entity-type":"item","numeric-id":1052316,"id":"Q1052316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$43065E8D-4A1E-4609-A7D0-16B96983CCCF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fa2d1ad91af9619c8dd37ab889fe279a84c4057e","datavalue":{"value":{"entity-type":"item","numeric-id":259032,"id":"Q259032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$6AB3CAC0-EC71-4811-AD01-DE15EC0E7474","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e2370192b51581a9089045828e517d05f104e988","datavalue":{"value":{"time":"+1994-06-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1322473$8CFBFD65-5100-4647-B087-977C9F340EAC","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"58da52d3b7949f32430ea0f53861fb134ddbd3eb","datavalue":{"value":"System \\(F_ <\\), which is presented here, combines subtyping with the parametric polymorphism of Girard's system \\(F\\). Partially inspired by the PER semantics, it is obviously sound for it (but not complete) and differs from Curien and Ghelli's system \\(F_ \\leq\\) by the addition of a very natural equational rule (between terms of the same type). This rule improves in particular the categorical aspects of the system: for example the usual second-order encodings for products and coproducts are here true categorical constructs.   For what concerns typing judgements, \\(F_ <\\) is equivalent to \\(F_ \\leq\\) and is conservative over \\(F\\); wrt provable equality of terms, both fail and \\(F_ <\\) may equate simple \\(\\beta\\eta\\)-normal forms.   The expressiveness of \\(F_ <\\) is demonstrated by a set of examples including records.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322473$2511B32D-FADE-454A-9F48-F5C568DDA26C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$1EDD36F3-A978-4C2E-A5F6-4A4D75229DF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$9208101D-5E58-4101-8D1E-F230C70682C1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"be116f762fff79f7fe20ce4e751bcb9a807c9b8d","datavalue":{"value":"563080","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$379DE98B-31F7-4D1A-98A9-1EBC2A237F33","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543b5b6936751d447dfb75294948e5dafde0cec3","datavalue":{"value":"subtyping","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322473$E64DF2BB-1F67-456A-B432-1B5AEADCFA34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658b900684683a841bc471a204ddeb78a040d114","datavalue":{"value":"parametric polymorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q1322473$68E0D2BC-3B13-4214-A9EE-34CDE9F12947","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"cfea56292579072863c42a6e983fef653b45e536","datavalue":{"value":{"entity-type":"item","numeric-id":1391738,"id":"Q1391738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$2D56EC7E-7993-431E-97BB-AAC75B2FD987","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":"Q1322473$99FCBB1A-9CBA-45A2-BB56-83D3F77F19BF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"819da1434406d4de3736cf16cf299c8bab320ce2","datavalue":{"value":"https://doi.org/10.1006/inco.1994.1013","type":"string"},"datatype":"url"},"type":"statement","id":"Q1322473$F3EE5A4E-7166-494F-98FB-B21A49D49924","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ad9243cde5f61f729588e215848d29233f32bd44","datavalue":{"value":"W2165657834","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$390F3BCD-AC03-401A-99EE-65F1C52939EE","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"4c542ca8aa2747cb02da847444466448324d1695","datavalue":{"value":"Q56518661","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$83B6D6D1-E57B-446D-B089-F2C70BF0E16B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"58a9d2327f3ea2f8c0c6757f5e58bf32e3527955","datavalue":{"value":"10.1006/INCO.1994.1013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1322473$EA747D85-1383-4FBD-9946-483132B3D102","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"242cf683288af100827015f68ac43b1efdb86b09","datavalue":{"value":{"entity-type":"item","numeric-id":5096247,"id":"Q5096247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e443d042caa270adc01c03c1ec2c2bea3b5b8641","datavalue":{"value":{"amount":"+0.9057289361953736","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":"Q1322473$64EF85A1-4CD5-4AD4-955B-A5CE3E17836B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eee3a3403892b4f66e652e5a89a91407811a4734","datavalue":{"value":{"entity-type":"item","numeric-id":1605176,"id":"Q1605176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"51972f82a0c34b7d36fb78a113a8634223923d0b","datavalue":{"value":{"amount":"+0.8286574482917786","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":"Q1322473$EB62EA17-5ACD-417B-8412-09BBD11D7203","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ddfc248ef8f670fb557ac7a904ceb5e0e5afcfb1","datavalue":{"value":{"entity-type":"item","numeric-id":4364396,"id":"Q4364396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"25af56a99778cb833f0f1fe6ff583e0029724b2f","datavalue":{"value":{"amount":"+0.7956899404525757","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":"Q1322473$3C1493E0-C0F9-4399-A83B-4AF326DBA84C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"06e5c49e676c41aa5ec4011d82699145efeda181","datavalue":{"value":{"entity-type":"item","numeric-id":1392282,"id":"Q1392282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38894a70569d744dc2e8193e064328d996a41235","datavalue":{"value":{"amount":"+0.7926732897758484","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":"Q1322473$C250750A-4299-4961-A92B-28D9DD46D746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aac00bfb186d8dda9d55b5cac0875f10e393feed","datavalue":{"value":{"entity-type":"item","numeric-id":5096246,"id":"Q5096246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6112c3d6a3f455b42ff59d8d5126975b0885c704","datavalue":{"value":{"amount":"+0.7899491190910339","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":"Q1322473$F0EAF3E8-BF86-4C1B-9035-031B67D6F25F","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"c39a117a349789e54237c0a3254f5a10c0a6517e","datavalue":{"value":{"entity-type":"item","numeric-id":6830565,"id":"Q6830565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1322473$F736A85E-13D6-4EB4-97AA-0AA52B28C0B1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An extension of system \\(F\\) with subtyping","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_extension_of_system_%5C(F%5C)_with_subtyping"}}}}}