{"entities":{"Q5370876":{"pageid":7400450,"ns":120,"title":"Item:Q5370876","lastrevid":92249213,"modified":"2026-06-05T01:14:49Z","type":"item","id":"Q5370876","labels":{"en":{"language":"en","value":"The exp-log normal form of types: decomposing extensional equality and representing terms compactly"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6794666"}},"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":"Q5370876$71880AC7-1293-49FA-960A-B1E6C4D231FB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5e178ea7b757fce3ad87135c5a0bc9f876b91bf6","datavalue":{"value":{"text":"The exp-log normal form of types: decomposing extensional equality and representing terms compactly","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5370876$5565D733-800B-4C06-A430-C204744FECB5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8ffa96cfe92e688f63957277f54707df564582ac","datavalue":{"value":"1380.68093","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370876$00824543-3AC1-4B19-B63B-F741C627E51F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b087ab3be90d7cab4af00ec981175e173ff47cc7","datavalue":{"value":"10.1145/3009837.3009841","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370876$40DA4D13-BD23-4EC3-8CD6-45D01201B430","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3eaf340d7ff821e26d8a935bc7e4aa006ed3e278","datavalue":{"value":{"entity-type":"item","numeric-id":450949,"id":"Q450949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370876$56732ADF-716A-4F3E-831E-C411CDCF8399","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e2300a4bb532724f6695014ad32dc9335c9fdde3","datavalue":{"value":{"entity-type":"item","numeric-id":5370840,"id":"Q5370840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370876$ABD92DD9-E37E-4FAA-B87C-1336A0F305BB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c23b22abb6cd47509eac4c3e5d58b13717e9ea4","datavalue":{"value":{"time":"+2017-10-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5370876$9A3BBA48-6EB6-4FB3-8E00-1A3CDCB85E3B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"48010c0d8ced74fce6b41cd9b643e7c72034a0eb","datavalue":{"value":"https://arxiv.org/abs/1502.04634","type":"string"},"datatype":"url"},"type":"statement","id":"Q5370876$B8AA9E06-23FB-44B7-B565-4D870AE067DF","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370876$230D7598-F73F-48F5-AE9F-C79588CAF60C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370876$A3B3DDB9-435E-4259-AEEE-52629393BD71","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ecb0da6526a2e37b3a317eac9ffb03839c3f71f3","datavalue":{"value":"6794666","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370876$83996D8C-D6AA-4BF1-8620-DD3AE22A8122","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fb061fb1cd35d79961314147769f7dae863f7f57","datavalue":{"value":"eta-equality","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370876$5C4B03AC-8AB8-4101-B2B9-0536C0BDCD37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e21b301cc01308d4b32384bfef39d6edd32325f","datavalue":{"value":"normal term","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370876$5FD75BD3-A814-4C94-B18A-D126B0BB8A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"62c2ea68de80beedc11e24479aa39b62d7080e3f","datavalue":{"value":"normal type","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370876$409E34D9-A856-40C5-9880-ACCFDE1B0CFE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1e570fa846c15de5d20dd532e9dbac8a22e7e29a","datavalue":{"value":"sum type","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370876$B5DB7DB0-E4B2-497E-8F93-20795E5A1CBC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"96c91c7c0e1050145142a02efaff3a9478404799","datavalue":{"value":"type isomorphism","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370876$168C4168-1CD3-484E-8900-2699576AF29C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dd659ac5b8a74f4c597d57fe951dd55cf510e8f1","datavalue":{"value":"type-directed partial evaluation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370876$60077FB3-C1B1-4658-8FE7-A8DEB8DF9B23","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":"Q5370876$1B5FF65D-6C38-45EE-9046-6C8D9B17F6BD","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":"Q5370876$635A3535-0C29-4614-8255-99150D2E32DB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4e61ef1e0ed40a447a39ab09290f7fc5c9e919d0","datavalue":{"value":"W3102609340","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370876$47BDF52E-26A8-4100-9C07-54A601F8AD83","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"23060c9dc1628bd92e9ce02531ff52f85143df1d","datavalue":{"value":{"entity-type":"item","numeric-id":3024834,"id":"Q3024834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a5b0e1628f3e4fda968b6718b518e945449341fa","datavalue":{"value":{"amount":"+0.7911588549613953","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":"Q5370876$91A6EF2B-37D1-4429-9273-A86584452DA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf019fe8bdfb83e5c4d6e25bd18014512b360e04","datavalue":{"value":{"entity-type":"item","numeric-id":3452250,"id":"Q3452250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"74426117d3b30c17a7343911407b391a7a252df9","datavalue":{"value":{"amount":"+0.7499755024909973","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":"Q5370876$13209D16-F5FD-425E-8A8B-BB5008DEFE21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d90b02514e25d1bb10193ff646a700dd1d89f642","datavalue":{"value":{"entity-type":"item","numeric-id":5370875,"id":"Q5370875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c67132039b1bfbb4f5c606757993a7880028f8f7","datavalue":{"value":{"amount":"+0.742943286895752","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":"Q5370876$1F1B4F9A-2F75-4358-A083-4086B9CE759C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b6f8eb7cd8caa082eea1e8d697a5efc3a629a89","datavalue":{"value":{"entity-type":"item","numeric-id":3638919,"id":"Q3638919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"501aaea5fa115577df0ca802570376829119a643","datavalue":{"value":{"amount":"+0.7354861497879028","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":"Q5370876$5D354E6E-478A-48CB-89F6-7FA345FD05D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12b9cbfb80a3c71c4bf3f247de6c661e68291464","datavalue":{"value":{"entity-type":"item","numeric-id":3612636,"id":"Q3612636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19fa347b18cc879d8fa1da3258fc981999f72942","datavalue":{"value":{"amount":"+0.7253334522247314","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":"Q5370876$0959D8D1-DDCF-431B-8905-6EE70024FC06","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The exp-log normal form of types: decomposing extensional equality and representing terms compactly","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_exp-log_normal_form_of_types:_decomposing_extensional_equality_and_representing_terms_compactly"}}}}}