{"entities":{"Q2936804":{"pageid":2947524,"ns":120,"title":"Item:Q2936804","lastrevid":52166633,"modified":"2026-01-21T02:06:09Z","type":"item","id":"Q2936804","labels":{"en":{"language":"en","value":"Effective interactive proofs for higher-order imperative programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6383944"}},"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":"Q2936804$442269C1-35A2-4B5F-838F-D0E8FF3E746C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0cbbb8533fcb3c99992dab30598dbb36eefc45d7","datavalue":{"value":{"text":"Effective interactive proofs for higher-order imperative programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2936804$3282CC29-7D71-4634-9074-7CB0B504D2CF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9c4d56594cd0bcaee73f587227d96e97ae88fae5","datavalue":{"value":"1302.68087","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$0F51FD13-41BB-4B8B-A1F6-F038196CB7B6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c495702fa4fe44c069b108537a83515896463eb8","datavalue":{"value":"10.1145/1596550.1596565","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$677E246F-A89C-4ED0-A73D-07FAFD57DD87","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d957a3f31f9610e79e212a1ae2ae0004027dee9c","datavalue":{"value":{"entity-type":"item","numeric-id":1702890,"id":"Q1702890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$E506D7E6-15D6-461B-9D9E-EB8777A8FF40","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"37c934bcf8e2c9b0dbbfdff9b30323524a23c9d7","datavalue":{"value":{"entity-type":"item","numeric-id":609754,"id":"Q609754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$D7E34238-F3D6-4A10-9B1F-C71B1C76CDFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1380f7d0e077e40df5a34bb335939f3c6ce8766c","datavalue":{"value":{"entity-type":"item","numeric-id":617975,"id":"Q617975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$49EE3229-C100-48AF-91FC-CFA0C8FC9175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"35bf2f3a894a597d19b27b5739e2d0210b5075c4","datavalue":{"value":{"entity-type":"item","numeric-id":2936803,"id":"Q2936803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$7B94C232-5D1A-4AE4-B5EE-D27D7473A4A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aaa9d25d4099917aaf828811c00c1624c46c9480","datavalue":{"value":{"entity-type":"item","numeric-id":617976,"id":"Q617976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$8AD4694F-139E-4F25-ABE8-F3172E456323","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"304e11f28f1f8f9fec1b2f20c4f059e0c713c531","datavalue":{"value":{"entity-type":"item","numeric-id":2936796,"id":"Q2936796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$C8AA67F0-E993-467B-A4C5-DD2D7C4E342B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"39d11daed231ddc9c09fdaf1d1bb16c5de77d47a","datavalue":{"value":{"time":"+2015-01-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2936804$E2C3A21B-042A-4489-8832-6E31D330B996","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"476df0c0c2d25b97b38620e603ce1f9261e4ef35","datavalue":{"value":"http://nrs.harvard.edu/urn-3:HUL.InstRepos:4686803","type":"string"},"datatype":"url"},"type":"statement","id":"Q2936804$AF8BB532-EBC9-4204-B898-3A55B8D5F2B1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$ECFB77DD-16A3-471B-9C96-62FC4A7A8E2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$CDD24552-5019-40BA-B0D8-19D4CC9B6937","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$4FA50B9F-16CF-4959-9CC7-961FC1F9EDCE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e6abd5c6d907d36bc565551aa0409a2f9175589b","datavalue":{"value":"6383944","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$D1C3A9F0-5D78-442D-B71B-8D8550FFB849","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936804$830B6450-4096-4E17-BC7B-E481D85F9C60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00b76a2e54f8798fe172effecd557ced03e2f904","datavalue":{"value":"functional programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936804$D6411B93-1FE3-4344-89AE-70D1D7A9A269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b18a74c599c9ab6e6047b499c4529cfa47686616","datavalue":{"value":"interactive proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936804$2C861AC9-C4D5-4A09-B1F4-0D5C3E80FFA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2936804$5F2DCE7F-78C4-42C0-B6D5-8F7FD0E73596","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":"Q2936804$3E8B5B45-C1BD-42DF-ADE7-E56D97720063","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":"Q2936804$03035BBE-1EC4-4904-8FBC-BB7A6DE3557A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"076ade2f424feb4292ee73db98fc22d62f6154a2","datavalue":{"value":{"entity-type":"item","numeric-id":16769,"id":"Q16769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$7813D494-7DA0-4A45-B283-140860FFFD78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"493c4272f3e5f72c11a4ab08cd3c037673ba4268","datavalue":{"value":{"entity-type":"item","numeric-id":21766,"id":"Q21766"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$AFA9CC6F-D454-4122-8B77-F92BB4B9D85F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4dfe52116eea178df8e98fcb66fd7e4802fcbfc","datavalue":{"value":{"entity-type":"item","numeric-id":24263,"id":"Q24263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2936804$D5E50853-CE23-44E7-8246-D97BB8DEFF52","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":"Q2936804$5EB900C5-5BAA-45F4-8DF7-E3BC09AFC1DE","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fc1986ffb203c368733d874d98ca2d46e03044b3","datavalue":{"value":"W2129671708","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2936804$BDF7F0F0-A940-4673-AB2D-6053740CBFBC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ffbed544246e54d1ce7de6f97ee1ad1afaff97c4","datavalue":{"value":{"entity-type":"item","numeric-id":5178765,"id":"Q5178765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9c96856184c142d1b8b3c7edbf9eb3d32371f34","datavalue":{"value":{"amount":"+0.7895451188087463","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":"Q2936804$4FF0F85A-7CFC-43AB-ACB3-1D1802FEC7F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13cececf5dd03a1f6016067f19008279b5c3a46c","datavalue":{"value":{"entity-type":"item","numeric-id":617977,"id":"Q617977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa86b1310661346e94240cdde041879ee25176c7","datavalue":{"value":{"amount":"+0.7888367176055908","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":"Q2936804$7E85EE47-4616-4019-8DBC-223A668E07A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54dac0ad3a84c5897bebd78827e84bdb3c2abbdb","datavalue":{"value":{"entity-type":"item","numeric-id":2324204,"id":"Q2324204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df8addbdb4fbe7bd2e1bf8d712e2852f1c82ba46","datavalue":{"value":{"amount":"+0.7864552736282349","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":"Q2936804$9383A0B5-4AEC-4E01-9150-50AE62716321","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ddfe8706eb56f964bdfd12380be6a420c1d49e0","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f8f12f4f6bc07ca761d23dedcaf112e837b1d73","datavalue":{"value":{"amount":"+0.7781482934951782","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":"Q2936804$0F87404F-C674-409B-A72C-940681D11DCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54945991e72c4e075bbdaee9b84ef77985d61019","datavalue":{"value":{"entity-type":"item","numeric-id":3087993,"id":"Q3087993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f732196efd66e21469fec3d930566801a3d2f29","datavalue":{"value":{"amount":"+0.7726170420646667","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":"Q2936804$0FE6DF62-2DDC-4DF5-B505-ACC12F812F24","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2936804","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2936804"}}}}}