{"entities":{"Q5951521":{"pageid":8128323,"ns":120,"title":"Item:Q5951521","lastrevid":41145653,"modified":"2025-04-18T12:21:32Z","type":"item","id":"Q5951521","labels":{"en":{"language":"en","value":"An implementation of LF with coercive subtyping and universes"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1686106"}},"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":"Q5951521$7CB0721E-F57A-41CF-B490-8C84B465EB3E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7403320f589caff51a735ff6792a682699d6d6b3","datavalue":{"value":{"text":"An implementation of LF with coercive subtyping and universes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5951521$6838042C-42E8-4968-8CA2-33A32F9E3FE0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"663f7e68d6760ddb1490862068373e1756074fbc","datavalue":{"value":"1023.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5951521$28957D8F-42EF-480C-A8F6-6F11C64A814A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ae14731c9f03583cf1ea8be28336c12e73cb9fca","datavalue":{"value":"10.1023/A:1010648911114","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5951521$647DD865-FCF5-4DE0-9AB9-453B67885684","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"455bae95859b37c76b307ba0c2ccbe1537e6ac0a","datavalue":{"value":{"entity-type":"item","numeric-id":220708,"id":"Q220708"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5951521$90B77D3A-5BC7-4FEB-AB44-9D8E7C53F16F","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":"Q5951521$DD794C45-33C4-4583-A37C-4C2886FC5C4A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5951521$F01DAC10-2748-41EF-A919-BD910E5F86C2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f5e795d8a81678d731e723940d525286b4e103d2","datavalue":{"value":{"time":"+2003-11-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5951521$20EEEB28-5571-49A7-AE86-CAE1B7F92AE1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"03e1a821dd73ed45e8244146641e1fa25fbd62e1","datavalue":{"value":"An implementation of a variant of Martin-L\u00f6f's logical framework with coercive subtyping, called LF, is presented. The paper begins with an outline of LF with its extensions of inductive types and coercions; then, motivations and the basic architecture of the implementation are given; finally, some examples are presented. In particular, special emphasis is put on the implementation of the the theory of a hierarchy of universes included in the object type theory UTT, which is outlined and implemented. The relationships between universes and inductive types, and between universes and coercive subtyping are studied and, as a conclusion, the authors claim that the combination of Tarski-style universes together with coercive subtyping provides an ideal formulation of universes that is both semantically clear and practical to use.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5951521$C6F1CF4F-114D-468B-8B21-881D729A604F","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d9c7994377655925beca167212c6ec3527b954b5","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5951521$09215ABF-3B86-474F-9818-0EA2BCEBEB38","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5951521$DDC0B0B5-F7DC-4A6E-A59C-F5FC92A80740","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0adfffbe0e586fc682ec4fff201fa7d0f1f9df8f","datavalue":{"value":"1686106","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5951521$4F2B9002-53E0-4909-B900-1721ACFE4397","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5951521$22411803-F329-46AB-9BCD-4230FE9CD542","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb8ff27bbbd9959dc9d199dde836f711285242b5","datavalue":{"value":"universes","type":"string"},"datatype":"string"},"type":"statement","id":"Q5951521$9F0895ED-767E-485D-8902-7F38B2CDB016","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95c030d9a0c4c312aef7a319ac8b5849913b2040","datavalue":{"value":"logical framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q5951521$67C72453-191D-4EE6-A36D-E1854A44D5DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ef359d59e74cb9142903f0e8e9f4e9a6db893b78","datavalue":{"value":"implementation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5951521$0013C34B-4165-4446-8CC8-5409546A0F17","rank":"normal"}],"P1463":[{"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":"Q5951521$0720D503-587F-4715-99DF-AEEEE8C7A159","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05e19126d9e9907924a4600d0a5598afdc2c5f70","datavalue":{"value":{"entity-type":"item","numeric-id":20609,"id":"Q20609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5951521$1C20C5B3-7AE6-4E89-9521-48954068CD20","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":"Q5951521$EE2ACED0-CAA2-4BBD-BF37-12C21B2C97D4","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3b39ffe8f8b7a34c4cccf9af03267aba5852a511","datavalue":{"value":"https://doi.org/10.1023/a:1010648911114","type":"string"},"datatype":"url"},"type":"statement","id":"Q5951521$BA347A72-198D-4579-B748-46EDB885E34F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3669fa7c596e393858cbe38c35b4732fdac9f0ab","datavalue":{"value":"W1813213602","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5951521$FA8ACDC7-0609-42AD-9E64-9E21A325B317","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c48aae8fd39c8b4a66b19bb4c6c754b913540fee","datavalue":{"value":{"entity-type":"item","numeric-id":2942921,"id":"Q2942921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97e5636ba93d4f90a6dd6f71b5020bc4f08330e0","datavalue":{"value":{"amount":"+0.89930457","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$B20A006C-35CE-4B81-85C9-78ABFED91C9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09dcfc29a679f1edee160689ef72e73458c00e75","datavalue":{"value":{"entity-type":"item","numeric-id":4246948,"id":"Q4246948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa0ed33f9c02320e5fad4c3cb748b98d6ac0ef31","datavalue":{"value":{"amount":"+0.89812005","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$ED936046-2C62-417A-83D6-68F6CAFF1F71","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":"f4cb455e366ace5ae9b857d81d9ba50f6d95323e","datavalue":{"value":{"amount":"+0.87735325","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$3B655130-557A-4C4E-B37D-8E276D57E9E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b12fca70c80b50c2c2b9f44f6d856ee5c5a831c8","datavalue":{"value":{"entity-type":"item","numeric-id":4499304,"id":"Q4499304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c81843d6d270387c555f657c517c2dd42de38e6","datavalue":{"value":{"amount":"+0.8767761","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$ABC4F89E-6999-440D-B3D2-0035D232825E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b0580c3e92656291b2b623d4dd1fefc3c024e797","datavalue":{"value":{"entity-type":"item","numeric-id":2747942,"id":"Q2747942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c81843d6d270387c555f657c517c2dd42de38e6","datavalue":{"value":{"amount":"+0.8767761","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$8FBD8872-7DB8-4BDC-8709-1D74B03C2582","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f30882d14a49fa9276a462e5339dbd1b4df27322","datavalue":{"value":{"entity-type":"item","numeric-id":2936830,"id":"Q2936830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fbe826b912ac1e2d3975cd09934bdfe5709187c","datavalue":{"value":{"amount":"+0.87580454","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$6F8DE89C-54A4-47BD-86B3-6C6CCE5F40B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b361ca1aa5526764549f3d95137afb2aca29dcf6","datavalue":{"value":{"entity-type":"item","numeric-id":6061881,"id":"Q6061881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c098a159a8c81031a7254ad3a8a09d8a0423c10","datavalue":{"value":{"amount":"+0.8712586","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$B1E08621-A3E9-4CFD-8D6C-41BEFDC842A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb5df00425f6b36425ebf937a40a35a967a7fdb2","datavalue":{"value":{"entity-type":"item","numeric-id":3372684,"id":"Q3372684"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d9b8b8ac2c77e1a0edd70c336bea049645ef7a3","datavalue":{"value":{"amount":"+0.87061524","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$15E34463-284A-4F19-81B4-26776C039C5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6272bff2ef2753562174842ca396160d3c8e9852","datavalue":{"value":{"entity-type":"item","numeric-id":5957918,"id":"Q5957918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c74633cb4e0f3376c67d5ded62087c407bfea734","datavalue":{"value":{"amount":"+0.867405","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$99F6F171-15B6-4651-9E59-068FBCF6031D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"48e6b2f2aa39a2a7a9d647c753613818954876ff","datavalue":{"value":{"entity-type":"item","numeric-id":2871871,"id":"Q2871871"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a88771f5bcdbe2fbcc4cccb1e3ead5cdc5f58dfd","datavalue":{"value":{"amount":"+0.86485195","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5951521$14E5F77A-618C-4A50-A08C-B7455314FD79","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5951521","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5951521"}}}}}