{"entities":{"Q3613430":{"pageid":5643336,"ns":120,"title":"Item:Q3613430","lastrevid":50603783,"modified":"2026-01-14T13:14:14Z","type":"item","id":"Q3613430","labels":{"en":{"language":"en","value":"A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5528310"}},"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":"Q3613430$6A7C8F33-43B3-4148-9698-3FBC979EE944","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fbec24372df70d536a75cc1489d559e1b609c227","datavalue":{"value":{"text":"A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3613430$633FF53A-5D64-4280-B3C4-37FDB256E36E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ad82fd7ed21ee4044e1a7fcb03066f8e0c817f2b","datavalue":{"value":"1222.68374","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613430$D75717E3-E424-4CD8-A2E8-447419A520C5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d7ccf9e88c7a7b3f8fc7d4e7d26aa668d18dc25c","datavalue":{"value":"10.1007/11814771_41","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613430$5323B6A3-F826-47E2-93FE-150E22718F50","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8be13823e57b532010d417bfefa3b5133f759f9a","datavalue":{"value":{"entity-type":"item","numeric-id":860832,"id":"Q860832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$3BD8ADAE-630F-4802-A732-2D27A5A2E900","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"886664d698445e1702c39c62a8e99a722a88bdd6","datavalue":{"value":{"entity-type":"item","numeric-id":817699,"id":"Q817699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$7D22A420-39FC-4ECE-8F63-22B12AB2FB7B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3085facee3457e7f15d7356906b0165b8709b141","datavalue":{"value":{"entity-type":"item","numeric-id":2817907,"id":"Q2817907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$FF00676A-90BD-488D-B988-5B800AEE1BBA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5633353462eee310c4db3234ed97ea2c49f28694","datavalue":{"value":{"time":"+2009-03-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3613430$4DB3FABA-B12F-4EF6-8276-33A3FF2D3597","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613430$461E26C0-75DD-40C6-82B4-582098875227","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613430$D4C4B924-6626-4D2E-A6B1-0F9A2F92DC44","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0b8e0a6867ec48755f4f298e63c180b0f1229bee","datavalue":{"value":"5528310","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613430$CDB97FEC-A422-4589-914A-0AE77ED7677E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78b2cb2aa8953507be78145ef07fb1e05160aa99","datavalue":{"value":"lambda-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q3613430$D37589CC-5C19-446A-AB50-75D803D7DB14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q3613430$E895EE23-9CDA-4B5E-A752-BC9BC47D6A2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b78f667b6c625145d6218b1051d1ef814c946291","datavalue":{"value":"nominal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3613430$FCD4418E-1BE5-448F-BD0A-5646DAC2C66C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac91c497e5a12b747663afac74f58bf2ab28eb97","datavalue":{"value":"primitive recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q3613430$9D3A37A5-EC64-4E29-9938-7A1C2F47338A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$CAE36B0B-521B-4DF1-9F0F-F350EA2E4562","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$16C4B1E2-31DF-4ABF-9ED1-DB9239B6B045","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$E89CECEF-8BC5-46D9-8D98-275DF09765CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3613430$C84155C2-50C0-4CBF-9443-731B26586EA2","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":"Q3613430$308EACA2-8F79-4E7B-AFD8-D47DAA07BB01","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b2e80cd7c117f41614fd466892f2d46577736e88","datavalue":{"value":"https://doi.org/10.1007/11814771_41","type":"string"},"datatype":"url"},"type":"statement","id":"Q3613430$07DAD619-21AA-4B55-BD07-9DCB6373DD6E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"912872e35f5b435210a57f293e91b484db8f22b1","datavalue":{"value":"W2162208777","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3613430$696A058C-9DD8-421E-9047-E8B5C016B4CF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad70124600704120650b3399879cba7e852de047","datavalue":{"value":{"entity-type":"item","numeric-id":928672,"id":"Q928672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ece2154d777d601f259a27709e6a649d0f6291d1","datavalue":{"value":{"amount":"+0.7952859401702881","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":"Q3613430$6F387F78-EAC0-4C2D-B6C8-0E8E6F5C4D80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a8121b45f5a2121f5d02e937ed3d255985aa611","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c73c26a2db2ab92c99f581dda466c399c8bb08f","datavalue":{"value":{"amount":"+0.7928194403648376","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":"Q3613430$5F98A8C6-566D-46D7-B631-C19FFFF2AA8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b403893b3853ccc2d56f9e150dc2696721cc1178","datavalue":{"value":{"entity-type":"item","numeric-id":5891628,"id":"Q5891628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce8f0b82bdfad62580b33b44feba5a255f1fc959","datavalue":{"value":{"amount":"+0.7804818153381348","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":"Q3613430$062D1A2D-A311-4B25-8250-B9CD3DE90DC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b0f0d0f0a622c9959dcd383c9f471cd4a0a93bb","datavalue":{"value":{"entity-type":"item","numeric-id":5892493,"id":"Q5892493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2923842bd23d469ff0f1d2666036b96b9c2d6da5","datavalue":{"value":{"amount":"+0.7765383720397949","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":"Q3613430$8708FB82-8979-4031-B0D8-68AD7AE4B1D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4a45bc8bbd65bfc7012c61b3077d81f2b27c76b2","datavalue":{"value":{"entity-type":"item","numeric-id":5255070,"id":"Q5255070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8bd8aee6c4caa5f30958c9ae274d6a13697636dd","datavalue":{"value":{"amount":"+0.761854350566864","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":"Q3613430$548C8240-CDF3-4B77-9497-F34965317A87","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3613430","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3613430"}}}}}