{"entities":{"Q5089035":{"pageid":7118611,"ns":120,"title":"Item:Q5089035","lastrevid":55415380,"modified":"2026-02-17T15:57:18Z","type":"item","id":"Q5089035","labels":{"en":{"language":"en","value":"Guarded recursion in Agda via sized types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7559298"}},"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":"Q5089035$73C55B27-7782-4F64-A1E0-01C70460476D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c39a632e645d6ba105bdab27ef952da1f8327439","datavalue":{"value":{"entity-type":"item","numeric-id":1675788,"id":"Q1675788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$2FE2E6EB-5F63-4283-8FF9-08FEBAFE6C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7621c274c256d2c46ce77f2004ae28ad57e4e062","datavalue":{"value":{"entity-type":"item","numeric-id":2133177,"id":"Q2133177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$BED23C2B-A220-4F74-8A33-7165186BB473","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6793430fc5b4ace9180691774574e339423361ba","datavalue":{"value":{"time":"+2022-07-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5089035$37FBC711-58CA-4C24-AD31-3B96A782134D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089035$5A4361B0-D44D-4D9A-A897-3318F3473AC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f969879f531643f058f8dd4c87a7dd4eb7b8c4c8","datavalue":{"value":"68Qxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089035$1E461373-BA83-4BCB-8C01-3F36B954C46E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6b48ebe2d2b0345f4569b93155cd0fd74c2b566d","datavalue":{"value":"7559298","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089035$37CE61EB-F8A6-4E53-88C9-D620DE19DF15","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78595e01e33a776db47f64e25022b2efb0c67194","datavalue":{"value":"guarded recursion","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089035$D0AABAD2-184F-4A7C-8F2A-52594E79DF38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089035$EDE50C86-8AFF-42E4-8904-50B2A9B5CD01","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089035$A3C5B7C1-0B9C-4803-8C1B-9A86DF455F16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fafcf953018573f92a433319a1c11197d7661331","datavalue":{"value":"coinduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089035$E867AE25-4683-45FD-94D1-F5A510C1CA38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"87eba31a19b98c71e9abca58a20a6775e063d827","datavalue":{"value":"sized types","type":"string"},"datatype":"string"},"type":"statement","id":"Q5089035$6645EBB2-254B-413F-98EA-1D1D22ECF453","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":"Q5089035$A2BBF67D-925C-47F2-8CFC-8C98C38AE7F3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5249c80fcd11fa0612fb7dd29644b8dc29907a14","datavalue":{"value":{"entity-type":"item","numeric-id":4939690,"id":"Q4939690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$EF50F94E-D84C-4675-BD9D-9BC02ECE2EC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6519e78c88768a783b2e41047ba9f54f9a675438","datavalue":{"value":{"entity-type":"item","numeric-id":4995161,"id":"Q4995161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$A1433340-9718-44B0-AF91-AD8641ECD6EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57ea5885832b9f867e6bed74c7137f05eec86479","datavalue":{"value":{"entity-type":"item","numeric-id":2931780,"id":"Q2931780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$1776E869-641E-4E29-A405-836072756CCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9adc9ece3fc28f9fa23c825c75712926538583a7","datavalue":{"value":{"entity-type":"item","numeric-id":2789044,"id":"Q2789044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$5A82CA6D-75A4-4216-B5C4-37ACB22E2331","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34a544eff9bd65de4592fa7b247517554bcdddd5","datavalue":{"value":{"entity-type":"item","numeric-id":2828239,"id":"Q2828239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$D0E32D3A-EB29-41FA-93CC-1F038132FEE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8c7616163d4c3c1da7c14cb6770dc41c8c4dd14","datavalue":{"value":{"entity-type":"item","numeric-id":5244800,"id":"Q5244800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$4269945A-ABF9-45B9-BEA4-A035A1461F3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"064320c898684f731a75d9b590e5a89bb2e057ec","datavalue":{"value":{"entity-type":"item","numeric-id":5144643,"id":"Q5144643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$52734CC5-81AE-46AA-B55E-FB4CDB4F551F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6456459239ab3bc5fb70e6036ded27e15251da27","datavalue":{"value":{"entity-type":"item","numeric-id":3166222,"id":"Q3166222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$237DA3F4-0DC5-4776-BC61-E1197E7EA271","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"072b5fb9c9a1c997399d8dc463715bbc2b6911ef","datavalue":{"value":{"entity-type":"item","numeric-id":2811330,"id":"Q2811330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$9C147A11-C8B7-4FA2-A84B-6ABE5BFFED6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31f5eaa659fe8e8ca88c500da0fd4cebc92efeb8","datavalue":{"value":{"entity-type":"item","numeric-id":2804938,"id":"Q2804938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$2A6D06B6-E13F-48AE-A70F-477BDE02C746","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91fe9d16779ad15662d25b9e25734ff43ba2fad7","datavalue":{"value":{"entity-type":"item","numeric-id":2949454,"id":"Q2949454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$8818F9F7-D3ED-4151-94F0-9525DC4F0F4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f6f8766e5c0ef891b06dd86d56e3436041297c02","datavalue":{"value":{"entity-type":"item","numeric-id":6083690,"id":"Q6083690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$750EECCF-152F-4131-A81E-EE819EB8062B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"774c78d6dbda4571a17369b1d7dd4c328ec3072f","datavalue":{"value":{"entity-type":"item","numeric-id":3575268,"id":"Q3575268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$4521CBCB-48A9-44EC-9664-32BE5C8B6FA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4da806e6297e618e7714c75d11216ab0dccef6a6","datavalue":{"value":{"entity-type":"item","numeric-id":1189567,"id":"Q1189567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$06F89629-37F9-487A-BD1F-3027BD7C8962","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57dc163f9a92f92cb8fe7d3aa3b03ecb4dc0a54d","datavalue":{"value":{"entity-type":"item","numeric-id":4993353,"id":"Q4993353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$60A93101-5CC3-4CAE-8F0F-5455D375C732","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"175cbf8a20822167166d2c3042a8727801090085","datavalue":{"value":{"entity-type":"item","numeric-id":4635656,"id":"Q4635656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$BC1A4355-EBDB-41DA-BF79-9BFFE15FA6A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d485418966b2d901af8aed1e09d37a587c9ec423","datavalue":{"value":{"entity-type":"item","numeric-id":5271060,"id":"Q5271060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5089035$EC43D02C-3016-45A2-8CD8-B20548CC21C9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a1f1e51875b3cc3c712f140fa8ebeaab5e98bb10","datavalue":{"value":"10.4230/LIPICS.FSCD.2019.32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5089035$677C86FD-A865-4725-BF81-949D807E47AB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9892fc98bbefb0a9f2ddd559807aca5e8db6622b","datavalue":{"value":{"entity-type":"item","numeric-id":2949454,"id":"Q2949454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13837e4a5ec9376df242974a7af3033e523e4c0f","datavalue":{"value":{"amount":"+0.8154655694961548","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":"Q5089035$D83C62A9-8762-411A-BB0D-B8E59E9AF9EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67c3fd0446b514853334ac69119827a8eca4b15e","datavalue":{"value":{"entity-type":"item","numeric-id":4635656,"id":"Q4635656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b480dba193c75087b6f29e0241ccb2760c3678c","datavalue":{"value":{"amount":"+0.8098946809768677","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":"Q5089035$150C80FE-1295-4AB1-A22E-5955E0309F57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6922a340f259f222c652fb9237b5b015ff20319","datavalue":{"value":{"entity-type":"item","numeric-id":2974778,"id":"Q2974778"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6430cdf555f17febe683baa8d2bf2ee1080a2134","datavalue":{"value":{"amount":"+0.7969781756401062","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":"Q5089035$040C8E33-5EC0-4403-BEC1-768F832BEB9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3061c25d6f2c9d8be47fee4dfab609b514b4579a","datavalue":{"value":{"entity-type":"item","numeric-id":5144643,"id":"Q5144643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3d2ca06051664a3fee3c4e42a873ae14a713865","datavalue":{"value":{"amount":"+0.7707192897796631","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":"Q5089035$3EE81544-D551-4856-96BA-7BBE02D07A70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"23c095875774ffee57b0e0e5306fd68355b8adc7","datavalue":{"value":{"entity-type":"item","numeric-id":2811330,"id":"Q2811330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7cee64d4de937eead25bafd4f99c28e6de2daf89","datavalue":{"value":{"amount":"+0.7618836164474487","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":"Q5089035$991229B4-4115-47CF-9833-5D21A4AA6B21","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5089035","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5089035"}}}}}