{"entities":{"Q6854422":{"pageid":20623174,"ns":120,"title":"Item:Q6854422","lastrevid":84263033,"modified":"2026-05-14T08:59:52Z","type":"item","id":"Q6854422","labels":{"en":{"language":"en","value":"Type safety of rewrite rules in dependent types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8163125"}},"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":"Q6854422$BF75F03D-3FD7-4D5B-BF6D-408AEC20923B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"3df74978a04950a6bd7e02447902801c0553bff2","datavalue":{"value":{"text":"Type safety of rewrite rules in dependent types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6854422$0D82FEA6-315E-4E44-A401-D53330000E4A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"62d7ba61652d4a21b1499384f0d2ffce25cb9b56","datavalue":{"value":"10.4230/LIPICS.FSCD.2020.13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854422$DC8525D7-AE67-411C-B6FE-AAE142DC5362","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8807e9b5ca6f3e9539fb2629b3f3fe474d0fb0ea","datavalue":{"value":{"entity-type":"item","numeric-id":235598,"id":"Q235598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$86902EFF-3285-496A-8D33-406293754498","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"23f7bc78d27ce33f5d6c9d48966ef81d2c43df8b","datavalue":{"value":{"time":"+2026-02-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6854422$544910F9-6860-4411-9A2F-49C9C0A7FD9D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"62a49b155c9af634e6c3562b1547da1f7c08791a","datavalue":{"value":"68-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854422$C85FCFEE-A420-48F7-9746-DCD9F49C8965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854422$F7CF2773-3382-486A-B659-C2A83E86FB95","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854422$EE878622-0B2F-4B76-9963-8CDDD65C7D88","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e69bdbf52f7ccd13857032cbee2ab2860a39d01f","datavalue":{"value":"8163125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854422$06F87D65-5D9F-49FA-BD85-2450F4340B52","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"daf5f856a5d861312ad309ab567540337a5f61d6","datavalue":{"value":{"entity-type":"item","numeric-id":57050,"id":"Q57050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$404621D7-9BAE-4949-AC6D-AF0AE725C565","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8354b53f538e2f3360f689a0a9975f1a472d2733","datavalue":{"value":"subject-reduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854422$89D7836A-4C75-474E-9B8F-571EB1457630","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"476e70cc5d552d5cdc76575cc73d40a8bfb4b86e","datavalue":{"value":"rewriting","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854422$337A0618-AD34-4873-BFEA-8BDEB92AB0CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854422$4AC85DC0-C702-4268-90D6-0007DFAAB92C","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":"Q6854422$431394FC-3E07-4C52-92AC-4F944DA7D24A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a3bd3ba10b0a8db4c435a1f311674675f6385e0","datavalue":{"value":{"entity-type":"item","numeric-id":4234771,"id":"Q4234771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$CF9EC7A0-F101-4033-87A3-E92C0786D46F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e6aa3e3851825ce947035770e997710fa99c398","datavalue":{"value":{"entity-type":"item","numeric-id":4657751,"id":"Q4657751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$5A111F42-8383-4FBA-9F03-AC911F29B0F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34b87924f23be2e9cf6d7b6faa675b811f5a3d7c","datavalue":{"value":{"entity-type":"item","numeric-id":3612625,"id":"Q3612625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$7C161B54-F071-44E7-8FF9-E6A2124478A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b37a40a03c37bebfcf2bb14674f3a940ea98e19","datavalue":{"value":{"entity-type":"item","numeric-id":4383698,"id":"Q4383698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$C53A2B68-E9EC-4B32-9D21-56CD74FD7682","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad49c0e73a818ba4ceaf2b590f61e94f93060ab5","datavalue":{"value":{"entity-type":"item","numeric-id":1929227,"id":"Q1929227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$5DADC7D2-D51D-4D26-A9C5-D2F20B9FC98A","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":"Q6854422$2FC8BB07-F663-4A27-B4BD-05AE9B99E505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be604f9726a120d8606eea2ea8bf40b25f834421","datavalue":{"value":{"entity-type":"item","numeric-id":3918095,"id":"Q3918095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$CB3B8802-B143-4F54-82C3-25FE2D177CF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba1eb42d9c5348c57088bd4b838a7a5b42853faa","datavalue":{"value":{"entity-type":"item","numeric-id":1314356,"id":"Q1314356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$6629958C-250C-4004-8233-3B874AAFB21B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52993d82a0ab7d20a5a52eff1d3b454c784598a7","datavalue":{"value":{"entity-type":"item","numeric-id":1107975,"id":"Q1107975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854422$6C1DF152-F801-4D33-BEC8-567C270F8CDE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Type safety of rewrite rules in dependent types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Type_safety_of_rewrite_rules_in_dependent_types"}}}}}