{"entities":{"Q2392480":{"pageid":2403223,"ns":120,"title":"Item:Q2392480","lastrevid":51788234,"modified":"2026-01-20T01:14:38Z","type":"item","id":"Q2392480","labels":{"en":{"language":"en","value":"Strongly typed term representations in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6193954"}},"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":"Q2392480$5FB026C6-9144-436C-8396-3C5FD7A09631","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"343a71c80e6ff9fe2736b3ec9e726421f198b464","datavalue":{"value":{"text":"Strongly typed term representations in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2392480$B56EE8BE-E903-4C63-84E2-ABBF2443C65B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"060ab5c59b5bb49dd1149720f28213cf404511c6","datavalue":{"value":"1269.68041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$97579639-C9AF-4BAD-8962-C69FEC139351","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"24edb71357444cfa1110c00b8f09fd608c1bc854","datavalue":{"value":{"entity-type":"item","numeric-id":2392478,"id":"Q2392478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$F0372395-9775-409F-B05B-2F929C17EF47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"61b4416adb1b221673db19b3bfc1a87bd25d3903","datavalue":{"value":{"entity-type":"item","numeric-id":1014643,"id":"Q1014643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$93AFB7CB-7F12-459A-AE06-1BEDB7B6BC1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e6914e2235b043c4f674d5b34fe68fb5b97b9a12","datavalue":{"value":{"entity-type":"item","numeric-id":724925,"id":"Q724925"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$4231A1BA-AF30-4370-BE2D-0F5AA46BA8C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"76aea849f9d31d470a57d9a5c902b7b2098fef91","datavalue":{"value":{"entity-type":"item","numeric-id":2392479,"id":"Q2392479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$76ACDDB0-9A0F-4263-A292-6D1B64BF19CF","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":"Q2392480$29D6BAE4-DBB2-4AFB-BD6C-C98EE92D8742","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7e52174554282dcd72d8428d308340f8fb7a9109","datavalue":{"value":{"time":"+2013-08-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2392480$A3D4A2A5-2F5B-4241-8AD4-B1BBBE8F987F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$2AF1EB41-6723-4BF6-AB51-A104919E9FFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$586A5721-CA51-4E03-BD20-E3A3E181ABE4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6cd96b685eb9b3da9ef090ef61a789de3c250d6e","datavalue":{"value":"6193954","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$3F380BA8-1A9A-4DEF-BBFA-49DA32008FBC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50070997a3eb672eae615ed68215d674ea65d5f8","datavalue":{"value":"\\texttt{Coq} proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q2392480$0D4FF293-EB9D-43D2-BF09-452193147EF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"edcaf4b865d581f486f497f6d16d5aa00bdf7e23","datavalue":{"value":"de Bruijn indices","type":"string"},"datatype":"string"},"type":"statement","id":"Q2392480$83536ED9-8963-4141-BE4B-B67ABA7072FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92d8c3f4d9ba01bede6893cf2af99618cf13e5d4","datavalue":{"value":"typed object languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q2392480$62EC54B1-11D6-4874-9EF7-98C20A5F4749","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"078e133db5b32b2a8c110691f05bbddf6876c263","datavalue":{"value":"Q56851585","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$5BFA0203-6AAB-486E-A28C-03797BC6AF5E","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":"Q2392480$6E4FC295-ACE6-4C50-AE85-0E35CBA2E5D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"903d87e27bfdb3664cdd0faa36258b30256b8fbd","datavalue":{"value":{"entity-type":"item","numeric-id":44981,"id":"Q44981"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$62B64165-F27A-4AFF-8B53-4993863AD673","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":"Q2392480$0B2D9ACC-2CCC-4E8B-88A4-202BB0B07B01","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3c29feadacf52e25da508e581d7e75dc7e2c0c0d","datavalue":{"value":"https://doi.org/10.1007/s10817-011-9219-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q2392480$412BFA97-C484-4DF2-AA52-1E823640E5C4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8b994e6b91ec3a309dd69c52b6fa2f37e6f9cbfd","datavalue":{"value":"W1997354605","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$B5EE5BCB-BAB5-4351-91C5-89610F9FE924","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7651946351829281edb6e9c299e3fa3b5f82af70","datavalue":{"value":{"entity-type":"item","numeric-id":5898169,"id":"Q5898169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$CC31443C-B7D3-4970-8210-8AB6E76FD98E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c541a0e0fccb98a32f18a8695d9eabb1926b39f3","datavalue":{"value":{"entity-type":"item","numeric-id":4945244,"id":"Q4945244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$7DFAE978-F670-4784-931B-8E993710B4B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05417919433e4d5ed4f85fc6474f5b255b9fe668","datavalue":{"value":{"entity-type":"item","numeric-id":2936808,"id":"Q2936808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$87C3FBAB-5BB2-4EA1-ABCB-2E5A451B2808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d98b134c489ef3023af867487d565081ebe9b47c","datavalue":{"value":{"entity-type":"item","numeric-id":3183523,"id":"Q3183523"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$67AEE1AE-360B-4C3E-A55C-12802BB1D149","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a797407b4949355fcd06204fe2bcb7b1218a925","datavalue":{"value":{"entity-type":"item","numeric-id":4256148,"id":"Q4256148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$D10F68B3-955C-42B4-941A-AAA6E9BF1CB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"367ef177c9ab91da57ee385240218ffe15eeadc2","datavalue":{"value":{"entity-type":"item","numeric-id":5178760,"id":"Q5178760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$FD15D5CA-CA30-489B-85A9-5FFBE8873713","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70ca3169b9facb7516f26162b8b9f1adfa3076fd","datavalue":{"value":{"entity-type":"item","numeric-id":1850959,"id":"Q1850959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$61DE70C5-DC45-468C-812B-E4EBFB01473E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b459d33ed668cef3cd5e11aaa940ab996a4a88bc","datavalue":{"value":{"entity-type":"item","numeric-id":3612438,"id":"Q3612438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$AFC11E69-5537-4DF3-9B88-59B70949C3D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$2F207881-E8B8-4B37-890F-BCA012908805","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":"Q2392480$66FA566F-AFE5-4744-9117-BA898886DF41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3ce3da52eafd9adc89e62fe46c921f7d614a2b9","datavalue":{"value":{"entity-type":"item","numeric-id":1945918,"id":"Q1945918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$08125C0C-7364-4C35-94D5-D69A2130403A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5029f3bd44027d166b83affc49717f11751e7c08","datavalue":{"value":{"entity-type":"item","numeric-id":4736399,"id":"Q4736399"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$3FAAD5FB-FCD7-49BD-BE5E-C70EF79A1600","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3893e24895c818d766b4ac601e2292c1956a8e2a","datavalue":{"value":{"entity-type":"item","numeric-id":4819653,"id":"Q4819653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$24936929-FECE-4E61-BDB5-22CAC578E192","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1cd712557cb33f4408f7f319583701e72d7ca321","datavalue":{"value":{"entity-type":"item","numeric-id":5168921,"id":"Q5168921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$51B472C0-CE83-4BA1-9EF5-0D2D3CF1CC8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f0b8d74eb30783ead52df96f665a06c49d9668e6","datavalue":{"value":{"entity-type":"item","numeric-id":2942928,"id":"Q2942928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2392480$E63A66D7-CEAC-47B3-B94E-E4C29BADCD99","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"cd0a1c205739afdbd3433f2e739a306af44a48cf","datavalue":{"value":"journals/jar/BentonHKM12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$86753D7A-6B5F-4076-BBB3-245AAABEFD7E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"726a7f6e67f615e255d2efda493dacc136fe5b7d","datavalue":{"value":"10.1007/S10817-011-9219-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2392480$F59B8607-1419-48F1-B66E-5A94B026C79C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e96f86b1d42820e56e89a9c5aff7e04de83089f4","datavalue":{"value":{"entity-type":"item","numeric-id":5195243,"id":"Q5195243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6b9179d95ebd07970f77cb50c975b2ba80620c3","datavalue":{"value":{"amount":"+0.7844849228858948","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":"Q2392480$4DFCB925-B82A-42A8-9FED-A3C3B2E1B616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d8981901febcd7accd965714d3a1f4b9b8c7219","datavalue":{"value":{"entity-type":"item","numeric-id":3024831,"id":"Q3024831"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"195378f02417c2703830eeef0b8561912807d5af","datavalue":{"value":{"amount":"+0.7720122337341309","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":"Q2392480$0AA0A980-3A19-4D63-B921-130653D65D82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"52ec3446f944ddce5f627197ad5663afdcdade75","datavalue":{"value":{"entity-type":"item","numeric-id":5898169,"id":"Q5898169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b1f571fd09fc9ebc51d52f5cfd42b31db719a96","datavalue":{"value":{"amount":"+0.7566585540771484","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":"Q2392480$54A88CB4-34D0-4A5C-A7D3-116CD9F53AA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"319f0e45bfa506ba9fbe0adbda954a115f9a8a53","datavalue":{"value":{"entity-type":"item","numeric-id":3189820,"id":"Q3189820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ede7aef84b23e0562a485d69f418476d6b064c56","datavalue":{"value":{"amount":"+0.7550787329673767","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":"Q2392480$7862DA80-607A-4D4E-BC9C-19322890570A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0dc23719a4c51797bff536a8269e1f58408b22ed","datavalue":{"value":{"entity-type":"item","numeric-id":897934,"id":"Q897934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35b56bf985dc5a37f84d2ba020c44984171352ee","datavalue":{"value":{"amount":"+0.7512854933738708","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":"Q2392480$48182228-0A78-4112-B2F5-363875D344CB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2392480","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2392480"}}}}}