{"entities":{"Q408534":{"pageid":410301,"ns":120,"title":"Item:Q408534","lastrevid":61681356,"modified":"2026-04-11T00:55:42Z","type":"item","id":"Q408534","labels":{"en":{"language":"en","value":"Unifying sets and programs via dependent types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6022766"}},"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":"Q408534$607AC774-A807-43DA-8386-78844670A8B4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"dc3bec4707fbaf06470b01e5585720cf454e5c9f","datavalue":{"value":{"text":"Unifying sets and programs via dependent types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q408534$E8C2D554-56AB-4E2D-9672-32C605762270","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7f6034a5800047f747f91f402012c95e26efb00e","datavalue":{"value":"1238.68050","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$4D0D1E67-2677-44F9-A09B-DE03F7575FE5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7d45bc58b6343c85796331c2c0125934a8b7086","datavalue":{"value":{"entity-type":"item","numeric-id":408533,"id":"Q408533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$6E9FA52A-4582-4F79-8580-36CB3044F0D8","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$142940F7-2F7C-461A-9697-FCF5A5059FEA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b23f7bc3899b33a4c3b235a941fe6fd0e7130556","datavalue":{"value":{"time":"+2012-04-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q408534$AFC44900-9335-42C5-B1E0-C36E0494F8C7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$407E9461-42BA-4589-98D2-71A81BA2F933","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b0919c48a255b26fcf065230a9a621cd8c579a3","datavalue":{"value":"03E70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$4607BA55-57B0-4A29-9E9E-66ADC88D9DEE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$2D4D720F-A86C-43E2-8CA7-1642FCEB516E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d2f2b562c3feb4eb9c8b8b71d938a78cb813bcfd","datavalue":{"value":"6022766","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$A8708599-DB64-465B-91C7-4A3E0C8E9C38","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d9fe5be894cb092393ff85e0f41c719edbf1e697","datavalue":{"value":"constructive set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q408534$611423B9-C805-44B8-914C-73F82CE8E38B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q408534$B34BDE7F-2735-4439-BD03-CDC6176A7DDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q408534$22949687-7AF4-45AE-954B-39D14239012D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$C26384D5-410C-485E-8563-BCFC4EEFED28","rank":"normal"},{"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":"Q408534$77C1AB41-D0A9-4AE1-9243-FD20128D63D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$34488187-24CA-4318-94F4-BCD0EC98CFAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$6624EB17-9756-478A-AC3B-FC026D4BBE34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$7DFD0F40-6AF2-4CD7-AA6B-EF26EF97546A","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":"Q408534$BEB0F10B-B8F8-41B5-866F-B04D36783FA9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"37df2bdf0ed3b85a4c708456410556e9886a16a4","datavalue":{"value":"https://doi.org/10.1016/j.apal.2011.09.016","type":"string"},"datatype":"url"},"type":"statement","id":"Q408534$0B9D3939-01E5-48A4-BBEA-2C80646EE644","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"099ad2e6273eac6b53d6c166d5991796565ccb0d","datavalue":{"value":"W2070864670","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$8E2395F6-DCF2-4B5D-BB25-BE45A5F67D02","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae170f67b5a99f655b51707d2e6917e4913c4d7a","datavalue":{"value":{"entity-type":"item","numeric-id":4208552,"id":"Q4208552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$C77B88A1-44C2-49CE-A848-2500372E4860","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e21df1d3055daa4725f01a29fad1e4853704fa4c","datavalue":{"value":{"entity-type":"item","numeric-id":3762311,"id":"Q3762311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$9F85E2D5-ADAA-4EBD-BEB8-9B9086CE2C65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e6f0b82d28d67b4e3312c91b8fa8f0254a3dc1e","datavalue":{"value":{"entity-type":"item","numeric-id":4524766,"id":"Q4524766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$B606A385-073C-414E-8371-1A0C93EDF8F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"819a2535befb2a67f49ee5e43432525215be36de","datavalue":{"value":{"entity-type":"item","numeric-id":4702972,"id":"Q4702972"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$0108BE63-E7BB-4C9C-87A8-E8C0A40C8084","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9595474d6c649f08e5d55140eff822a5539301af","datavalue":{"value":{"entity-type":"item","numeric-id":3613407,"id":"Q3613407"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$0FE80DBC-F79E-436F-8944-C9F9D3C852E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc3f49c7e55fab01a06f84c68fdf4990068cc091","datavalue":{"value":{"entity-type":"item","numeric-id":4357062,"id":"Q4357062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$7188AE5E-1ADA-4115-9D5F-DB9002A2F151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3551f2a22d68d8091928801d8423ada3760e3e7a","datavalue":{"value":{"entity-type":"item","numeric-id":3863865,"id":"Q3863865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$A7BA4CDD-E7F9-469C-B961-B40264C2E92A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$2FBEE57C-8147-40DF-9BED-7250CD897212","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3a442df7fc5b2e13404a6aff88cfc0223c7cbae","datavalue":{"value":{"entity-type":"item","numeric-id":1193653,"id":"Q1193653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$BCF4EE72-78A9-49DD-A0CD-483B826C51B5","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":"Q408534$8795840A-D130-47B1-9B08-E6EF512538FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9854627288bb9c35dacdc8035d00458c4f8cde85","datavalue":{"value":{"entity-type":"item","numeric-id":4490719,"id":"Q4490719"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$A37F140A-9711-4131-81DF-0F514537169F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"04cc1322638944d58c97f2602d06ebe61743d649","datavalue":{"value":{"entity-type":"item","numeric-id":4354789,"id":"Q4354789"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$D63BBF4E-C45E-4435-B7E7-079A8246F23C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da47f505e4676f000e190202d67ce831f4acdb1b","datavalue":{"value":{"entity-type":"item","numeric-id":4921444,"id":"Q4921444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$69D83892-46E2-470B-B507-7B07D2350396","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3671c04a28b3c6321772a8c859c51ac112c8b4d","datavalue":{"value":{"entity-type":"item","numeric-id":1127334,"id":"Q1127334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$EDA258B1-EFB5-49C5-B4EE-172EFF2F4D63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"412c65ba7cbb4986ecab32f5da59be81d7bb88f4","datavalue":{"value":{"entity-type":"item","numeric-id":5901479,"id":"Q5901479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$FFE64405-DFBC-4FFE-84FB-04C55BC71D07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59c8e9d898906d9e08aa7d9efe3af4528b97ee58","datavalue":{"value":{"entity-type":"item","numeric-id":5426072,"id":"Q5426072"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$188F130D-0F27-43B4-A99F-B9423C938469","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e13325bae56272b4ba305483ee09cc3ad5047e8","datavalue":{"value":{"entity-type":"item","numeric-id":3214891,"id":"Q3214891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$26C999C8-DE7F-4F41-815F-892F16AB253B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e32e6c895a421389f04c5499d388fc13d53e99f","datavalue":{"value":{"entity-type":"item","numeric-id":2778806,"id":"Q2778806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$79AB5016-E335-4AE1-886F-04E047B08A21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4441a33df5428b009347f1022f1440c1aaee513","datavalue":{"value":{"entity-type":"item","numeric-id":881453,"id":"Q881453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$BA931B66-A060-47E9-9972-B8C95E161DC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"86bf808c34edd92c2b99b788129bd6db0f113c6b","datavalue":{"value":{"entity-type":"item","numeric-id":1876088,"id":"Q1876088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q408534$2714C3BA-41E1-4D5F-974B-0069A237C6D2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"103ee8714c07b017e211af0f1b076d63d7f994c7","datavalue":{"value":"10.1016/J.APAL.2011.09.016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q408534$2C06C3FA-CDE6-4FA2-A32E-E08190E7D401","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec5da10da657af8f7990cb7e2a5fd9b0658a0622","datavalue":{"value":{"entity-type":"item","numeric-id":3605541,"id":"Q3605541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"90b9f89ecb396274cc212141fbba79df6e94273c","datavalue":{"value":{"amount":"+0.998909831047058","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":"Q408534$52ED08AE-5554-4CE1-B899-55E538CD9CDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0fb18c1c5852128bff5686d0e5094ce1a989c69c","datavalue":{"value":{"entity-type":"item","numeric-id":2757819,"id":"Q2757819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6035e979fe3e4a1760f66e2d5aec3808da5ab37","datavalue":{"value":{"amount":"+0.7810139656066895","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":"Q408534$7EDB5377-C35F-422A-8001-79C0F3EDA36C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b981abc9d5a2934b1599e79993a3b619b1e445cd","datavalue":{"value":{"entity-type":"item","numeric-id":3613410,"id":"Q3613410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab3ae927bf4b9a3d52f2bcb26e02fe768d66bbf6","datavalue":{"value":{"amount":"+0.7211490273475647","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":"Q408534$863F6959-2533-48B4-8F1C-EBBA177E2615","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec2f0bb38b56f759cbb69a7dc3cbce032e16f8c6","datavalue":{"value":{"entity-type":"item","numeric-id":5055716,"id":"Q5055716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b81fe04758b033d096b9d21eee6fb15ac725aaa0","datavalue":{"value":{"amount":"+0.7181879878044128","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":"Q408534$9AB82AB1-4027-412E-AEB4-1E489FF284D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2fd0887d9303d6a5b7f60dd0479ea33753b3bb35","datavalue":{"value":{"entity-type":"item","numeric-id":5408400,"id":"Q5408400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce0b520124abccdd9e794bbef94651ddc1431c13","datavalue":{"value":{"amount":"+0.7082532644271851","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":"Q408534$3F841A59-7965-4FE9-B1BE-42E8F9182794","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Unifying sets and programs via dependent types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Unifying_sets_and_programs_via_dependent_types"}}}}}