{"entities":{"Q1945918":{"pageid":1956660,"ns":120,"title":"Item:Q1945918","lastrevid":69831900,"modified":"2026-04-13T10:38:44Z","type":"item","id":"Q1945918","labels":{"en":{"language":"en","value":"Nested abstract syntax in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154939"}},"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":"Q1945918$921DC2F7-0682-4F54-A7E0-A52C39F408EA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b5c17f8a780897318278327cde33bfe6cca758b5","datavalue":{"value":{"text":"Nested abstract syntax in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945918$0AC5CCA3-E2E8-4F6A-851A-60FC36CA4D83","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9e88ef19cc2aafee351c89d1e934438983de0145","datavalue":{"value":"1260.68374","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$9395C381-9046-4E69-BAED-3C9212559278","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ea229d5c7d566db264a7e69175c2b14cf582fccb","datavalue":{"value":{"entity-type":"item","numeric-id":438545,"id":"Q438545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$47DDA6F9-CB60-460B-8833-3931E156DC78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b98d978fe1bcd6c0757acb680bbf15dfeeab6501","datavalue":{"value":{"entity-type":"item","numeric-id":1253341,"id":"Q1253341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$3362FE4B-71C4-412F-862E-29C369D1A842","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":"Q1945918$6A8721CC-AFD4-490D-96BB-DFA5A905E4E2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4bad757aec17a8570e2102d57df4c93baefd6019","datavalue":{"value":{"time":"+2013-04-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1945918$A0BF983A-CA52-4719-88BD-C1256B433567","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$3B098B7E-82B7-4C3B-A087-785C00F7A7C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$D7A3B2BC-F88A-4353-BF81-ADA4D77D6545","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$14169C73-6124-44BF-8503-0B42B187EE5E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ecbc125d5a9afad502368ab62e64eefa6a065fc7","datavalue":{"value":"6154939","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$2A6EF2A0-6CB6-4BA9-8F7A-927171B03651","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"17def916adb6b4246c3d8558f18624e3541d6d4c","datavalue":{"value":"POPLmark","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945918$396F9FAA-1179-4BF6-B2DD-0ADC573D7954","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543bf8400f98f9e945a1fb4a6d773856ebd6d9fc","datavalue":{"value":"abstract syntax","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945918$48CB0C83-227A-44AA-B9BF-283DF1FA66CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945918$0A252397-A44E-4204-85F1-E4B2A302BF65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5078cf6f277ce8f633e2f2940b8f9652adcda82a","datavalue":{"value":"nested datatypes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945918$7A161BEF-35C2-47AD-A94A-73E5B19D122E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"905c185b35495bc6c5c2ada6dd808940c7264ec2","datavalue":{"value":"\\texttt{Coq}","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945918$51C085E9-3889-4AE3-8CD7-3CD5406B5E32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"975bdfd17aa9f17c4fe3971912f8bc73290411ae","datavalue":{"value":"System \\(\\mathrm F _{ < :}\\)","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945918$B844CCB9-3B8A-4B03-B72B-6AED3CBAFADF","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":"Q1945918$E349A5C9-5CF1-455D-89B3-8303EEAA0BE8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$FE0C5C2A-0608-45DA-BE61-EB7DA623B8C1","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":"Q1945918$1B98DBAB-7069-4B9A-B3C3-7FA0641FA0A9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9f7e49b0050255c5c9269a79818bab8dfd2072b2","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9207-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945918$810EACB4-6502-4472-82DF-4FA3131C419B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8f7fe33d0cfc75dae4b77f7b92270469f3e42022","datavalue":{"value":"W2147567862","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$AB2D793F-0496-45DD-99EB-842968CB097F","rank":"normal"}],"P223":[{"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":"Q1945918$4CF249E5-77BA-4368-9970-C0C911C0EC28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$62362114-EE89-4E40-B128-C6C75389F1EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c50237c8bde09d6668086722c62e1080ba158cf","datavalue":{"value":{"entity-type":"item","numeric-id":3189820,"id":"Q3189820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$901FCFC1-0BA3-4942-94D0-6CE02F713530","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":"Q1945918$CDE4C346-F6F0-4640-977D-D166D95E72F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"882e318ac9b6bbd79e82dcc1ce3fe340042f5778","datavalue":{"value":{"entity-type":"item","numeric-id":699761,"id":"Q699761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$035555F2-C0A5-4B7A-970C-625EF48D47A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54369932520febcb9c58f8434b9b8e94505ec97a","datavalue":{"value":{"entity-type":"item","numeric-id":3612664,"id":"Q3612664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$95296846-967E-4E92-A776-A02326098803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb4eaff37ca0626b0bedd741648f8cc265e3ccc4","datavalue":{"value":{"entity-type":"item","numeric-id":964503,"id":"Q964503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$C609446D-35DD-4599-A858-3D9AA7027D47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc09fba81e6a14082e7e439b4990f073f09d0006","datavalue":{"value":{"entity-type":"item","numeric-id":4535076,"id":"Q4535076"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$F301226E-13F6-489A-B19E-D2D30EE94DAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6063e4a144bafe1447ae8b10555347d26c418f1d","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$1C224CD2-F9E1-447E-8E7F-CD9A8B004C72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7339740287f50f43f28bfb905009c15405396d84","datavalue":{"value":{"entity-type":"item","numeric-id":3521990,"id":"Q3521990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$644FF0AB-AACF-4D40-A7FF-A349294781ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b948850fe331e2b203a34ee2a1cc029dc3504fe4","datavalue":{"value":{"entity-type":"item","numeric-id":3507459,"id":"Q3507459"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$E2AA6B33-3B19-4305-AFB6-A85111D513CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58137c2009742a39b30e5cb42aa06402d77c473a","datavalue":{"value":{"entity-type":"item","numeric-id":3638923,"id":"Q3638923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945918$CEA2C15E-6BFB-4280-B112-88BE4BB4EB07","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ba51aceeb95fe4a886993a81ab471dd821586880","datavalue":{"value":"10.1007/S10817-010-9207-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945918$CF97CC7E-5C9C-40A9-8D4B-83F55518BD6F","rank":"normal"}],"P1643":[{"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":"7e1736950a8431f9521f20dfcf55dc42b827f375","datavalue":{"value":{"amount":"+0.93848765","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$3ECBC8F1-0CB0-4153-9D58-8EE55793A5EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"771e6bf14bf9eed658c21b56b460fb04bed1fd1d","datavalue":{"value":{"entity-type":"item","numeric-id":3656423,"id":"Q3656423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"19affcea61ab9407a9e630b24cd45644c060ee9d","datavalue":{"value":{"amount":"+0.8696933","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$F297532B-3E2C-4876-8F68-FF87462247A0","rank":"normal"},{"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":"a3d04947ddb6828a85c574d894678ddd83626ac0","datavalue":{"value":{"amount":"+0.8673823","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$DFFB695E-9522-4FD5-998F-02E6E5FF2412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13f12cc42a11f603ff3a7078a8ce829374450f4f","datavalue":{"value":{"entity-type":"item","numeric-id":4790656,"id":"Q4790656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc5b4a2c36c76c8309ee8138bce7bcf8e2050db7","datavalue":{"value":{"amount":"+0.85932","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$8BFC37D8-54AF-44FD-8A93-0F8805D168B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fba24dbc87145dcfa5054973152a32e0554098f4","datavalue":{"value":{"entity-type":"item","numeric-id":3612436,"id":"Q3612436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"424c30df9071099035e03a50d192dda775d1611a","datavalue":{"value":{"amount":"+0.85772663","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$67AA3EEC-ACF9-4DC9-BF7B-9F7CFE11045D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b980f02bbfdab06904251eb25e41ba0a430fc4d2","datavalue":{"value":{"entity-type":"item","numeric-id":5191090,"id":"Q5191090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df6f18a7f9de9fb94b0b6e80a5661170381c583b","datavalue":{"value":{"amount":"+0.85754967","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$E483F19D-6F33-42D4-BCD9-2D5302FC2D50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c581e669ae9408182aff3af608d0ce1c9f3579f4","datavalue":{"value":{"entity-type":"item","numeric-id":5747671,"id":"Q5747671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"030870f8cb6a2b5e8f653c121f9e552b01707c3b","datavalue":{"value":{"amount":"+0.8574858","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$51A9BC89-00CB-40F3-A1A8-CC90323CE71A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b85b92a612525e53f1940e47c9de317d158f38a","datavalue":{"value":{"entity-type":"item","numeric-id":3608814,"id":"Q3608814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eba76b7a36dee569f08da5d20ecef19edff6306c","datavalue":{"value":{"amount":"+0.8559743","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$A29F25C1-826D-468D-B596-EECE81B6FEAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4e08ae23f2ce5afd49576406a05a26a50add7678","datavalue":{"value":{"entity-type":"item","numeric-id":2873661,"id":"Q2873661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98667b95fb665dde868f29fc07bf9cb171cc7b1a","datavalue":{"value":{"amount":"+0.85372037","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q1945918$7D5B2DFE-EFC5-4F01-827C-90043FF7E7C7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Nested abstract syntax in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Nested_abstract_syntax_in_Coq"}}}}}